Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 12 Sep 2006 18:16 george wrote: > Peter_Smith wrote: > > george wrote: > > > > > Godel's original proof was a formal derivation. > > > > No it wasn't. Gödel's original proof was a bit of informal > > mathematics. > > The overall outline may have been informal > but this informal shell housed a huge formal > kernel. There is nothing whatsoever informal > about defining a whole bunch of predicates to > construct a Godel sentence. There is nothing > informal about an explicit Godel numbering. You have to tell in advance an exact algorithm that creates every proof. You are saying that it can be formalized, but Godel didn't. BTW To formalize the results of Godel et. al., it helps to rearrange the arguments into a "tree structure" of logic. If you formalize it verbatim, then you have more or less a program that is being defined - "take wff G. If it is provable, then . . . If it is not provable, then consider . . ." Then you have to describe what these "programs" in general accomplish - not so easy! But if you rearrange it so you see that e.g. the result is showing that P=>Q and Q=>P and then that P==Q, you can develop rules for constructing these tree structures. (That's how CBL does it.) C-B
From: Peter_Smith on 12 Sep 2006 19:20 george wrote > Godel's original proof was a formal derivation. I wrote > No it wasn't. Gödel's original proof was a bit of informal > mathematics. He *claimed* in 1931, at the end of his great paper, that > the informal reasoning could be carried out within the formal > type-theory he labels P. But he didn't show it there. Tthe first formal > proof was given by Hilbert and Bernays some years later. C-B wrote > You're going to have to define "formal proof" here. Why so? The situation is surely entirely clear and entirely well-known. (i) Gödel in 1931 showed that a certain sentence is not formally derivable within the formal system P (a simplified version of the type theory of Principia). (ii) His argument for this is a bit of ordinary unformalized mathematical reasoning, rendered as it happens in German, not within P. (iii) However, there isa sentence of P's formal language, call it Th, which -- via coding -- expresses the result that he has informally proved. (iv) In 1931, Gödel claimed, but didn't show, that there is in fact a formal derivation of this formal arithmetic sentence Th within the formal theory P itself. (v) Hilbert and Bernays later showed in considerable detail how to do the derivation within the formal system P In other words, in the utterly standard textbook sense of 'formal proof', they showed how to give a formal proof of Th in P. (Well strictly, within variants of P, but the differing details don't matter here). No odd or unusual sense of "formal proof" that needs special explanation is involved.
From: Patricia Shanahan on 12 Sep 2006 19:34 Charlie-Boo wrote: > Alec McKenzie wrote: > >> In which case you must have meant to say "A formal proof that in >> every programming language there is a program that outputs >> itself". >> >> It seems clear to me that that cannot be true > > Why? Consider, for example, an XML-based Turing Machine description language in which the tape alphabet is limited to {'0','1',' '}. No program's source code can appear on the tape, because every XML document contains '<' etc., yet the language is Turing-complete. Patricia
From: Charlie-Boo on 12 Sep 2006 20:37 george wrote: > Rupert wrote: > > What's the merit in being completely formal, for any branch of > > mathematics? Surely it's enough to convince ourselves that we could > > formalize it. > > The question is surely not so much about the merits > of that approach as the POSSIBLITY. People are not > computers. People in general just don't communicate > in a "completely formal" way. But that does NOT change > the fact that MATH *is* BY DEFINITION *completely* formal; > that is what MAKES it math. And we can't communicate Math without being formal, can we? If Math = Formal, then what does it mean to be formal? C-B That's george, always hot on the trail of a new scoop. Is physics formal?
From: Charlie-Boo on 12 Sep 2006 20:42
Chris Menzel wrote: > On 10 Sep 2006 14:29:13 -0700, Peter_Smith <ps218(a)cam.ac.uk> said: > > > > Chris Menzel wrote: > > > >> Can that proof be found in their Grundlagen der Mathematik? If so, do > >> you happen to know which volume? > > > > Vol2, pp. 283-340. > > Thanks. I'm do impressed! I want you to write back and tell us all exactly what it says and just what it means, 'k? I think it's also in Gruntlonger dis Mathemydik Vol. 69 i. 812 |