[FOM] First Order Logic

Thu Aug 29 11:23:31 EDT 2013

Harvey addressed simple type theory when he addressed second order
arithmetic: "not the fake notion [of second-order logic] used in so
called second order arithmetic, where it is simply a two sorted first
order theory".
In this particular FOM context, the various axiomatic type theories
are just syntactic sugar for many-sorted first-order theories, and
thus are in the same category as explicit first-order theories like
ZFC.

> Hopefully it is not merely pedantic to say this is overstating. Proofs in
> type theory (e.g. simple type theory) are also "definite finite objects
> that can be objectively tested for correctness"; and speaking of software
> proof assistants, type theory / higher-order logic has strong communities
> that formalize mathematics in type theory. First order logic does have a
> special cultural status, clearly.

On Wed, Aug 28, 2013 at 12:04 PM,  <fom-request at cs.nyu.edu> wrote:
> Send FOM mailing list submissions to
>         fom at cs.nyu.edu
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://www.cs.nyu.edu/mailman/listinfo/fom
> or, via email, send a message with subject or body 'help' to
>         fom-request at cs.nyu.edu
>
> You can reach the person managing the list at
>         fom-owner at cs.nyu.edu
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of FOM digest..."
>
>
> Today's Topics:
>
>    1. Re: First Order Logic (Cris Perdue)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 27 Aug 2013 09:01:30 -0700
> From: Cris Perdue <cris at perdues.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] First Order Logic
> Message-ID:
>         <CAOoe=WJMo3ic7MRd4VaCNOzwwAOEp-JaSMcJDCO3=3KKXMboFA at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Professor Friedman,
>
> (please see below)
>
>
> On Sun, Aug 25, 2013 at 12:59 PM, Harvey Friedman <hmflogic at gmail.com>wrote:
>
>> For any of the usual classical foundational purposes, you need to be able
>> to get down to finite representations that are completely non problematic.
>>
>> E.g., one normally uses ZFC, or fragments and extensions of ZFC, for
>> representing mathematical proofs (and of course sugared according to what
>> features of proofs one wants to represent).
>>
>> The first order form of such a T is important, because then a proof within
>> T is a definite finite object that can be objectively tested for
>> correctness, with no disagreements possible. (Of course, in practice, one
>> does not usually, but sometimes one has, an actual correct proof in the
>> appropriate sense. But that leads us into rather different issues
>> concerning proof assistants, etc.).
>>
>> Imagine the situation if one proposed a second order version of ZFC, in
>> the serious sense of second order here (not the fake notion used in so
>> called second order arithmetic, where it is simply a two sorted first order
>> theory). There would be widespread disagreement about whether a purported
>> proof within second order ZFC is correct or not. This directly stems from
>> the fact that it is not a first order formulation.
>>
>> Insisting on a first order formulation here is also fruitful - it forces
>> the disagreements to come to the surface and be focused on.
>>
>> Furthermore, first order logic is apparently the unique vehicle for such
>> foundational purposes. (I'm not talking about arbitrary interesting
>> foundational purposes). However, we still do not know quite how to
>> formulate this properly in order to establish that first order logic is in
>> fact the unique vehicle for such foundational purposes.
>>
>
>
>
>>
>> In summary, whereas it can be interesting and important to give second
>> order formulations of various theories, ultimately in each case you are
>> compelled to provide a clarifying first order associate.
>>
>> Harvey Friedman
>>
>>
>> On Sun, Aug 25, 2013 at 11:56 AM, Sam Sanders <sasander at cage.ugent.be>wrote:
>>
>>> Dear Carl,
>>>
>>> > Not everyone has been on same old conventional page as Tarski.  For
>>> example, [Barwise 1985] critiqued the first-order thesis as follows:
>>> >
>>> > "The reasons for the widespread, often uncritical acceptance of the
>>> first-order thesis are numerous. Partly it grew out of interest in and
>>> hopes for Hilbert's program. ... The first-order thesis ... confuses the
>>> subject matter of logic with one its tools. First-order language is just an
>>> artificial language structured to help investigate logic, much as a
>>> telescope is a tool constructed to help study heavenly bodies. From the
>>> perspective of the mathematics in the street, the first-order thesis is
>>> like the claim that astronomy is the study of the telescope."
>>>
>>> I believe I did not mention the "first-order thesis", but let me make it
>>> clear that I believe that (at the very least) we need second-order
>>> arithmetic
>>> to formalize mathematics.  Reverse Mathematics is a good example, though
>>> heavy on the coding sometimes;  Classical logic is used there.
>>>
>>> > In particular, Computer Science has requirements that go far beyond
>>> classical first-order logic. The domination of classical logic is coming to
>>> an end because practical real-world theories are pervasively inconsistent.
>>> >  Computer Science needs Inconsistency Robust mathematical foundations
>>> with the following characteristics:
>>> >  * Standard Boolean equivalences hold for conjunction, disjunction, and
>>> negation
>>> >  * Disjunctive Syllogism holds as well
>>> >  * Capability to reason about arguments for and against propositions
>>> >
>>> > Consequently, the range of acceptable CS solutions for Inconsistency
>>> Robust inference is actually quite narrow :-)
>>>
>>> Do people in applications really throw out classical (whatever order)
>>> logic and embrace paraconsistent logic as "the true way"?  Or do they just
>>> think/work classically and somehow
>>> manage to contain the inconsistent information, i.e. prevent it from
>>> doing damage?
>>>
>>> I have seen examples of the latter, but not the former in practice.
>>>  Chow similarly asked for a clear example (related to the ongoing saga
>>> mentioned), I believe.
>>>
>>> Best,
>>>
>>> Sam
>>>
>>>
>> _______________________________________________
>> 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/20130827/9f2535c6/attachment-0001.html>
>
> ------------------------------
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
> End of FOM Digest, Vol 128, Issue 25
> ************************************