FOM: SOL confusion: reply to Friedman

[JoeShipman@aol.com]

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