From: rz@mips.complang.tuwien.ac.at (Richard Zach)
Subject: Re: Logic and Mathematicians (quite long)
Reply-To: zach@csdec1.tuwien.ac.at
Organization: Technische Universit"at Wien
Distribution: sci.math
Date: Sun, 15 Nov 1992 15:04:08 GMT

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