1
$\begingroup$

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.

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

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.

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$ – Daniels Krimans Sep 25 '18 at 19:40
  • $\begingroup$ So my idea was that you can take any axiom from number theory that is not in propositional calculus and then you will have proof of it but because it will be replaced by single propositional letter you obtain a contradiction for the theorem stated. $\endgroup$ – Daniels Krimans Sep 25 '18 at 19:43
  • $\begingroup$ Yes, it is true. But what about $\Gamma^* \vdash E^*$? $\endgroup$ – Daniels Krimans Sep 25 '18 at 19:44
  • $\begingroup$ @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). $\endgroup$ – hmakholm left over Monica Sep 25 '18 at 19:46
  • $\begingroup$ Is that so? I will think about it for some time, thank you. I guess it makes sense. $\endgroup$ – Daniels Krimans Sep 25 '18 at 19:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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