From: MoeBlee on
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
MoeBlee wrote:

> A system of theory

'of' should be 'or'.

MoeBlee


From: kleptomaniac666_ on
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
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
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