FOM: Omega logic references

[A.P. Hazen]

Engstrom asks how badly compactness fails for omega logic, and whether
there is a standard reference on the subject.
    I would LIKE to be able to say (since i wrote it) that the standard
reference is the article "Non-constructive rules of inference" in v. 7 of
the "Routledge Encyclopedia of Philosophy."  Unfortunately, this is just an
elementary article on basic concepts and history, written for a general
philosophical audience, and not much help on technical questions.
(Bibliography includes a checlist of classic sources, though!)
    As for compactness....  Neil Tennant has helpfully pointed out that
compactness fails abysmally for omega logic.  So the question has to be
interpreted as "What interesting properties fore or less similar to
compactness does omega logic have and lack?"  What follows is free
association (with references) on that theme.
   (1)  Quite trivially, omega logic allows a COMPLETE formulation of
FIRST-ORDER arithmetic.  So...
   (2)  The interest moved to formulations of SECOND-ORDER arithmetic
having an omega rule for their First-Order quantifiers.  These systems are
INCOMPLETE.  This was noted early (Rosser, in "JSL" 1937), and is easy to
see by looking at what is needed for Gödel's incompleteness theorem for
FORMAL systems.  There are two essential ingredients:
        (i) DIAGONALIZATION (Gödel's double-substitution trick for
obtaining self-referential sentences) works as well for higher-order as for
first-order languages of arithmetic.  (Gödel's original paper proved it for
a higher-order system.)
        (ii) MATHEMATIZATION OF METAMATHEMATICS: metamathematical objects
(such as formulas and derivations) can be construed as mathematical
objects, and metamathematical notions (like "X is a proof of P") defined.
For formal systems, the proofs can be represented by Gödel numbers.  The
proofs of omega logic-- infinite trees of formulas-- can be represented by
sets of numbers.
   (3)  Leading to the not very well defined question: is Second Order
arithmetic "just barely" incomplete, or "badly" incomplete?  Mostowski
investigated Second-Order arithmetic with the omega rule (and other
non-constructive "turbocharging").  The basic system-- Second-Order
arithmetic with an omega rule but otherwise conventional-- has unpleasant
models: models which are not BETA MODELS.  That is, this system has models
in which the domain of sets-of-numbers the second-order variables range
over contains sets which (a) do NOT, when construed as sets of ordered
pairs, represent well-orderings, but (b) satisfy, in the model, the formula
saying "this set represents a well-ordering."  Maybe we can think of this
as a kind of BAD failure, or a failure of something analogous to
compactness: there is a denumerable set of formulas ("X is a well-ordering"
and an infinite set of formulas of the form "m X-precedes n" defining an
infinite descending X-path) which, from an intuitive, semantic, point of
view, OUGHT to be inconsistent, but which not only can't be shown
inconsistent by ordinary formal means (no surprise: compactness fails), but
can't even be shown inconsistent by the use of the omega rule.  Mostowski
went on to define another infinitary rule of inference that allowed him to
characterize Beta-models.  Relevant Mostowski papers (titles are something
like "On the classical and the omega-complete arithmetic" and "On a system
of arithmetic based on a non-constructive rule of inference") are included
in volume I of Mostowski's "Foundational Studies" (North-Holland yellow
"Studies in Logic").
    (4)  There are, however, partial