[FOM] First Order Logic

[Colin McLarty]

I spent a lot of time thinking about this, originally in a very different
context than Harvey.  I want to entirely agree with his statements:  "For
any of the usual classical foundational purposes, you need to be able to
get down to finite representations that are completely non problematic.... 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. "

Colin



On Sun, Aug 25, 2013 at 3: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/20130826/7e85a2af/attachment.html>