# Converse of substitution for propositional letters

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.

• See page 108: a propositional letter formula is not a single prop letter. $\mathcal A \lor \mathcal B$ is a prop letter formula. – Mauro ALLEGRANZA Sep 25 '18 at 19:29
• @MauroALLEGRANZA From page 108: "1. A propositional letter is a formula". – Daniels Krimans Sep 25 '18 at 19:32
• Example with $\Gamma$ empty : $E^*$ is $(a=0) \lor \lnot (a=0)$ and $E$ is $\mathcal A \lor \lnot \mathcal A$. – Mauro ALLEGRANZA Sep 25 '18 at 19:32
• @Mauro, I'm having some trouble seeing how your comments relate to the question here. Could you be more explicit? – hmakholm left over Monica Sep 25 '18 at 19:35
• @MauroALLEGRANZA In my edition (1971) page 112 theorem 4. – Daniels Krimans Sep 25 '18 at 19:45

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.
• Sorry, I was not explicit enough. Actually in Kleene's book $a+0=a$ is taken as an axiom in number theory. Can you explain a little bit more about why my idea about why theorem is not true is not true? – Daniels Krimans Sep 25 '18 at 19:40
• Yes, it is true. But what about $\Gamma^* \vdash E^*$? – Daniels Krimans Sep 25 '18 at 19:44
• @DanielsKrimans: Whoops, I missed some stars. I meant to say: In order for the theorem to be true, it must be that $\Gamma^*\vdash E^*$ means that $E^*$ can be derived from $\Gamma^*$ without using any of the non-logical axioms of number theory. (Except in case some of those axioms happen to be in $\Gamma^*$, of course). – hmakholm left over Monica Sep 25 '18 at 19:46