The problem about the Gödel proposition V in 1931 paper?

Question

Proposition V says that every recursive function R can find a relation symbol in system P such that:

R(v1, v2....,vn) -> prove(subst( r(u1,u2,...,u3), (z(v1),z(v2),...,z(vn)))

~R(v1, v2....,vn) -> prove(subst(not(r(u1,u2,...,un), (z(v1),z(v2),...,z(vn)))

Gödel didn't write the proof completely and I try to write the proof by myself.

I found a proof in this site.(Proof of Proposition/Theorem V in Gödel's 1931 paper?)

It says that for "R(x, y) ~ y = x+1", for you can write "r(x,y) ~ y = fx" in System P, so it is proved.

This can not satisfy me. See the following example:

R(0, 1) is the satisfied relation then proceeding the substitution in System P, it gets that:

r(z(0), z(1)) -> r(0, f0) -> f0 = f(0) -> f0=f0

For R(0,1) is the satisfied relation in recursive function, so prove(f0=f0) should be satisfied, i.e. you can prove "f0=f0" in system P.

Relations 1-46 can be regarded as a System P interpreter on a number theory computer.

See the following definitions:

22.FR(x)≡(n){0<n≦l(x)⊃Elf(n Gl x)
        ∨ (Ep,q)[0<p,q<n 
        & Op(nGlx,pGlx,qGlx)]} & l(x)> 0

23.Form(x) ≡ (En){ n≦(Pr[l(x)^2])^x.[l(x)]^2
                 & FR(n)
                 & x=[l(n)] Gl n} 35)

39.L2-Ax(x) ≡ (Ev,p,q){ v,p,q≦ x & Var(v) & Form(p)
                      ¬( v Fr p) & Form(q)
             \         & x = [v Gen (p Dis q)] Imp [p Dis (v Gen q)]}

42.Ax(x) ≡  Z-Ax(x) v A-Ax(x) v L1-Ax(x)
         v L2-Ax(x) v R-Ax(x) v  M-Ax(x)

44.Bw(x)≡(n){0<n≦l(x) ⊃ Ax(n Gl x)
         V (Ep,q)[0<p,q<n & 
                 Fl(n Gl x, p Gl x, q Gl x)]} & l(x) > 0

FR(x) and Form(x) defined the well-formed formula in System P. See L2-Ax(x) if we construct any well-formed formula which have to be satisfied for L2-Ax(x) or other axiom relations to be regarded as axiom‧

Bw(x) restricts the proof can be only derived from axioms defined in Ax(x) exactly. How to prove f0=f0 can be proved in Gödel System P interpreter(relations 1-46)?

I am trying many times but unable to find the proof! Does someone know it?

Answer 1

See the post understanding Gödel's 1931 paper: proof of Theorem V, regarding the difficulties to handle Gödel's system P.

Specifically, we have to note that system P is not FOL with equality, but high-order logic: equality is defined.

Thus, we have to prove the usual properties of equality, including:

$t=t$, for every term $t$ of the language [i.e.individual variables, $0$, $f0$, and so on].

---

Proof sketch

As stated by Gödel:

[system] P is essentially the system obtained when the logic of PM is superposed upon the Peano axioms (with the numbers as individuals and the successor relation as primitive notion).

For the logic, see:

• Alfred North Whitehead & Bertrand Russell, Principia Mathematica to *56 (2nd ed - 1927): *13 IDENTITY, page 168-on:

*13.15 $ \ \vdash x = x$

The proof needs the propositional law "Id." [*2.08, page 99]: $\vdash p \supset p$.

By substitution we get: $\phi(x) \supset \phi(x)$.

Now we need "generalization" [*10.11, page 139] to derive: $(\phi) (\phi(x) \supset \phi(x))$; with Gödel's notation: $x_2 \Pi (x_2(x_1) \supset x_2(x_1))$.

Finally, we have to apply:

*13.1 $ \ \vdash x = y \equiv (\phi) (\phi(x) \supset \phi(y))$ [page 169]

(with Gödel's notation: $x_1 = y_1 \equiv x_2 \Pi (x_2(x_1) \supset x_2(y_1))$), derived from Def *13.01 [page 169: the definition of identity; see Gödel's paper, footnote 21], to conclude by modus ponens with:

$x=x$.