How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent (EASY PROOF)
in [Math]
|
Prev: get cancer and die, musacunt
Next: deriving speed of light out of pure math as pseudosphere nested inside sphere Chapt 19 #215; ATOM TOTALITY
From: David Libert on 8 Jul 2010 00:25 Nam Nguyen (namducnguyen(a)shaw.ca) writes: > Aatu Koskensilta wrote: >> Nam Nguyen <namducnguyen(a)shaw.ca> writes: >> >>> MoeBlee wrote: >>> >>>> And, in that regard, I have said all along that there is no >>>> finitistic proof of the consistency of PA. >>> So you've agreed that there's no formal proof for PA's consistency and that >>> if you go by formal proof only then you don't have knowledge of PA's >>> consistency. >> >> There are many formal proofs of the consistency of PA. None of them are >> finitistic. > > So it doesn't seem you used the phrase "formal proof" in the standard > way that textbook (e.g. Shoenfield's) would use. In that standard > usage, a formal proof is a (finite) syntactical proof of a FOL formal > system theorem. > > Given that standard definition of "formal proof", would you agree with > my statement above that: > > >> there's no formal proof for PA's consistency and that if you go by > >> formal proof only then you don't have knowledge of PA's consistency. > > ? This discussion seems to me to be reducing to what people often call (in common language, not the technical logical sense), semantics, ie definitions of words. Namely what do we mean by "know" or "really know" or "formal proof" . My edition of Shoenfield is copyright 1967. All page numbers I reference below are for that edition. On page 4 Shoenfield defines the theorems of a formal system, namely the usual involving axioms and rules and conclusion. Earlier on this same page 4 he defines a formal system as havin axioms and rules of inference. This simply says axioms, with no further specification. On page 22 Shoenfield writes: "We can now define the class of formal systems which we are going to study. A first-order theory, or simply a thoery, is a formal stysten T such that i) the language of T us a first order language; ii) the axioms of T are the logical axioms of L(T) and certain further axioms, called the nonlogical axioms;" There is a iii) I omot about rules of inference. An important part of logic is to be able to have applied theories. If all we ever did with logic was pure logic, all we could talk avout is = and substitution instances of propostional logic on other predicates. And indeed, Shoenfield like any other logic book spends a lot of time discussing applied theories. So Shoenfield talked about theorems for formal theories, and later he spelled out these formal theories include nonlogical axioms. And this is what I have always understood to be the standard definition, not just Shoenfield but every text and every course I have seen. A formal proof is a sequence of statements with the conclusion at the end, every statement following from previous statements by a rule of inference, or being an axiom, an axiom being a logical axiom or a nonlogical axiom. If you think that formal proofs must only be in pure logic, and all you are telling us is pure logic does not prove Con(PA), all of us I am sure have known that for years. I do know that I have. For myself, and I think a reasonable reading of the pther people here, we never meant to be claiming that pure logic has a formal proof of Con(PA). Instead we regard Con(PA) as accepted by the normal canons of mathematics, and many of us, including me, feel that ZFC or ZF or whatever is one reasonable codification of that. We say we consider that we know Con(PA) as a mathematical statement by the normal standards of mathematical knowledge, and this fact itself can be illuminated by ZF |- Con(PA). And ZF provability is by a first order applied system, as Shoenfield discusses. In fact on page 239 he evens begins a description of ZF. So the technical work in logic defining what a proof is applies to this case. And so we do apply it. As is justified by Shoenfield's own words above. Anyway, if there is some problem with ZF being a formal system why does Shoenfield have a chapter on it? So you dispute our mathematical knowledge by saying know means really know, and relaly know means having a formal proof, and formal proof means over pure logic only with no nonlogical axioms. But you are just changing our claims to something we never meant. -- David Libert ah170(a)FreeNet.Carleton.CA |