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

Aatu Koskensilta schrieb:
On 2008-01-29, in sci.logic, MoeBlee wrote:
Would you please re-express that last paragraph in more contemporary
and rigorous terms - those of the system P you laid out - rather than
Russell's antiquated notion of propositional functions?

Add to the language of P infinitely many predicates: order[0], order[1],
order[2], and so on. Instead of the set axiom schemata of P introduce
the following axiom schema:

(Ep)(x)(order[k](p) & (p(x) <--> P))

where the type of x is n and that of p n+1, p does not occur free in
P, and all variables x in P are either of type <= n or restricted
by the predicate order[k-1](x) \/ order[k-2](x) \/ ... \/
order[0](x). (If k is 0 all variables must be of type <= n).

Propositional functions aren't extensional, so extensionality is not
included.

Where would you make this change?

My current assumption until now was that Goedel used
P to proof his theorem about his Godelization of P.

At least it can be seen from 2.1 Definitions and
2.4 Expressing metamathematical concepts, that 2.4
mirrors 2.1. (*)

Lets say you have replaced the comprehension schema
of Gödel by your order restricted comprehension schema,
lets call the new system P'. Do we then have?

Goedel could also have used P' to proof his theorem
about his Godelization of P.

- or -

Goedel could also have used P to proof his theorem
about his Godelization of P'.

- or -

Goedel could also have used P' to proof his theorem
about his Godelization of P'.


Best Regards
(*)
http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

.