Re: Gödel's system P, Principia Mathematica, and the reducibility axiom

Jan Burse schrieb:
Aatu Koskensilta schrieb:
My current assumption until now was that Goedel used
P to proof his theorem about his Godelization of P.

Hint:
at least syntactically I have evidence that he proofed
something about a Goedelization of P:

We have provable is defined by means of proofFor and other things.
is proofFor is defined by means of isProofFigure and other things
is isProofFigure is defined by means of isAxiom and other things
is isAxiom is defined by means of redAxiom and other things.

But I am not so sure whether he really used full P in
proofing his theorem. I was following a little his proof,
and I didn't really see comprehension. At least I could
not yet figure out whethere he uses or needed comprehension.

He also writes:

One can easily convince oneself that the proof we just
did is constructive, i.e. it the following is
intuitionistically flawlessly proven:

I am not so sure whether this is true, what the scope of
this note is. Maybe he talks only about the Goedel sentence
and not about some lemmas he uses.

For example he uses the following lemmas:

forall x(provable_k(x) <-> x in conseq(k))

forall x(provable(x) -> provable_k(x))

forall x(r(x) -> provable(subst(r,u,number(x)))) r primrec

forall x(~r(x) -> provable(not(subst(r,u,number(x))))) r primrec

Damned, do we need redAxiom to proof these? Think I
saw something about this in Shapiro.

Best Regards
.