Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 9 Sep 2006 16:07 Do we all agree that Computer Science definitely should be formalized? While the definitions of common terms (e.g. recursively enumerable) are formal, the manipulations of these concepts (e.g. the derivation of proofs) is not. Can anybody show a single example of a formal derivation of a result from any branch of Computer Science? For example: 1. Program Synthesis: The creation of a computer program based on only its specifications. 2. The Theory of Computation: A formal derivation of Turing's proof of the unsolvability of the halting problem. 3. Recursion Theory: A formal proof that there is a program that outputs itself, or of the Fixed Point theorem or the Recursion theorem. 4. Incompleteness in Logic: A formal derivation of Godel's Incompleteness theorems or Rosser's improvement or Smullyan's Dual Form theorem. Any formalization would include: A. A formal statement of the theorem or result. B. The meaning of any such statement. C. How A corresponds to the statement of the theorem. D. An algorithm for generating formal statements such as A. E. A demonstration that D generates A. F. A demonstration that D generates only true statements. Curry-Howard, Manna/Waldinger, Boyer/Moore, Modal Logic, Prologue and TPTP all attempt to do this, but nobody has ever shown any examples of anything near A-F. Would we say that formalization is the ultimate goal of every branch of Computer Science? What problem is not enhanced when expressed formally? C-B
From: Alec McKenzie on 9 Sep 2006 16:23 "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? -- Alec McKenzie usenet@<surname>.me.uk
From: Peter_Smith on 9 Sep 2006 16:27 Charlie-Boo wrote: >Can anybody show a single example of a formal > derivation of a result from any branch of Computer Science? For > example: > 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??
From: Charlie-Boo on 9 Sep 2006 18:27 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 the CBPL2 programming language, the special variable A is equal to "W A" and W is the command to write a variable, so the program W A also outputs itself. But does that prove it is so of all programming languages? 2. Any single specific proof (such as a specific program to prove that something is true of one language) is vastly improved if we have a procedure to produce it and lots of other proofs automatically. Isn't that obvious? You haven't formalized a branch of Computer Science. These are at opposite ends of the spectrum and is described in A-F that is missing from your proof. C-B > -- > Alec McKenzie > usenet@<surname>.me.uk
From: Charlie-Boo on 9 Sep 2006 18:32
Peter_Smith wrote: > Charlie-Boo wrote: > > >Can anybody show a single example of a formal > > derivation of a result from any branch of Computer Science? For > > example: > > > 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 ...). It looks like you're talking aboiut Rosser's result, but that doesn't really matter here. > 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?? A to F: A. A formal statement of the theorem or result. B. The meaning of any such statement. C. How A corresponds to the statement of the theorem. D. An algorithm for generating formal statements such as A. E. A demonstration that D generates A. F. A demonstration that D generates only true statements. C-B |