Re: Gödel's system P, Principia Mathematica,

This is nothing to do with the metatheory in which
he proves the theorem.

sorry you are wrong again
godel derives his theorem directly from P

The*** general result about the existence of undecidable propositions goes
as follows:**
Theorem VI: For every Ï?-consistent primitive recursive class κ of
formulae there
is a primitive recursive class-sign r such that neither forall(v,r) nor
not(forall(v,r))
belongs to Conseq(κ) (where v is the free variable of r)


Since the premise in the theorem is Ï?-consistency, which is stronger than
consistency, the
theorem is less general than if its premise were just consistency.
Proof: Let κ be any Ï?-consistent primitive recursive class of formulae.
We define:
isProofFigure
κ
(x) â??
(
â??n â?¤ length(x).isAxiom(item(n,x)) â?¨ (item(n,x) â?? κ)â?¨
â??0 < p,q < n.immedConseq(item(n,x),item(p,x),item(q,x))
)
â?§
length(x) > 0
(5)
(compare to the analogous concept 44)
proofFor
κ
(x,y) â?? isProofFigure
κ
(x) â?§ item(length(x),x) = y
(6)
provable
κ
(x) â?? â??y .proofFor
κ
(y,x)
(6.1)
(compare to the analogous concepts 45, 46)

ETC

***One can easily convince oneself that the proof we just did is
constructive&***

****During the proof of theorem VI we did not use any other properties of
the system
P than the following:****
1. The class of axioms and deduction rules (i.e. the relation â??immediate
conse-
quenceâ??) are primitive recursively definable (as soon as you replace the
basic
signs by numbers in some way).
2. Every primitive recursive relation is definable within the system P (in
the sense
of theorem V).
****Hence there are undecidable propositions of the form â??x.F(x) in
every formal
system that fulfills the preconditions 1, 2 and is Ï?-consistent,,****

--
Message posted using http://www.talkaboutscience.com/group/sci.logic/
More information at http://www.talkaboutscience.com/faq.html

.