home *** CD-ROM | disk | FTP | other *** search
- Newsgroups: sci.math
- Path: sparky!uunet!convex!darwin.sura.net!paladin.american.edu!news.univie.ac.at!email!mips.complang.tuwien.ac.at!rz
- From: rz@mips.complang.tuwien.ac.at (Richard Zach)
- Subject: Re: Logic and Mathematicians (quite long)
- Message-ID: <1992Nov15.150408.18663@email.tuwien.ac.at>
- Sender: news@email.tuwien.ac.at
- Nntp-Posting-Host: mips.complang.tuwien.ac.at
- Reply-To: zach@csdec1.tuwien.ac.at
- Organization: Technische Universit"at Wien
- References: <1992Nov13.090126.7142@jarvis.csri.toronto.edu>
- Distribution: sci.math
- Date: Sun, 15 Nov 1992 15:04:08 GMT
- Lines: 157
-
- In article <1992Nov13.090126.7142@jarvis.csri.toronto.edu>, leemike@eecg.toronto.edu (Michael Lee) writes:
- |> re: zelany's reponse to zach@csdec1.tuwien.ac.at:
- |> note: `>' represents the statements of zach@csdec1.tuwien.ac.at
- |> `|' represents some of zelany's statements
- |>
- |> I'm working from zelany's posting (see above). Hence, if I have
- |> misinterpreted the originator of this thread, feel free to correct
- |> any errors.
-
- |> >Examples: G"odel's Incompleteness Theorems:
- |> >He INVENTED the concepts of undecidability of
- |> >a sentence in a theory and of incompleteness.
- |>
- |> In full, Godel's paper, `On Formally Undecidable Propositions
- |> of Principia Mathematica and Related Systens', dealt with the
- |> problem of consistency of a given set of axioms and the transformation
- |> rules of a given system, i.e., these axioms and the transformation
- |> rules do not lead to a theorem which is both true and false.
-
- My point was that that was what G"odel did only marginally
- deal with. What it REALLY is about, imho, is the arithmetization
- of formal systems--G"odel numbering--and, complementary to what he
- did in his dissertation, about the relation between truth and
- provablity in arithmetic: while his completeness theorem
- says that whatever is logically true is provable in prdeicate
- logic, his (first) incompleteness theorem says that there are
- true sentences of arithmetic which are not provable in a
- formal system of arithmetic. The unprovability of consistency
- is a corollary to that.
-
- [some background deleted]
-
- |> >The interesting sentence (from the logical, and
- |> >also from G"odels standpoint) is the FIRST
- |> >incompleteness theorem (Why else did G"odel
- |> >entitle his paper "On undeciadable propositions"?
- |> >If he were interested more in consistency,
- |> >he would have titled it "The Unprovability of
- |> >Consistency" or something).
- |>
- |> Your suggestion, i.e., the latter title would of implied something Godel
- |> did not prove.
-
- Ok, ok: "The formal unprovability of consistence" or
- "Artithmetic does not prove itself consistent" or
- "Hilbert's Program fails" or whatever
-
- [description of consistency proofs deleted]
-
- |> Also, it wouldn't really solve the
- |> question at hand, inference rules more powerful than simple arithmetical
- |> calculus may lead us to doubt the consistency in the reasoning itself
- |> shifting our focus from the consistency of the axioms to the consistency of
- |> the reasoning.
-
- After all, maybe propositional logic is inconsistent :-)
-
- |> Whatever Godel's initial intent may be, his paper isn't
- |> trying to disprove axiomatic consistency but map-out the boundaries, its
- |> limits.
-
- Hm. Did I say this? I dont think I did.
-
- |> >From the mathematician's
- |> >viewpoint, the proof is trivial: A simple
- |> >diagonalization argument (in Kreisel's words).
- |>
- |> I'm not certain of your term `simple diagonalization.' From my perspective,
- |> I found the proof difficult to read and understand, I found nothing
- |> trivial about his proof. He completely arithmetized a formal calculus
- |> and established a one-to-one correspondence between the expressions
- |> of a calculus and a particular subset of integers.
-
- That was exactly my point: *G"odel numbering* is his big contribution
- there. As soon as you know how to do that (and I do not consider
- G"odel numbering a difficult concept per se), and you know
- what a diagonalization argument is, it is easy to obtain the
- result.
-
- |> [deli service analogy deleted]
-
- |> If the triviality of
- |> an idea is based on its most banal application then all of mathematics
- |> fall under the general heading of banality.
-
- Hm? All of mathematics is banal? or trivial?
- I dont get your point.
-
- |> >Yet, Hilbert (and others) were very much taken by
- |> >surprise. In a sense, incompleteness says:
- |> >"The concept of consistency is not important"
- |>
- |> Why wouldn't he be surprised?
- |> Godel demonstrated that his proposal
- |> on a finistic absolute proof for every deductive system is highly
- |> unlikey. Godel, also, showed that inifinite bits of true arithmetical
- |> expression can not be formally be deduced from a given set axioms by a
- |> closed set of inference rules. Yet still, the concept of consistency is
- |> possible along Hilbert's proposal; Godel proof doesn't logically conclude
- |> the impossibility of `consistency' nor does it directly address the
- |> importance, or the lack thereof, of `consistency'. Although, Godel
- |> didn't say Hilbert's proposal was impossible, he did flesh out its
- |> intractable characteristics.
-
- What else does the 2nd theorem say, if not that Hilbert's Program is
- impossible? Could you please explain to me how an elementary proof
- of consistency of PA would work in spite of the 2nd Incompleteness Thm?
-
- The importance of consistency was never questioned (sorry for being
- imprecise), but the importance of elementary proofs of consistency.
- And G"odel's results say that that is the wrong question to
- ask: after all, there is no answer.
-
- |> Suffice to say, consistency for a mathematician or a logician is important;
- |> what would be the point, if it was otherwise?
-
- [stuff about V=L and CH deleted]
-
- |> >The undecidability of predicate logic from
- |> >Turing's work: The really important part of his
- |> >paper were the "Computable Numbers", not
- |> >the "Application to the Entscheidungsproblem".
- |> >And he MADE UP Turing machines etc. Again,
- |> >easy theorems, difficult concepts requiring
- |> >deep insight.
- |>
- |> |You can add Church and Kleene to the same list.
-
- |> I think you're talking of the first-order predicate logic, which was
- |> shown to be complete by Godel and then undecidable by Church and
- |> Turing by different methods.
-
- |> >Gentzen's sequent calculus: his invention. Totally
- |> >disconnected from anything that had been done before.
- |> >Required deep insight into the nature of logic
- |> >to come up with. The "problems", eg, Herbrand's
- |> >Theorem, were easy corollaries of the Hauptsatz,
- |> >which, in itself, was easy to prove. But how do
- |> >you come up with the Hauptsatz in the first place?
- |>
- |> How is Gentzen's work totaly disconnected from anything?
-
- In the sense that he came up with something new which, at
- least at first sight, does not have anything to do with
- what had been done before. He didnt solve an open problem.
- He made up the sequent clculus, then proved some things
- about it. It was as if someone came up with an abstruse
- algebraic structure, proved some theorems about it,
- and the sole motivation for why anyone should consider
- it is because you can do certain things with it which
- you can also do with other means.
-
- [questions deleted]
-
- --
- Richard Zach Technische Universitaet Wien
- [zach@csdec1.tuwien.ac.at] Abteilung fuer Formale Logik 185.2
-