Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Alec McKenzie on 10 Sep 2006 04:36 "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > 3. Recursion Theory: A formal proof that there is a program that > > > outputs itself... > > > > I have in my possession a program that outputs itself. Therefore > > there *is* such a program. Are you asking for a better proof > > than that? > > 1. That doesn't prove the theorem, which must apply to all languages. > It only says it can be done in that language. 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, so there can be no proof of it, formal or not. -- Alec McKenzie usenet@<surname>.me.uk
From: george on 10 Sep 2006 14:40 Peter_Smith wrote: > Charlie-Boo wrote: > > 4. Incompleteness in Logic: A formal derivation of Godel's > > Incompleteness theorems > > Well, we know that once the Hilbert-Bernays derivability conditions are > in place, there are easy formal derivation of Con_T --> not-Prov(#G_T), > using # for "the Gödel number of ...). > > And starting with Hilbert-Bernays there are textbook outlines of formal > proofs that the derivability conditions hold for theories with Sigma_1 > induction. See e.g. Boolos's book. > > That looks like a formal derivation to me. What more do you want?? This is an odd way of putting it. Godel's original proof was a formal derivation. Presumably he just wants it translated from the PM that Godel had it in, into the 1st-order PA that we use today. But it doesn't have to be translated directly. There are lots of newer better ways to prove all that. The acutal problem is that that doesn't initially appear to be a computer science result: that is a number theory result. It is derived from axioms purporting to describe the arithmetic of the natural numbers. Clearly, what C-B wants instead is for someone to present a set of basic axioms defining computer science, where the things in the universe are algorithms instead of sets. Or where algorithms operate on strings instead of sets. I guess strings would replace sets as the foundation, and then you could represent algorithms by strings. That at least seems slightly more natural and computational than representing them by sets. But it is unnecessary; you Really Can represent EVERYthing by sets (it's just that sometimes it gets cumbersome, or you have to stop short of your own total universe).
From: Peter_Smith on 10 Sep 2006 14:55 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. 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. (Gödel and Bernays discussed how to do it on a transatlantic vogage. Kreisel has apparently said that Gödel *dictated* the proof to Bernays.)
From: Chris Menzel on 10 Sep 2006 16:11 On 10 Sep 2006 11:55:26 -0700, Peter_Smith <ps218(a)cam.ac.uk> said: > 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. 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. The first formal > proof was given by Hilbert and Bernays some years later. Can that proof be found in their Grundlagen der Mathematik? If so, do you happen to know which volume?
From: Peter_Smith on 10 Sep 2006 17:29
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. |