Converse of substitution for propositional letters

80 Views Asked by At

I would like to get some advice in understanding the following theorem found in Kleene's "Introduction to Metamathematics" chapter VI section 25.

Theorem: Let $\Gamma$ be propositional letter formulas, $E$ be a propositional letter formula in the distinct propositional letters $P_1, ..., P_m$. Let $A_1, ..., A_m$ be formulas (in number-theoretic sense). Let $\Gamma^*$ and $E^*$ result by substituting simultaneously $A_1, ..., A_m$ for $P_1, ..., P_m$ respectively. Also assume that $A_1, ..., A_m$ are distinct prime formulas. If $\Gamma^* \vdash E^*$ then $\Gamma \vdash E$.

I am not sure I understand the statement because I am not sure I agree with this statement.

Assume the case where $\Gamma$ is empty. Then, $\Gamma^*$ is empty as well. Let $E$ be a propositional letter formula $P_1$. It is a formula because a propositional letter is a propositional letter formula. Let $A_1$ be a formula in number-theoretic sense $a+0 = a$. Then, $E^*$ is a result of substitution and is equal to $a+0=a$. Also, $A_1$ is prime formula because it is not of the form $A \supset B$, $\lnot A$, $A \& B$, $A \lor B$. So, by the theorem it should be the case that if $\vdash a+0=a$ then $\vdash P_1$. The first deduction is true because $a+0=a$ is an axiom in number theory. On the other hand, I think you can not prove $\vdash P_1$ in pure propositional calculus.

I would appreciate your thoughts on this.

1

There are 1 best solutions below

5
On BEST ANSWER

Your reasoning breaks down because it is not the case that $\vdash a+0=a$. It is true that $a+0=a$ in everyday mathematics, but it is not something we can prove in pure logic. It depends on axioms about how the $+$ and $0$ symbols behave, and you're explicitly not assuming any such axioms here.

In fact, for the claimed theorem to be true we need to be working in a predicate calculus where $=$ is not a logical primitive, such that we don't even have $\vdash 0=0$. But for all I know, that could well be the context Kleene is working in.