[FOM] R: Re: Seeking sage advice on terminology

[Colin McLarty]

Thanks to everyone for a lot of helpful answers.   It has really helped and
forced me to think about the issue.    "Elementary proof" seems to me an
important idea but it is pretty ambiguous in usage now: maybe a proof
informally stated in terms of PA, which transparently could be put into in
PA.  But how informality or transparently?

With help from people here and on MathOverflow and from Kreisel's writings
 I have come to think of a elementary proof in number theory as a second
order argument using arithmetic comprehension, so you can see how to
formalize it in $ACA_0$.  That is more than i want to explain in the
expository paper I am writing now.    I am not sure what I will do.

Again, thanks.

Colin


On Wed, Aug 7, 2013 at 4:04 AM, iao271055 at libero.it <iao271055 at libero.it>wrote:

> Dear Colin,
>
> How about using the traditional distinction between elementary and
> non-elementary proofs of a mathematical assertion A? If by 'elementary
> proof of an assertion A belonging to the language of a mathematical theory
> T' we mean a proof of A carried out entirely within T, it seems to me that
> a proof of 'T |- A' is not elementary (in the above sense).  At present we
> only have a non-elementary proof of Fermat Last Theorem.
>
> Best wishes,
>
> Gianluigi Oliveri
>
>  ----Messaggio originale----
> Da: frode.bjordal at ifikk.uio.no
> Data: 3-ago-2013 12.39
> A: "Foundations of Mathematics"<fom at cs.nyu.edu>
> Ogg: Re: [FOM] Seeking sage advice on terminology
>
> I now write *thesis* for theses of the system and *theorem* for results
> about the system.
>
> Professor Dr. Frode Bjørdal
> Universitetet i Oslo Universidade Federal do Rio Grande do Norte
> quicumque vult hinc potest accedere ad paginam virtualem meam<http://www.hf.uio.no/ifikk/personer/vit/fbjordal/index.html>
>
>
> 2013/8/1 Nik Weaver <nweaver at math.wustl.edu>
>
>>
>> Colin,
>>
>> I'm writing a book on forcing right now and have a similar issue.
>> The terminological distinction I am using is "theorem" versus
>> "metatheorem".  Once that terminology is set up I don't find it
>> necessary to use different terms for proof of theorems and proofs
>> of metatheorems.
>>
>> If saying "FLT is a theorem (of PA)" and "PA |- FLT is a metatheorem
>> (of your metatheory)" doesn't solve your problem, perhaps you could
>> use the term "metaproof" for a proof in the metatheory.
>>
>> Nik
>>
>>  When I write about proofs of FLT I always have trouble finding a graceful
>>> terminology to distinguish proving FLT in PA versus proving in proof
>>> theory
>>> that PA |- FLT.
>>>
>>> I don't mean the conceptual distinction is difficult.  I mean I'd like
>>> a cleaner terminology for it so i don't keep using "proof" to mean two
>>> different things.  Maybe the literature I have been reading does have
>>> a solution but if so I have not absorbed it.
>>>
>> ______________________________**_________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/**listinfo/fom<http://www.cs.nyu.edu/mailman/listinfo/fom>
>>
>
>
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130809/32c287f3/attachment.html>