Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 20 Sep 2006 20:12 george wrote: > > > Charlie-Boo wrote: > > > > You have to tell in advance an exact algorithm that creates every > > > > proof. > > I replied, > > > That this is trivial is PRECISELY what Godel's proof proves. > > CB, digging his hole deeper... > > Trivial? No man, it depends on what you're trying to formalize. > > NO, Charlie, Mr. Boo to you, thank you. > it cannot DEPEND on what we are trying to > formalize, because "what we are trying to formalize" is not > VARYING! But there's more than one thing we can formalize: Theory of Computation, Recursion Theory, etc. > WE KNOW what we are trying to formalize! YOU > SAID, > >*>*> an exact algorithm that creates every > >*>*> proof. > ^^^^^^^^^ > > So PROOF is what we are trying to formalize. Not all proofs are created equal. > And 1st-order proof-predicates are PRIMITIVE-recursive. > It is EASY to tell whether an alleged proof is one or isn't > one, But it's not so easy to create that formalism. But that is a red herring. If it's so easy, why hasn't anyone else done it? Why do you think it took me years to, if it's so easy? That begs the question. Has anyone shown a general method of formally generating the results from any branch of Computer Science? Not some result created by hand, but a system (e.g. axiomatic) that generated the results? If so, why doesn't anybody seem to be aware of it? C-B > at least it's easy compared with THE LENGTH of the > proof. Put another way, proofs can be long, but they CAN'T > be hard. You think Andrew Wiles' proof is easy?
From: Steven Zenith on 21 Sep 2006 03:45 Charlie-Boo wrote: > Steven Zenith wrote: > > > http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=65476 > > This is only an abstract. > > What is the theorem? > What is the formal representation of the theorem? > What is the sequence of steps (or at least the first few and the last > few) that construct the formal representation of the theorem? > I did give the answers to these questions. > I have given examples of CBL proofs. I continue to offer to present > here the formal derivation of any of the theorems that I have mentioned > and other related theorems that anyone wants: Godel 1931, Rosser 1936, > Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program Synthesis of > Number Theoretic functions. > > Why don't you? Because that is not my level of participation here. You made a claim and I pointed you to work that I believed countered the claim - you have not, to my satisfaction, acknowledged the information I provided. The derivations you are interested in do not seem to me to be particularly interesting from a practical point of view, though as examples that are case studies in CBL they are no doubt of interest. Why is it you have such a hard time acknowledging the work of others - and I am not referring to my part in any of it - which was minor compared to the people that established the formal basis of concurrency theory (Roscoe, Hoare, Milner). The work speaks for itself and directly contradicts your claim that CS has not been formalized in any part. With respect, Steven
From: Charlie-Boo on 21 Sep 2006 06:29 Steven Zenith wrote: > Charlie-Boo wrote: > > Steven Zenith wrote: > > > > > http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=65476 > > > > This is only an abstract. > > > > What is the theorem? > > What is the formal representation of the theorem? > > What is the sequence of steps (or at least the first few and the last > > few) that construct the formal representation of the theorem? > I did give the answers to these questions. I don't see anywhere that you say anything about "The formal representation of the theorem is . . . The formal derivation is . . ." Where did you give such specifics here? What are those formal representations? > > I have given examples of CBL proofs. I continue to offer to present > > here the formal derivation of any of the theorems that I have mentioned > > and other related theorems that anyone wants: Godel 1931, Rosser 1936, > > Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program Synthesis of > > Number Theoretic functions. > > > > Why don't you? > > Because that is not my level of participation here. But you have in fact participated in making the claim that formally generated results do exist. You simply have not given them. > You made a claim > and I pointed you to work that I believed countered the claim - you > have not, to my satisfaction, acknowledged the information I provided. The information that you have provided here does not include the result and its formal derivation, only references that have not been shown to contain any such formal representations. You could prove that these references contain such a result by telling us all what that result is. However you only say "It exists." rather than telling what the result is that you believe exists. What is there to acknowledge? > The derivations you are interested in do not seem to me to be > particularly interesting from a practical point of view, though as > examples that are case studies in CBL they are no doubt of interest. Why do you consider the results of Godel and Turing not interesting, when so many others have written so much about these results and have claimed that they are significant? Have they not done this? Are they wrong? > Why is it you have such a hard time acknowledging the work of others Because you will not give the result that I am supposed to acknowledge. You only state that "it exists". If I should acknowledge it, then why don't you give the result that I am supposed to acknowledge? How am I supposed to acknowledge a result if you will not state what that result is that I am supposed to acknowledge? You are yourself not acknowledging any results because you haven't given any. Why haven't you given any such results here? > and I am not referring to my part in any of it - which was minor > compared to the people that established the formal basis of concurrency > theory (Roscoe, Hoare, Milner). The work speaks for itself What result has been formalized that speaks for itself? What is the formal representation of that result and of its formal derivation? > directly contradicts your claim that CS has not been formalized in any > part. Then why don't you give it here? C-B > With respect, > Steven
From: Chris Menzel on 21 Sep 2006 10:17 On 20 Sep 2006 09:47:14 -0700, Charlie-Boo <shymathguy(a)gmail.com> said: > I have given examples of CBL proofs. I continue to offer to present > here the formal derivation of any of the theorems that I have > mentioned and other related theorems that anyone wants: Godel 1931, > Rosser 1936, Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program > Synthesis of Number Theoretic functions. Could you provide references to those proofs? I seem to have missed them. Thanks.
From: Charlie-Boo on 21 Sep 2006 15:06
Chris Menzel wrote: > On 20 Sep 2006 09:47:14 -0700, Charlie-Boo <shymathguy(a)gmail.com> said: > > I have given examples of CBL proofs. I continue to offer to present > > here the formal derivation of any of the theorems that I have > > mentioned and other related theorems that anyone wants: Godel 1931, > > Rosser 1936, Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program > > Synthesis of Number Theoretic functions. > > Could you provide references to those proofs? I seem to have missed > them. Thanks. I gave a reference to my ARXIV paper a little earlier (and I believe you and I have discussed it before, if I am not mistaken.) In any case, here is the on-line version again: http://www.arxiv.org/html/cs.lo/0003071 This contains CBL as of the year 2000, with the formalization of Program Synthesis (including the formal derivation of both Number Theoretic functions and Database Query Processing) and the Theory of Computation (including the formal derivation of Turing's proof of the undecidability of the Halting Problem and a number of related theorems.) Since then, CBL has been generalized from the base of the recursive functions to any base in general, including provable wffs (analogous to a Turing Machine that halts yes), which derives theorems from Incompleteness in Logic (Proof Theory.) I have posted a number of formal derivations from Incompleteness in Logic (including Godel's 1st Incompleteness Theorem based on soundness and an amazingly short proof of Rosser's 1936 extension) here, but they have yet to be included in a formal paper. That is why I offer to repost and explain those results here. There is also the application of CBL to the formalization of Recursion Theory, which I discussed earlier, and of course, as with all of CBL's applications, will provide further detail if there is interest. BTW These various branches of Computer Science (there are 11 altogether) are defined as follows in CBL: Program Synthesis: X # I / YES Recursion Theory: X # X / YES Theory of Computation: - X / YES Incompleteness in Logic: - ~P / P Each branch of Computer Science is really a "problem" to be solved, as formalized above. Each theorem is the solution of one special case of that general problem. The general problem is: Computer Science: X # Y / Z (This means to output, for every base, all expressions and what relation they represent, which is the general problem of Computer Science that begats all results.) If you'd like all of these results explained (again) in one coherent theory, then please start a new thread requesting that, and I will be glad to explain in further detail how it all ties together. Thanks for the interest. C-B PS Notice the stark contrast between the reticence of others to give Computer Science results (that purportedly exist) that are formally derived (without human intervention), and the ease at which we can exhibit results formally derived in CBL! |