Proof of $(0=0)$ in Gödel's system

Question

Here is a translation i am using for my studies :

http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

it seems like a silly question, but i can't find a way, how do i prove (0=0) inside gödel's system ?

I feel like i have a solid intuition of the construction of the undecidable statement. Yet there are some parts i can't prove by myself, especially the theorem V.

I am trying to adapt the proof from Peter Smith's book, showing that "his" system P is "primitive-recursive adequate", but i don't know how to adapt it in godel's context and being unable to prove that (0=0) prevents me from carrying on my adaptation :

(p.125) "The successor function $\ Sx = y$ (outside of the theory) us captured by the open well formed formula Sx = y (inside the theory)

Gödel's system seems to lack an axiom :

http://web.mit.edu/24.242/www/PeanoArithmetic.pdf

(page2) "Proposition 1. $\ PA |- (\forall x) ((x=0) \lor ((\exists y)x=Sy)) $ with $\ S $ being the successor function

that axiom would solve everything but it's not in Gödel's system. I guess Gödel didn't make a mistake so what am i missing ?

Thank you

Answer 1

See your previous post regarding elementary formulae.

Equality is defined in Gödel's system; we have that $x_1=y_1$ is :

$x_2 \Pi (x_2(x_1) \to x_2(y_1))$

that reads : $\forall P [P(x_1) \to P(y_1)]$.

Form the logical law : $P(x_1) \to P(x_1)$ [*], we can derive the immediate consequence [**] : $\forall x_1 \forall P [P(x_1) \to P(x_1)]$, that reads :

$\forall x_1 (x_1 = x_1)$.

Using logical axiom-schema III.1 :

$v \Pi (a) \to \text {Subst} \ a^v_c$

that reads : $\forall v \varphi \to \varphi [v/c]$, with $0$ as $c$ we get, by modus ponens :

$0=0$.

---

Regarding Peano axioms, I'm quite sure that there is no mistake in Gödel's system.

The system is an high-order logic system (this is the reason why he can define equality, instead of using the usual fist-order axioms for it).

The arithmetical axioms used by Gödel are the translation in his own system of the last four axioms of original (second-order) Peano's formulation in Arithmetices principia, nova methodo exposita (1889).

The paper you have linked proves : $\mathsf {PA} \vdash (\forall x)(x = 0 \lor (\exists y) (x = sy))$ [it is a theorem, and not an axiom] using the induction axiom as well as some "theorems of pure logic" .

Having proved in Gödel's system $P$ that $0=0$, with 1.3 of Principia : $\vdash q \to (p \lor q)$ (one of the "theorems of pure logic" needed), we have :

$P \vdash 0=0 \lor (\exists y) (0 = sy)$.

Using equality we have : $sx=sx$, and thus $(\exists y) (sx = sy)$.

Thus, with 1.3 again, we conclude with :

$P \vdash sx=0 \lor (\exists y) (sx = sy)$.

Finally, with 2.02 of Principia : $⊢ q → (p→q)$ we derive :

$P \vdash ((x = 0 \lor (\exists y) (x = sy)) \to (sx = 0 \lor (\exists y) (sx = sy)))$.

Now the result follows by a suitable instance of the induction axiom schema and modus ponens.

---

---

Notes

[*] The logical part of Gödel's system is W&R's Principia Mathematica; see page 101 for the proof of:

2.08 $⊢ p → p$,

called the "principle of identity".

[**] In your translation one of the two rules of inference is omitted (it seems a typo) but it is used in def.43 IMMEDIATE CONSEQUENCE.

The two inference rules in Gödel's system are described as follows :

A formula $c$ is called an immediate consequence of $a$ and $b$ if it is the formula $(\sim (b)) \lor (c)$ [i.e.: $c$ is an immediate consequence of $a$ and $b$ if $a$ is $b \to c$ ], and it is called an immediate consequence of $a$ if it is the formula $v \Pi (a)$, where $v$ denotes any variable [i.e.: $\forall x \varphi$ (or $\forall P \varphi$) is an immediate consequence of $\varphi$ ].

Answer 2

No axiom (at least not specifically about numbers) is needed to prove something like that, since $0=0$ is a logical necessity: anything is idetical to itself, whether we are talking about numbers, apples, or whatever. So, you should be able to derive it using the purely logical rules or axioms. Same with something like $s(0) = s(0)$, or $joseph = joseph$.

Most logical proof systems for first-order logic will have a rule that allows you to obtain any sich identity in a single step, typically called Identity Introduction. It is only when you want to prove something like $0 + s(0) = s(0)$ that you start to need axiom for the natural numbers, like the Peano axioms. Of course, if you want to prove $0+s(0) = 0+s(0)$, you are back at a logical necessity, and you can use Identity Intoduction to prove that in 1 step.

So, figure out what the purely logical rules or axioms are that Godel uses in his paper, and you should be able to prove $0=0$ quite easily.