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

On Jan 29, 8:53 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
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.

Thanks, I'll think about it tonight.

MoeBlee
.

Relevant Pages

  • Re: =?iso-8859-1?Q?G=F6dels?= system P, Principia Mathematica, and the reducibility axiom
    ... and rigorous terms - those of the system P you laid out - rather than ... Instead of the set axiom schemata of P introduce ... Propositional functions aren't extensional, so extensionality is not ...
    (sci.logic)
  • Re: ramified type theory
    ... >>> Propositional functions are not extensional in PM. ... > in fact great generals have all the properties of a great general. ... axiom of extensionality cannot prove the axiom of reducibility. ...
    (sci.logic)
  • Re: ramified type theory
    ... Chris Menzel wrote: ... > Propositional functions are not extensional in PM. ... extensionality or following Bertrand Russell's procedure of translating ... assertions about classes into assertions about propositional functions. ...
    (sci.logic)