FOM: Re: SOL confusion

[Harvey Friedman]

Reply to Shipman 1:01AM 90.10.00:

>Friedman:
>>> There cannot be a development of ordinary mathematics within SOL, which is
> sound for standard semantics, unless that development uses proper SOL
> axioms. This is precisely the same situation as with FOL, which also cannot
> formalize mathematics without proper FOL axioms.<<
>
>Shipman:
>    I think I see an important difference.  FOL requires both LOGICAL axioms
>(Frege's predicate calculus, shown to be complete by Godel) and MATHEMATICAL
>axioms (e.g. Peano's axioms for the integers or Zermelo's for sets) in order
>to develop mathematics.

At first glance, the "difference" does not exist. If you are going to make
up a deductive SOL for the purpose of smoothly formalizing mathematics, it
is going to have mathematical axioms also.

This doesn't mean that you cannot make good sense of your feelings about
this. But to get anywhere with this idea, you would have to draw some sort
of sharp distinction between mathematical and logical that is convincing.
E.g., you can't just say that anything in deductive SOL is automatically
logical and not mathematical.

>    For example, it is not enough, given an arithmetical theorem T (that is,
>a 1st-order statement constructed in the usual way from the quantifiers,
>connectives, = symbol, constants 0 and 1, and function symbols + and x) , to
>take the finite set of axioms {A1, A2, ...,An} used to prove T, note that "
>(A1&A2&...&An) --> T " is a validity of FOL because a deduction of it exists
>in the predicate calculus with no nonlogical axioms, and conclude that T
>follows "from logic alone".
>    In fact, even to interpret T as a theorem about the structure of integers
>[|N, 0, 1, +, x] is not straightforward because there is no categorical
>1st-order axiomatization for this structure.

Your last sentence is misleading and irrelevant. Using the concept of set,
one has the obvious suitably categorical treatment of the structure of
integers. In fact, this is something I recommend when formalizing
mathematics in set theory - that one proves various categoricity results
about the integers and real numbers, and then uses the axiom of infinity in
order to derive existence. The only difference between the deductive FOL
approach and the deductive SOL approach here is that one has semantic SOL
categoricity. But we are talking about deductive SOL, and so this
(semantic) categoricity is entirely irrelevant to the comparison.

>There is still no "best"
>deductive calculus for generating SOL-validities, but there are certainly
>deductive calculi (for example C2 in Manzano chapter II) whose axioms are
>clearly LOGICAL rather than MATHEMATICAL which are quite strong enough to do
>ordinary mathematics (in particular to prove any theorem PA can prove and
>much more).

I repeat: to get anywhere with this idea, you would have to draw some sort
of appropriate sharp distinction between mathematical and logical that is
convincing. I am assuming that you would like to claim that Zermelo set
theory (Z) and its variants are mathematical and opposed to logical,
whereas some particular form of deductive SOL is logical as opposed to
mathematical. You can try to justify such a claim, but you must take into
account not only what I said earlier here, but the fact that one can
trivially adjust Z in many relevant ways; e.g., using urelements, and
ordered pairs as primitive, etcetera. Ultimately, one also has to confront
the view that the cumulative hierarchy of length omega + omega is logical
anyways, as it is simply a streamlined version of cumulative type theory
with omega + omega types, where the bottom type has no objects. Cumulative
type theory is just a variant of type theory, which is considered
"logical". So from that point of view, Zermelo set theory (perhaps with
bounded comprehension if you want) is already "logical".

>Shipman:
>    This is a failure of perspective frequently seen in discussions of
>alternatives to ZFC.

This is a failure of perspective frequently seen in discussion of
alternatives to Z and ZFC, whereby something is called an alternative to Z
or ZFC that is simply a variant of Z or ZFC that is inferior for the
purposes of the formalization of mathematics.

>But SOL, or nth-order logic for
>n large enough (4 ought to suffice) to do all "ordinary mathematics", or Type
>Theory, are all natural systems, ***with natural (though incomplete)
>deductive calculi containing only "logical" axioms***,

As I indicated above, I haven't seen you justify any such distinction.

>which can be accepted
>on their own terms, and in fact PREDATE Zermelo set theory (though Russell's
>type-theoretic system was more cumbersome than modern versions of SOL or type
>theory).

It is obviously true that Russell's type theory predates set theory, but
set theory was an obviously big improvement over type theory as a
formalization of mathematics. You are suggesting that there is a seriously
different move from type theory to something that is seriously different
than set theory, that also provides an eand appropriate formalization of
mathematics, that it somehow of special significance. I have yet to see you
back up such a claim.

I repeat the way of looking at set theory from a "logical" point of view.
Namely, as cumulative type theory, made into a single sort. You have to
justify a claim that that is not "logical" in order to get anywhere with
such ideas.

>Thus you can equally well look at it the other way round.
>Zermelo's system had technical advantages over Russell's which facilitated
>the development of mathematics, but something important was lost by building
>the system on the non-logical and initially unintuitive notion of set as
>axiomatized by Zermelo (with an assist from Frankel).  We've (almost) all
>developed an intuition now for "set" and "membership" that matches what ZFC
>axiomatizes, but this particular intuitive structure did not fall out right
>away as soon as "set theory" began, it was hard-won after a half-century of
>struggle.

I regard this as completely wrong. The only thing that was "hard-won" was
the idea that mathematics can be elegantly formalized at all, and that
there is any point to formalizing mathematics. The notions of set and
membership implicit in understanding Z or Z with natural numbers as
urelements are totally intuitive, natural,  and obvious and ingrained in
mathematical thought and were not hard-won. The serious contemporary issue
to this day is whether there is anything about our understanding of them
that even suggests anything like "determinate truth values". That is a
matter that has been discussed elsewhere on the FOM recently. My stated
view on this has been that it is totally unclear whether "determinate truth
values" exist or what it even means in the context of even set theory of
rank < omega + omega, and that this issue is irrelevant to when, how, or
why the general matheamtical community is going to accept any new axioms
for mathematics. The latter is not going to be decided on philosophical
grounds, but rather on the basis of coherent pragmatism and a feeling of
consistency based on experience. (There is a good case that the feeling of
consistency of ZFC is based on much more than experience, but in any case
such "intrinsic" reasons do not lift up to large cardinal axioms and the
like).

What will be especially "hard-won", if it happens at all, is any widespread
move to use any kind of deductive SOL for the formalization of mathematics.

>Shipman:
>I am DEFINING a deductive calculus for SOL which I call the "ZFC-calculus",
>which consists of all sentences phi of SOL such that ZFC proves that phi is a
>second-order validity.

This is a definition of a set T of sentences of SOL. I gather that you are
adding to T, certain trivial axioms together with the key comprehension
axiom

(therexists S)(forall x1,...,xk)(S(x1,...,xk) iff phi(x1,...,xk))

where phi is any formula in SOL in which S is not free.

You must be aware that T itself has no strength; i.e., T has a one point
model.

>I am PROPOSING that this be considered a "most
>complete" deductive calculus, as a challenge, in order to establish
>technically a superiority of FOL+ZFC vis-a-vis SOL+any SOL-deductive-calculi
>that have hitherto been plausibly proposed.

>If no one can supply a plausible
>deductive calculus for SOL (presumably motivated by logical considerations)
>that generates a second-order-validity not generated by the ZFC-calculus,
>then we have a much more solid reason for not preferring the "logicistic"
>foundation of mathematics via SOL (and presumably similar foundations using
>HOL or type theory).

I think you are asking the wrong kind of question. In order to make a
deductive SOL useful for the formalization of mathematics, it has to
contain existential principles. And such existential principles obviously
cannot be SOL validities. But your "ZFC-calculus" and the like consist
entirely of SOL vaidities.

So if I understand your proposal right, it seems confused. Is this a case
of more "SOL confusion"?