Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 15 Sep 2006 13:28 abo wrote: > Charlie-Boo wrote: > > abo wrote: > > > Does *your* system only have a small number of > > > intuitively obvous axioms? If so, what are they? > > > > The first few for each branch of Computer Science are: > > > > Program Synthesis: ADD(I,J,X)*, MUL(I,J,X)*, LT(I,J)* > > Theory of Computation: YIT(I,J,K)*, TRUE(x), LT(x,I)* > > Recursion Theory: M#f(I)=>s11(M,N)#f(N), s11(I,J) > > Incompleteness in Logic: -~P/P > > "First few"? Sorry, I would need a complete list. I would also need > either an explanation of what the terms mean or an explanation of the > axioms. As I said, please pick a branch. Incompleteness in Logic is very simple yet very powerful. Resursion Theory is more complex but also powerful. Theory of Computation is simple and shows how simple the popular "axioms" (actually theorems) really are and what all sorts of concepts from Logic and Foundations of Mathematics really mean. Program Synthesis is simple and shows how published efforts are so way off the mark. > I'd be more interested if you had claimed that > you had managed to reduce Godel's First Theorem down to a formal proof > with 1000 steps than with 10. WHAT?? Yikes! When formalized, almost all Incompleteness in Logic theorems are just a little bit of simple logic applied to a particular system's ability to represent relations. And the cool thing is, how they represent relations varies widely and is very different from the logic applied to them. There is no real general way to explain how they all represent relations - each is different. As a result, it is natural to make that a separate problem and use the results as axioms to which we apply the logic. For example, all of the reasoning used by Godel in his 1st. Incompleteness Theorem - more powerful version based on w-consistency - up to the 45th recursive relation/function is there only to establish the 45th. one. All of the reasoning past that uses only this single fact. Similarly, Turing's proof of the unsolvability of the Halting Problem takes a lot of effort to establish there is a Universal Turing Machine. But after that we use only that single fact plus simple logic. Since the two processes used by Godel and Turing to establish these first parts of their proofs are so qualitatively different, there is no simple common set of principles to accomplish both. So we formalize Godel's 45th recursive relation/function and the existance of a UTM as axioms. Then only simple logic is needed to prove each of the complete theorems. And this same logic creates other theorems as well. That is what I mean by formalizing Computer Science. C-B
From: Charlie-Boo on 15 Sep 2006 13:40 ¬a\/b wrote: > On 14 Sep 2006 12:38:03 -0700, george wrote: > >Charlie-Boo wrote: > >> You have to tell in advance an exact algorithm that creates every > >> proof. > >That this is trivial is PRECISELY what Godel's proof proves. > >1st-order consequence is recursively enumerable. > >There is an algorithm that (your choice) recursively enumerates > >proofs (there are only a finite number of proofs of length n, > > false Right. If anything, it shows there is NO proof of certain true sentences, and then there is no proof nor refutation. Yes, it is easy to generate theorems given Axioms and Rules of Inference. That's the whole idea behind the axiomatic method. That is not due to Godel. But to develop those Axioms and Rules is the hard part. A: "Can you prove X and Y?" B: "Yes!" A: "Why don't you prove X then?" B: "It's too trivial." A: "Why don't you prove Y then?" B: "It's too complex to explain." C-B
From: abo on 15 Sep 2006 13:48 Charlie-Boo wrote: > abo wrote: > > Charlie-Boo wrote: > > > abo wrote: > > > > Does *your* system only have a small number of > > > > intuitively obvous axioms? If so, what are they? > > > > > > The first few for each branch of Computer Science are: > > > > > > Program Synthesis: ADD(I,J,X)*, MUL(I,J,X)*, LT(I,J)* > > > Theory of Computation: YIT(I,J,K)*, TRUE(x), LT(x,I)* > > > Recursion Theory: M#f(I)=>s11(M,N)#f(N), s11(I,J) > > > Incompleteness in Logic: -~P/P > > > > "First few"? Sorry, I would need a complete list. I would also need > > either an explanation of what the terms mean or an explanation of the > > axioms. > > As I said, please pick a branch. Incompleteness in Logic is very > simple yet very powerful. Resursion Theory is more complex but also > powerful. Theory of Computation is simple and shows how simple the > popular "axioms" (actually theorems) really are and what all sorts of > concepts from Logic and Foundations of Mathematics really mean. > Program Synthesis is simple and shows how published efforts are so way > off the mark. I'm interested in the axioms you need to prove Godel's first Incompleteness Theorem (in 10 steps). Please include the statement of the Theorem in your system, as well as an explanation of any idiosyncratic symbolism. > > > I'd be more interested if you had claimed that > > you had managed to reduce Godel's First Theorem down to a formal proof > > with 1000 steps than with 10. > > WHAT?? Yikes! > > When formalized, almost all Incompleteness in Logic theorems are just a > little bit of simple logic applied to a particular system's ability to > represent relations. And the cool thing is, how they represent > relations varies widely and is very different from the logic applied to > them. There is no real general way to explain how they all represent > relations - each is different. As a result, it is natural to make that > a separate problem and use the results as axioms to which we apply the > logic. > > For example, all of the reasoning used by Godel in his 1st. > Incompleteness Theorem - more powerful version based on w-consistency - > up to the 45th recursive relation/function is there only to establish > the 45th. one. All of the reasoning past that uses only this single > fact. > > Similarly, Turing's proof of the unsolvability of the Halting Problem > takes a lot of effort to establish there is a Universal Turing Machine. > But after that we use only that single fact plus simple logic. > > Since the two processes used by Godel and Turing to establish these > first parts of their proofs are so qualitatively different, there is no > simple common set of principles to accomplish both. So we formalize > Godel's 45th recursive relation/function and the existance of a UTM as > axioms. I thought your claim was that your axioms are "intuitively obvious".
From: Jan Burse on 15 Sep 2006 15:05 For a start, try: Thompson, S.: Type Theory and Functional Programming, Addison-Wesley Publishing Company, 1991 He gives a definition of quicksort and then proofs its termination and correctness. From this follows that one can in theory also do programm synthesis: Just generate programms and pick those that you proofed termination and correctness. But there are some interesting approaches in inductive logic programming to do synthesis. Try googling the terms "machine learning" and "inductive logic programming". Bye Charlie-Boo wrote: > 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: Steven Zenith on 16 Sep 2006 04:26
Charlie-Boo wrote: .... > Sorry, but I seriously doubt that you can. Feel free to prove me > wrong. Read the literature I have referred to - which is readily available. With respect, Steven |