Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Peter_Smith on 12 Sep 2006 16:15 george wrote: > MATH *is* BY DEFINITION *completely* formal; > that is what MAKES it math. george also wrote: > 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. One contrast we might be interested in is fully formalized mathematics (presented in a formalized language, with the deductions conducted within some formalized deductive framework -- conforming to the Hilbertian ideal) versus "common-or-garden" mathematics of the kind you find in typical text books. Now in terms of *that* contrast, it is quite uncontroversial that lots of mathematics isn't fully formalized, and equally quite uncontroversial that e.g. Gödel's paper is an exercise in non-formalized mathmetics (it is *about* some fully formalized mathematics, but it discusses it in a not fully formalized way). Perhaps the more informal mathematics in some sense aspires to the status of the fully formalized, but most mathematics plainly isn't formalized as it stands Now if you want to use "completely formal" in some sense that covers both fully formalized mathematics and common-or-garden mathematical argument, then you owe us an account of what you mean. Perhaps the idea is that all mathematics *could* be made fully formal if we put in the effort? (Though it is far from clear either why that should be so.) But thinking about the rights and wrongs of that view is running ahead of ourselves. The question is: what could it mean to say that all mathematics is *completely* formal just in virtue of being mathematics. As I say, it is evident that it isn't all fully formalized as it stands -- so what is being claimed???
From: george on 12 Sep 2006 16:20 > Alec McKenzie wrote [wrongly]: > > 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 C-B asks, > Why? Because there are a lot of simple easy-to-define programming languages in which you OBVIOUSLY can't do it, that's why. SOME programming languages are LAME. But despite being right about that, Alec is still wrong in general; you obviously didn't mean "every" programming language; you meant every REASONABLY rich programming language. By analogy, not all recursive 1st-order theories are subject to Godelian incompleteness. But all the adequately powerful ones are.
From: Charlie-Boo on 12 Sep 2006 16:38 george wrote: > 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. Yes! Have you ever seen anything as short as the CBL proof of Rosser 1936? "If an axiomatic system is decidable and consistent, then its refutable sentences coincide with its unprovable sentences, but the former set is r.e while the latter is not." [CBL, 2006] > The acutal problem is that that doesn't initially > appear > to be a computer science result: that is a number theory result. Ixnay. The Theory of Computation is a branch of CS. A set is enumerable by a Turing Machine iff it is representable in Peano Arithmetic. Godel's and Turing's results are related - although nobody was able to show exactly how when I asked. I asked what the relationship is between Godel 1931 and Turing 1937 because, to answer this question, you must formalize both of them. And since it seems that nobody has even done that (without using CBL), that could be tested by seeing if anyone can say the exact relationship. The exact relationship is that each is a CBL theorem that uses different sets of assumptions and rules being applied. Godel's 1st.based on soundness: -{ ~PR/TW , PR=>TW, TW=>PR } 1, - ~P/P Axiom (all Incompleteness proofs begin with this axiom.) 2. -{ ~P/P } Notational change 3. -{ ~PR/PR } SUB 2: The set of unprovable sentences is not representable. 4. -{ ~PR/TW , PR=TW } SUB 3 5. -{ ~PR/TW , PR=>TW , TW=>PR } DEF 4 If unprovability is expressible, then the system is not both sound and complete. qed We can go into further detail: 6. ~PR/TW + PR=>TW => -TW=>PR If unprovability is expressible, then if sound the system is not complete. 7. ~PR/TW + PR=>TW => TW(M) + ~PR(M) If unprovability is expressible, then if sound there is a sentence that is true and unprovable. > 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, Well yes, that would do. As it turns out, axioms are what is needed. I didn't make it come out that way. That's just the way it is. The use of axioms and rules of inferences pervades formal Computer Science. The primitive relation is expressed by P=Q(M) where P and Q are relations and M is an individual element of the universal set, expressed as M#P/Q in CBL because of variations that are needed such as P/Q for (eM)M#P/Q and P for P/YES which is P is r.e. > where the things in the universe are algorithms instead of sets. > Or where algorithms operate on strings instead of sets. Wait a minute. If algorithm replaces set, then when you say that algorithms operate on strings, you are saying that sets operate on strings. But sets don't operate on things - functions do. Set just set there - I mean, sit there. > I guess > strings would replace sets as the foundation, That's PA. > and then you could > represent algorithms by strings. Fancy that! > 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 No. {x|~(xex)} is not a set. (Its formalization in CBL shows this.) > (it's just that sometimes it gets cumbersome, or you have to stop > short of your own total universe). All of that is represented formally in CBL. Basically, 1. Computer Science should be formalized. 2. No published paper has formalized any of it. (Definitions alone do not a formalization make.) 3. CBL formalizes almost all of Computer Science. In particular, Program Synthesis, Theory of Computation, Recursion Theory and Incompleteness in Logic are all axiomatized: Program Synthesis: ADD(I,J,x)* + MUL(I, J,x)* Theory of Computation: YIT(I,J,K)* + TRUE(x) + - ~YES(x,x) [Kleene, Peano, Turing] Recursion Theory: M#f(I) => s11(M,N)#f(N) + s11(I,J) + f(I,J) => f(I,I) Incompleteness in Logic: -~P/P (The Rules of Inference are the 8 rules that I describe in my ARXIV paper.) Then note the 3 levels of Computer Science displayed here: 1. Incompleteness in Logic: What properties of a formal system are compatible? 2. Program Synthesis & Theory of Computation: What relations are representable? 3. Recursion Theory: What relations have representations that have certain properties? C-B
From: Charlie-Boo on 12 Sep 2006 17:33 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. 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.) You're going to have to define "formal proof" here. Can you present A-F as I listed? Surely if something is formally proven, then there is a formal representation of the theorem, a way of generating proofs, a demonstration that the representation is generated, etc. Are you suspicious of axiomatic systems that prove only one theorem? C-B
From: Charlie-Boo on 12 Sep 2006 17:37
Rupert wrote: > Charlie-Boo wrote: > > Do we all agree that Computer Science definitely should be formalized? > > > > 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. Why develop mathematics? Why have people axiomatized branches of mathematics? Is it better to have a single representation for a theorem rather than many equivalent representations? C-B |