# Confusion about proof that first order logic without equality is not contradictory

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?

-
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

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.
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