How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent (EASY PROOF)
in [Logic]
|
From: Aatu Koskensilta on 7 Jul 2010 13:46 Nam Nguyen <namducnguyen(a)shaw.ca> writes: > Hopefully by now you'd understand why in the other thread I asked why > in debates you've tended to: > >> think you're infallible and above the rigorousness of mathematical >> reasoning? No. Why do you think I think I'm infallible and "above the rigorousness of mathematical reasoning"? -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Nam Nguyen on 8 Jul 2010 02:10
David Libert wrote: > 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. I do appreciate what you've said in this paragraph. All I've been asking others here is just a firm confirmation of such: we can't prove consistency by the most rigorous regime of proof in FOL, namely rules of inference and axioms. Once that is confirmed then I'd be able to expand my certain exposition(s) further. But no one up to now has "formally" confirmed such matter (and most of the time some of them actually went on the "attack" rather than dwelling deep into analysis of the issue, iirc). > > 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). I believe I understood and understand that. The key thing though I think they ignored (perhaps unintentionally, perhaps unintentionally) is that my motivation has been examining the possible _incompatibilities_ between the most rigorous method (syntactical inference by the rules) and the most "liberal" method, semantics interpretation. If we can identify these incompatibilities of different methods of reasoning then we'd know the strength and weaknesses of mathematical reasoning which is to Shoenfield is method oriented. Then I think we'd be in a better position to improve FOL reasoning in order to cope with a) existing problems or b) the never ending demand to use mathematics as a means to express sciences. > > 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. My aim isn't meant to persuade people to ignore such "feeling". FWIW, I too am using ZFC many times to have some intuitions into some "pet projects" of my own (such as formalizing some biological concepts). The point though is I've been arguing for a formal codification of what is impossible to know. Instead of presenting a clear cut reason why such "reverse" codification be impossible, others somehow just ignored my invitation to sincerely give such codification a fair and impartial consideration, to say the least. > > 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. I _tend_ to believe Q, PA, ZF(C) be consistent. But if Quinne himself could be wrong about ML, then from the reasoning point of view there's always such a dangling sword in the form of "F /\ ~F" that *potentially* could still be there. I believe we have to balance between intuition and rigid logic. If we discard the former it's difficult to do mathematics, if we ignore the later, we could send spaceships off orbits, manufacture medication with severe side effects, alter DNA sequences with unintended and unimaginable consequences. So to speak, intuition and logic have to "dance" together, imho. > 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? We have to assume we know something to move on and I'm OK with that. And it's not unusual for a textbook to gloss over or assume something, from what limited reading I've had. But if we _borrow_ a knowledge then we have to realize it's a borrowed knowledge. And I'd think the more impartial on what we feel we be entitled to know vs what we're only endowed to know, the better we can improve how we conduct mathematical reasoning. > > 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. I beg to disagree. Formal proofs apply to non-logical theorems as well. > > But you are just changing our claims to something we never meant. Again, I'd disagree here. What I think others have overlooked is FOL reasoning actually condones more that one way to "prove" knowledge: a rigorous way and an intuitional way. And what I've been saying that we should view the situation in a high level bird-eye view so that we know what-is-what, so to speak. And I think it's meant to be that way, the way the late President Reagan said in "Trust but Verify": we trust our intuition but if necessary we'll verify that with the rigorousness proofs through rules of inference. If for whatever the reason we couldn't the verification then the trusted is always an un-verified hence a guarded trust only. Naturally. *** And that's just my high-level of the situation. In details I do have a few technical reasons that would reveal unsettling reasons why the compatibility between intuition and rigor of syntactical proof is very much questionable. But due to the time constraint, let me defer presenting the reasons in the next post(s). -- ---------------------------------------------------- There is no remainder in the mathematics of infinity. NYOGEN SENZAKI ---------------------------------------------------- |