From: MoeBlee on 3 Dec 2007 12:24 On Dec 2, 4:54 am, "LordBeotian" <pokips...(a)yahoo.it> wrote: > The point was: does every > reasoning have to be formalizable in order to be a "reasoning"? Do there > exist rules of reasoning that we follow even when we are not conscient of > them? In this context a relevant "formalization" of reasonings should be > complete, I think, otherwise evrything is trivially formalizable by an "ad > hoc" incomplete set of rules. You can advocate such a thesis, but perhaps you should consider doing it with terminology that does not so markedly depart from the ordinary. A system of theory is formal or not depending on whether it has a recursive axiomatization (and recursive rules of inference), and not depending on whether the system or theory proves every formula that is entailed by its rules and axioms. MoeBlee
From: MoeBlee on 3 Dec 2007 12:26 MoeBlee wrote: > A system of theory 'of' should be 'or'. MoeBlee
From: kleptomaniac666_ on 3 Dec 2007 19:00 On Nov 30, 4:46 pm, george <gree...(a)cs.unc.edu> wrote: > For a long time I did not know (after FLT was proved) whether > FLT followed from PA or not. It turns out it was proved long ago that > it > doesn't. But the fact that that proof got as much acceptance as it > got > withOUT it being clear what axioms it was being proved from > IS ENTIRELY A BAD thing. I don't think it has been proved that FLT is independent from the axioms of PA, if that's what you mean. That would be quite some result. Do you mean that it has been shown that the proof of FLT as given by Wiles cannot be formalised in PA? That would not be surprising as the proof uses a lot of analysis of modular functions.
From: george on 4 Dec 2007 19:59 On Dec 3, 7:00 pm, kleptomaniac6...(a)hotmail.com wrote: > I don't think it has been proved that FLT is independent from the > axioms of PA, if that's what you mean. I do. It definitely has. It is actually an old result, like over 40 years. [27] Shepherdson, John C., A non-standard model for a free variable fragment of number theory, Bulletin de l'Academie Polonaise des Sciences. Serie des Sciences Mathematiques, Astronomiques et Physiques, 12, 1964, 79-86. > That would be quite some result. > Do you mean that it has been shown that the proof of FLT as > given by Wiles cannot be formalised in PA? Well, indirectly. It used to be in vogue to construct nonstandard models of PA. Back when it was (in the early '60s), Shepherdson constructed one in which FLT failed for the *first*/simplest case (cubic). This doesn't have any direct relevance to the TRW proof, but it does imply independence from PA. I'm almost sure (though my whole point is, this hasn't been made *clearly* explicit) it's not independent of ZFC.
From: tchow on 4 Dec 2007 20:21
In article <312d0bac-a5b0-4b01-bcdb-5f71252178cf(a)w28g2000hsf.googlegroups.com>, george <greeneg(a)cs.unc.edu> wrote: >On Dec 3, 7:00 pm, kleptomaniac6...(a)hotmail.com wrote: >> I don't think it has been proved that FLT is independent from the >> axioms of PA, if that's what you mean. > >I do. It definitely has. It is actually an old result, like over 40 >years. No, Shepherdson isn't studying PA in that paper. It is still open whether FLT is independent of PA. -- Tim Chow tchow-at-alum-dot-mit-dot-edu The range of our projectiles---even ... the artillery---however great, will never exceed four of those miles of which as many thousand separate us from the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences |