Re: Godel's original proof of completeness

From: Bruno Marchal <marchal.domain.name.hidden>
Date: Tue, 4 Apr 2006 10:40:24 +0200

Le 03-avr.-06, ˆ 14:46, LISP a Žcrit :

>
> Has anybody read Godel's orginal proof before.
>
> http://en.wikipedia.org/wiki/
> Original_proof_of_G%C3%B6del%27s_completeness_theorem


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)
(z­s(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.

Bruno


http://iridia.ulb.ac.be/~marchal/


--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to everything-list.domain.name.hidden
To unsubscribe from this group, send email to everything-list-unsubscribe.domain.name.hidden
For more options, visit this group at http://groups.google.com/group/everything-list
-~----------~----~----~----~------~----~------~--~---
Received on Tue Apr 04 2006 - 04:41:41 PDT

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:11 PST