LudovicoVan
Posts:
4,025
From:
London
Registered:
2/8/08


Re: Goedel's 1931 proof is not purely syntactical (?)
Posted:
Nov 7, 2013 4:07 PM


[Followup set to sci.logic only.]
"Alan Smaill" <smaill@SPAMinf.ed.ac.uk> wrote in message news:fwe4nl1ecfu.fsf@eriboll.inf.ed.ac.uk... > "LudovicoVan" <julio@diegidio.name> writes: >> "Alan Smaill" <smaill@SPAMinf.ed.ac.uk> wrote in message >> news:fwepq3qcru8.fsf@eriboll.inf.ed.ac.uk... >>> "LudovicoVan" <julio@diegidio.name> writes: >>>> "Alan Smaill" <smaill@SPAMinf.ed.ac.uk> wrote in message >>>> news:fwevcdicxwv.fsf@eriboll.inf.ed.ac.uk... >>>>> "LudovicoVan" <julio@diegidio.name> writes: >>>>>> "Alan Smaill" <smaill@SPAMinf.ed.ac.uk> wrote in message >>>>>> news:fwe390m97ia.fsf@eriboll.inf.ed.ac.uk... >>>>>> >>>>>>> The claim is rather that the implication is provable in the >>>>>>> particular >>>>>>> object theory that Goedel uses. That is to say, the claim in >>>>>>> this instance is that there are syntactic proofs showing >>>>>>> >>>>>>>  (x = 0) > Bew [ Sb (Aeq) {u0, u1}_{Z(x), Z(0)} ] >>>>>>> >>>>>>> and >>>>>>> >>>>>>>  ~(x = 0) > Bew [ Neg Sb (Aeq) {u0, u1}_{Z(x), Z(0)} ] >>>>>>> >>>>>>> (here using  to indicate provability in PM). This establishes >>>>>>> a relationship between proofs of statements in PM, and the >>>>>>> formalised >>>>>>> proof predicate Bew. >>>>>> >>>>>> And how do you prove that "claim"? >>>>> >>>>> Goedel outlines the proof immediately after stating Theorem V >>>>> (as it's called in the van Heijenoort translation). >>>> >>>> Then you must be misunderstanding my question: it is that exact proof >>>> that I am talking about, asking how he does establish *the base case*. >>> >>> Yes, I thought you were asking about the more general question. >>> >>> What we want to show is not exactly as you gave it, but >>> is in terms of particular numbers, not x=/= 0. >>> We need that formalised subsitution does what we expect, namely >>> that if F is encoding of F, namely the encoding of the >>> formula with substitution is the result of Sb applied appropriately >>> to the encoding of the formula. But this is provable, >>> in the metatheory, and independently of interpretation. >> >> I don't see a significant difference between interpreting and proving >> in the metatheory, in that the "purely syntactical" nature of the >> proof seems lost anyway: IOW, if I am getting you correctly, that >> formalised substitution does what we expect is anyway not proved at >> the object language level. > > It is possible to have formal proofs at the metalevel also.
But again not purely syntactical, ad libitum.
>> In hindsight, I'd say that indeed it can >> never happen: that a proof is fully mechanical since inception. > > Well, "inception" already suggests a human starting point.
As it should be, the matter suggests the appellation, not the other way round. Anyway, yes, the "human starting point" is exactly what I had in mind.
> On the other hand, automated mechanical theorem proving > systems can and do come up with proofs of statements > on their own, even where it is not known in advance whether > or not a proof exists.
That is interesting: are these systems able to come up anything like a proof of the incompleteness theorem?
Julio

