[FOM] First Order Logic

[Cris Perdue]

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.
>

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.


>
> 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.html>