[FOM] uniqueness of FOL

[Noah David Schweber]

(Apologies if this is a duplicate; I had some trouble trying to send this
the first time.)

I actually think we might be closer to formulating (and proving!) the
unique role of first-order logic than Prof. Friedman indicates.

Lindstrom proved (1969;
http://onlinelibrary.wiley.com/doi/10.1111/j.1755-2567.1969.tb00356.x/abstract;jsessionid=899FEBB4283B1F501009D02212BEC7C4.d01t03)
that first-order logic is the maximal "regular logic" satisfying

(i) both Downward Lowenheim-Skolem and Compactness;

(ii) both Downward Lowenheim-Skolem and Recursive Enumerability.

If we take "usable" to mean "proofs are finite and verifiable," then this
is almost the desired result; the only issue is the role that the downward
Lowenheim-Skolem property plays.

Personally, I also take the Lowenheim-Skolem property as a requirement of a
usable logic; but I understand that the argument there is slightly weaker.

(Some papers by Shelah might be helpful for visualizing compact logics
stronger than FOL; see, e.g.,
http://shelah.logic.at/files/375.ps,www.jstor.org/stable/1997362, or
http://link.springer.com/article/10.1007%2FBF02011631)

On the other hand, Lindstrom's Theorem seems to me a perfect formalization
of the following:

(*) First-order logic is the strongest usable logic for studying countable
structures.

(Maybe one might argue that the statement above should be "a strongest,"
not "the strongest;" but I tend to feel that logics not containing
first-order logic are automatically of less interest from the point of view
of logic-for-foundations.)

Don't get me wrong; I love second-order, infinitary, and other weird
logics. But I wouldn't view any of these as "usable" unless they are
interpreted in such a way as to be just (many-sorted) FOL.


On Wed, Sep 4, 2013 at 9:09 PM, <meskew at math.uci.edu> wrote:

> In a message dated August 25, 2013, Harvey Friedman wrote the following:
>
> "For any of the usual classical foundational purposes, you need to be able
> to get down to finite representations that are completely non
> problematic....
>
> "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."
>
> I would be interested to hear Dr. Friedman or others elaborate on why it
> appears that FOL is uniquely suited for classical foundational purposes.
> I agree that it is well-suited, and that several other logics are not as
> well-suited because they don't "get down to finite representations that
> are completely non-problematic."  But what is the evidence that FOL is
> uniquely suited for these purposes?  As Dr. Friedman said, we cannot
> firmly establish this at present.  But if this thesis is "apparent," is
> the evidence of an empirical nature, an intuitive nature, a philosophical
> nature, or does it take the form of theorems about logics in general that
> seem to support this broad thesis?
>
> Thanks,
> Monroe
>
> _______________________________________________
> 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/20130905/9de547ca/attachment.html>