[FOM] First Order Logic

[Harvey Friedman]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130825/899a8216/attachment.html>