Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Charlie-Boo on 12 Sep 2006 21:06 Peter_Smith wrote: > 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. Because they're trying to tell you one proof, not all proofs of a particular type. > Now in terms of *that* contrast, it is > quite uncontroversial that lots of mathematics isn't fully formalized, Is it good? Would it be good to reverse? > Perhaps the more informal mathematics in some sense aspires to > the status of the fully formalized, It is the ultimate solution - to translate it into a program to analyze. So every solution to every problem is a part of its solution. It is the composite of all solutions. > but most mathematics plainly isn't > formalized as it stands Yes, and none of Computer Science. > 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. To make a less formal argument is to show the analysis of some program where we cannot analyze all programs. > Perhaps the idea > is that all mathematics *could* be made fully formal if we put in the > effort? ALL = past? Past plus future? Possible? You need to first define mathematics. > (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??? Does "Mathematics" include the solutions to puzzles e.g. prove that you can't cover with dominoes a checkerboard with diagonally opposite corners missing? C-B
From: Charlie-Boo on 12 Sep 2006 22:05 george wrote: > > 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, How in the world can you define "programming language" then? I mean an r.e. set of expressions (programs) and a mapping from expression to set that is onto the set of r.e. sets. The difference between one programming language and another is syntactic not semantic. Let M#P/Q mean P=Q(M), M#P/Q* means Q(M) always halts, I J K = Inputs, X Y Z = Outputs, P/Q mean (eM)M#P/Q, YES(a,b) means TM a halts yes on input b, and -E mean E is false. Then we have: X # Y / YES = Programming Language Semantics I # X / YES = Program Analysis X # I / YES = Program Synthesis I # J / YES = Program Debugging - X / YES = Theory of Computation (e.g. Turing 1937) X / YES = TOC Positive - what can be computed X # X / YES = Create Self Outputting Programs = Recursion Theory - X / I = Paradoxes - ~P/P = Incompleteness in Logic (Yes, believe it or not, all Godel, Rosser, Turing, Smullyan et. al. incompleteness proofs end with a violation of CBL axiom - ~P/P.) C-B > 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 23:03 Peter_Smith wrote: > george wrote > > > Godel's original proof was a formal derivation. > > I wrote > > > 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. > > C-B wrote > > > You're going to have to define "formal proof" here. > > Why so? The situation is surely entirely clear and entirely well-known. Step D, An algorithm for generating formal statements such as A, has been studied in the form of axioms and rules of inference. But here we are doing all of A-F. We need to show that the theorem proven corresponds to a certain published theorem, what expressions in general mean, how it was proven, and how we know the system is sound. You can start with A, A formal statement of the theorem or result. C-B > (i) Gödel in 1931 showed that a certain sentence is not formally > derivable within the formal system P (a simplified version of the type > theory of Principia). (ii) His argument for this is a bit of ordinary > unformalized mathematical reasoning, rendered as it happens in German, > not within P. (iii) However, there isa sentence of P's formal language, > call it Th, which -- via coding -- expresses the result that he has > informally proved. (iv) In 1931, Gödel claimed, but didn't show, that > there is in fact a formal derivation of this formal arithmetic sentence > Th within the formal theory P itself. (v) Hilbert and Bernays later > showed in considerable detail how to do the derivation within the > formal system P In other words, in the utterly standard textbook sense > of 'formal proof', they showed how to give a formal proof of Th in P. > (Well strictly, within variants of P, but the differing details don't > matter here). No odd or unusual sense of "formal proof" that needs > special explanation is involved.
From: guenther vonKnakspot on 13 Sep 2006 02:09 Charly Boo Boo wrote: <snip yet another proof of his ignorance> > C-B You are joking, right Boo Boo?
From: Phil Carmody on 13 Sep 2006 02:49
Patricia Shanahan <pats(a)acm.org> writes: > Charlie-Boo wrote: > > Alec McKenzie wrote: > > > >> 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 > > Why? > > Consider, for example, an XML-based Turing Machine description language > in which the tape alphabet is limited to {'0','1',' '}. No program's > source code can appear on the tape, because every XML document contains > '<' etc., yet the language is Turing-complete. But that's simply a matter of encoding, they're information-theoretically equivalent. Something that outputs 100100011010010100001 or 010010000110100100100001 or the baudot equivalent, or... has, in my opinion, output 'Hi!'. If you have turing machine that can only output blank and mark, then it can never output zero using your logic, yet I presume that turing machines which had such an alphabet were used for arithmetic examples in your Computability 101 course without you batting an eyelid. Phil -- "Home taping is killing big business profits. We left this side blank so you can help." -- Dead Kennedys, written upon the B-side of tapes of /In God We Trust, Inc./. |