Le 03-avr.-06, 14:46, LISP a crit :
> Has anybody read Godel's orginal proof before.
A long time ago I take a look on it.
> The above proof sketch is partial.
> Like most computer scientists, I was only educated to learn
> Henkin's proof.
A good one. Easy to generalize, for example to quantified modal logic.
> One thing I dont understand. It is obvious that Henkin's
> proof relies on constants (to deal with the quantifiers), but
> Godel's proof starts with a version of predicate calculus
> (called Restricted Functional Calculus) without constants at all.
> Does anybody understand why constants are not essential
> in Godel's?
I guess you mean constant for 0-ary functional symbol. Like the
constant "0" in Peano Arithmetic.
I think you can always replace them by the use of an existential
quantifier "E". Let me use "(x)" for "for all x".
For example: (x)(0 s(x)) can be replaced by Ey((x)(y s(x) & (z)
(zs(x)) -> y = z)). The last conjunct must be added to say that "0" is
unique. You can use this in the formulation of the induction axioms.
All the same: in second order logic you should be able to code in this
way the unary (and others) functional constant. F(x) -> A should be
replace by EX(X(x) -> A).
Those constant are really only sort of syntactical sugar.
> Why can I find the material to show RFC to be equivalent
> to the Predicate Calc with constants? Note that the wikipedia
> sketch has this argument missing as "(to be written)".
It is a little bit technical and out of topic, but you should find a
precise specification of "RFC" in order to see if it is really
equivalent. I guess now that it would be equivalent with predicate
calculus with the identity symbol.
Hope that can help.
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to firstname.lastname@example.org
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at