FOM: Infinity

[A.P. Hazen]

   About finitely axiomatizable and predicative systems....
   (i) The use of "basic" predicative second order logic (only one "level"
of "propositional functions"; what Church calls the "predicative" second
order calculus in section 58 of "Introduction to mathematical Logic"
(1956)) allows you to substitute a single axiom for the axiom scheme of a
First-Order theory like PA, Zermelo set theory, or ZF.  "Predicative"
propositional functions are those definable  by First-Order formulas*, so
this isn't surprising: you are essentially replacing an axiom scheme with
an axiom that explicitly quantifies over (extensions of) formulas.
(*Technically, we ought to say "parametrically definable," since the first
order formula  may have free variables in them: these are the variables
bound by the indefinitely long string of initial universal quantifiers in a
careful formulation of the induction/separation/replacement scheme.  The
bad news being that  this complicates the formulation of a version with
finitely many "set-existence" axioms replacing the comprehension SCHEME of
the predicative Second-Order LOGIC.)
   (ii)  The fundamental idea behind Von Neumann/Bernays/Gödel set theory
is just this: reformulate ZF in predicative Second-Order logic.  This is
what is behind the Novak (=Gal, Miss Novak having published  her result
back in the days-- 1950, to be exact-- when women changed their surnames on
marriage) proof-theoretic relative consistency proof of GB relative to ZF,
improved by Shoenfield in J.S.L. 1954.  Basic idea: Gentzen's Hauptsatz
extends very easily from First-Order logic to predicative Second-Order
logic (just modify the definition of "grade" for the induction on
complexity of cut-formulas),and -- since cut-free proofs have the
subformula property -- a proof in the predicative  Second-Order theory of a
First-Order statement can be transformed into a  purely First-Order proof.
   (iii)  Standard textbook versions of GB are a bit more complicated,
however.  First-Order ZFC has an axiom of choice that says every SET has a
choice function; the First-Order language does not allow one to formulate
the stronger principle of "Global Choice," that there is a choice function
on the universe.  (You could do it if you supplemented the language with a
"selection functor": cf. Quine, "Set theory and its Logic," pp. 220 ff.,
for discussion.)  But as long as you have the expressive power of the
Second-Order language available, why not make use of it?  Textbook GB,
then, has global choice.  Making the proof that it is conservative over ZFC
a bit more complicated.
  (iv) Predicative Second-Order LOGIC is usually formulated with a
comprehension SCHEME.  So when a finitely axiomatized "PSO" theory (= a
theory in the language of PSO logic with finitely many non-logical axioms)
is reconstrued as a First-Order theory, it won't be finitely axiomatized:
the axiom SCHEME of the logic has been reconstrued as a non-logical axiom
SCHEME of class existence. If, however, the domain of "First-Order objects"
(= the critters the First-Order variables range over) is closed under the
formationof finite sequences....  As, for example, the domain of natural
numbers and (by Wiener and Kuratowski) the domain of sets are....  Well, in
that case RELATIONS (of arbitrary adicity) can be construed as  classes,
and Von Neuman showed that a finite list of class-existence axioms could do
the work of the predicative class (and relation) existence schema, allowing
the finitely axiomatized PSO  theory to be transformed into a finitely
axiomatized First-Order theory.  The same basic trick is what makes
possible variable-less formulations of First-Order logic: cf. Quine's
"Variables Explained Away" (in "Selected logic Papers"), "The Variable" and
"Algebraic Logic and Predicate Functors" (in the revised (1976) edition of
"The Ways of Paradox").
   (v) Use of this technique to give axiomatizations of predicative or
ramified systems goes at least back  to Hao Wang's 1949 "A Theory of
Constructive Types" ("Methodos" vol. 1, pp. 374-384.  (This is not, I
suspect, what most  people would think  of as  a
simple/intuitive/elegant/easy-to-use axiomatization....)
    (vi) But, returning to the original topic: GB is conservative over ZF.
I see no reason to suspect that replacing the axiom of infinity with its
negation would affect this relationship.  So "Finite GB" should be a good
finitely axiomatizABLE theory of finite sets.  In USING it, you'd use the
axiom SCHEME of class comprehension.  For some metamathematical results it
is enough to know  that the use of a finite collection of class-existence
axioms there.  For those that depend on details about the length of proofs,
a more detailed analysis may be needed.  John Burgess discusses this in
"Predicative Logic and Formal Arithmetic" (NDJoFL 39 (1998), pp. 1-17 ... I
am a co-author of this paper, but Johndid the hard  part!).
--
Allen Hazen
Philosophy Department
U. of Melbourne