[FOM] uniqueness of FOL

Noah David Schweber schweber at berkeley.edu
Sun Sep 8 15:32:10 EDT 2013


>   Not everyone loves Compactness.   Frankly, its acceptability seems
predicated
>on all the "nice theorems" it makes available.  However, consider this
interpretation:
>All infinite information can be reduced to some finite amount of
information with no
>loss at all.  <-- This interpretation makes compactness seem unacceptable
(of course,
>many logicians will squawk at this, since it would deprive them of plenty
of adorable
>theorems).

Personally, I'd squawk at that interpretation because it's wrong.

Let p_n be the first order sentence asserting "there exist at least n
distinct objects." No finite subset of P={p_n: n in N} has the same
consequences as P. Compactness *definitely does not* assert that we can
pass from infinite information to finite information "with no loss at all."

What it does assert is that, if I have a blob I of infinite information,
and some specific consequence p of I, then I can be reduced to some finite
amount of information F which, while losing plenty of information, doesn't
lose p. There's a quantifier order issue here: the statement

"given any infinite theory T and any consequence p, there is a finite
subtheory S_p of T such that p is a consequence of S"

is not the same as the statement

"given any infinite theory T, there is a finite subtheory S of T such that
any consequence of T is a consequence of S."

The former is the (slightly vague) statement of the compactness theorem;
the latter is nonsense. They should not be conflated.

As to acceptability, I can't speak for others, but I find compactness to be
a necessary property for a logic to have in order to be foundationally
interesting: to me, "proofs" have to be finite objects to deserve the name.


On Sun, Sep 8, 2013 at 8:53 AM, Charlie <silver_1 at mindspring.com> wrote:

>    Not everyone loves Compactness.   Frankly, its acceptability seems
> predicated
> on all the "nice theorems" it makes available.  However, consider this
> interpretation:
> All infinite information can be reduced to some finite amount of
> information with no
> loss at all.  <-- This interpretation makes compactness seem unacceptable
> (of course,
> many logicians will squawk at this, since it would deprive them of plenty
> of adorable
> theorems).
>
> On Sep 5, 2013, at 8:09 PM, Noah David Schweber <schweber at berkeley.edu>
> wrote:
>
> (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
>>
>
> _______________________________________________
> 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/20130908/aded3555/attachment-0001.html>


More information about the FOM mailing list