0

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

Mauro ALLEGRANZA
  • 94,169
joseph M'Bimbi-Bene
  • 241
  • An identity like that is a logical necessity, so you do not need any axioms for that ... The formal rules of any complete proof system for first-order logic will be able to prove it. In fact, most such proof systems contain a rule that says that any statement of the form $t=t$ can be inferred (from nothing). This is often called 'Identity Introduction'. – Bram28 Oct 27 '16 at 12:35

2 Answers2

1

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.

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • will first give an exact description of the formal system P [...] . By and large, P is the system that you get by building the logic of PM on top the Peano axioms (numbers as individuals, successor-relation as undefined basic concept).

    I thought about looking for Principia Mathematica and Peano, but he explicitely states that he gives an EXACT definition of the system he uses.

    I think i totally get it when you talk about logical necessity but i feel like relying only on that would imply to involve intuition and not mechanical rules, unless i misunderstood you.

    Let me try harder ...

     – joseph M'Bimbi-Bene Oct 27 '16 at 13:05
  • Or use of outside rules – joseph M'Bimbi-Bene Oct 27 '16 at 13:08
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$ ].

Community
  • 1
Mauro ALLEGRANZA
  • 94,169