FOM: SOL confusion: reply to Friedman
JoeShipman@aol.com
JoeShipman at aol.com
Sun Sep 10 01:01:37 EDT 2000
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.
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.
On the other hand, when one asks whether the SOL sentence S-->T is a
validity of SOL where S is the second-order sentence which categorically
axiomatizes the integers, there is first of all no semantic difficulty
because of the categoricity, and secondly no difficulty in identifying WHICH
validity one should be searching for because one doesn't have to know
{A1,A2,...,An} in advance (at least in the case of a
non-finitely-axiomatizable theory like PA or ZFC). 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).
Friedman:
>> One can obviously do this, even with the introduction of no constant,
relation, or function symbols. One can write down SOL statements asserting
that there exists relations giving what amounts to the first omega + omega
levels of the cumulative hierarchy, or what amounts to the first omega
levels of the cumulative hierarchy over a natural number system. This is
straightforward. And with the standard comprehension axiom scheme for
deductive SOL, one gets a deductive system that is more or less equivalent
to Zermelo set theory, or Zermelo set theory with natural numbers as
urelements. But so what? One has essentially lifted the usual set theoretic
foundations into another equivalent notation.<<
Shipman:
This is a failure of perspective frequently seen in discussions of
alternatives to ZFC. Of course one can found mathematics in an equivalent
way to "Zermelo set theory with natural numbers as urelements" (either in SOL
as you describe, or more naturally in Type Theory if you really want to go
arbitrarily many levels above the integers). 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***, 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). 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.
Friedman:
>> Obviously there is not any "most complete" deductive calculus for SOL.
...
ZFC is not a deductive calculus for SOL. I don't know what you are talking
about.<<
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. 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). You think it "obvious" that no one will do this, but
even though I agree with you that the above challenge is unlikely to be met,
a comparable challenge substituting Zermelo Set Theory for ZFC might well be.
If "logicism" can really get us as far as Zermelo Set Theory can, that's
pretty good (and you could then enjoy the distinction of having discovered
the nicest currently known theorem that is true for mathematical as opposed
to logical reasons).
-- JS
More information about the FOM
mailing list