Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am having a problem understanding a proof from the field of mathematical logic. Seems like my brain cannot digest concepts from logic very well.

I will quickly define some terminology and then present my issue.

We say that a theory T is contradictory if there is $ \vdash_T \perp$ that is, there exist a proof of $\perp.$ We already proved that propositional logic $\mathbb{I}$ is not contradictory. Let $\mathbb{P}$ denote first order logic without the rules for equality.

I want to show that $\mathbb{P}$ is also not contradictory. The idea we used at the classes is to construct a function $s$ mapping formulas from $\mathbb{P}$ to formulas in $\mathbb{I}$ such that

  1. $s(\perp) = \perp$
  2. If $ \vdash_{\mathbb{P}} \phi$ then $\vdash_{\mathbb{I}} s(\phi)$ that is, if there's a proof of $\phi$ using the rules of $\mathbb{P}$ then there is a proof of $s(\phi)$ in $\mathbb{I}$.

The existence of such a $s$ would then imply that $\mathbb{P}$ is not contradictory.

In our classes we defined $s$ in a certain manner and showed that $1.$ and $2.$ holds by ways of induction on the structure of a possible formula in $\mathbb{P}.$

I am wondering why the function defined as $s(\perp) = \perp$ and $s(x) = \top$ if $ x \not = \perp$ wouldn't be good as well?

I am aware this must be quite a dumb proposal since in this case, conditions 1. and 2. are satisfied blindly (are they?) and there is no difference in taking $\mathbb{P}$ or simply taking the whole first order theory with rules for equality included.

So either there is something else that $s$ must satisfy in order to be able to conclude that such an $s$ guarantees that $\mathbb{P}$ is not contradictory, "my" $s$ does not satisfy the assumptions 1. 2. or some other stupid confusion I am having.

Can someone enlighten me?

share|cite|improve this question
Well you certainly require some structural preservation. Maybe (1) means that if $\phi$ is equivalent to $\bot$ then $s(\phi)$ is equivalent to $\bot$ in $\mathbb{I}$? – Apostolos May 8 '12 at 16:35
The function you propose satisfies both conditions, but to prove that it satisfies condition (2) you need to know that $\mathbb{P}$ is consistent, which is what we are trying to prove in the first place. – Andrej Bauer May 10 '12 at 21:40
up vote 2 down vote accepted

The idea of the whole proof is that if you would have a proof of $\bot$ in $\mathbb{P}$, you could convert it into a proof of $\bot$ in $\mathbb{I}$. And since you know that no such proof exists in $\mathbb{I}$, you conclude that there cannot be such a proof in $\mathbb{P}$.

This gives one more property that $s$ must satisfy:

  • If you take a valid proof in $\mathbb{P}$ and apply $s$ to all its formulas, you get a valid proof in $\mathbb{I}$.

Only then, you can conclude that if you'd have a proof of $\perp$ in $\mathbb{P}$ you could use $s$ to convert it into a proof of $\perp$ in $\mathbb{I}$.

The mapping you suggested doesn't have this property. For example, if we derive $P, \lnot P \vdash_{\mathbb{P}} \perp$, your mapping would convert it into $\top, \top \vdash_{\mathbb{I}}^{?} \perp$, which is not a correct derivation.

share|cite|improve this answer
Well, you can require this additional property of $s$, but it isn't strictly necessary. There is no need for $s$ to be able to translate whole proofs; it only needs to know that proofs exist when they should. The real problem with the OP's suggestion was explained by Andrej in a comment above. – Miha Habič Aug 11 '12 at 22:30

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.