FOM: Axioms of Infinity: first-order versus higher-order

[Allen Hazen]

    At the risk of belaboring the obvious...
    Stephen Simpson made the observation that when Church (and I, following
Church) talk about axioms of infinity as sentences of HIGHER-ORDER logic,
we are concerned with provability in axiomatized fragments of higher-prder
logic, not with validity under the STANDARD semantics of higher-order
logic.  And that higher-order logics so considered can be thought of as
theories in (many-sorted) FIRST-ORDER logic.  Two comments:
    (1) Even so there is a difference between a first-order axiom of
infinity and its second-order "version" formed by treating its constants as
variables and existentially quantifying.  The second-order "version" is a
sentence of a richer language: the "logical" machinery of second-order
logic amounts to additional "non-logical" vocabulary when the second-order
LOGIC is treated as a first-order THEORY, and the second-order variables
range (in any, standard or "Henkin," model) over a different domain from
those of the first-order variables of the original first-order statement.
So there are more possibilities for mutual interpretability with
second-order versions than there are with first-order sentences.  (This is
all obvious, but I have found that many of my philosophy colleagues find
the distinction between second-order and first-order logics very confusing!)
    (2) Care is needed: many-sorted first-order logic has properties that
can be surprising if one is used to ordinary, single-sorted, logic.
Example: Julian L. Hook, "A note on interpretations of many-sorted
theories," JSL 50 (1985), pp. 372-375.  Another example: a single-sorted
first-order language cannot give a categorical axiomatization of an
infinite structure, but can give a categorical axiomatization of a finite
one.  Now take your favorite denumerable structure (N, for example, or the
simple type hierarchy over some a domain of individuals of SPECIFIED finite
size).  Partition it up into infinitely many subdomains (e.g. numbers less
than 10, numbers less than 100, numbers less than 1000..., or objects of
type 0, objects of type 1, objects of type 2....).  Set up a many-sorted
language with infinitely many sorts of variables, one for each finite
subdomain (in the second example, this is just the usual notation of simple
type theory).  Now a recursive axiomatization can be categorical (hence
complete, hence decidable)!  The usual trick for producing non-standard
models of single-sorted first-order theories as a corollary to compactness
(add an individual constant to the language and an infinite set of axioms
which collectively keep the new constant from denoting any object in the
domain of the standard model) doesn't work because the new constant has to
be specified for the sort(s) of variables substitutable for it, and once
this is done finitely many non-identities are enough to yield
inconsistency.
      I'm not sure how relevant the curiosities of my second comment are to
questions about axioms of infinity, but they make me think many-sorted
first-order theories can behave in unobvious ways.

Allen Hazen
Philosophy
University of Melbourne