[FOM] Variants of ACA

[Jeff Hirst]

On Nov 11, 2011, at 12:26 PM, pax0 at seznam.cz wrote:

Is there a complete list of variants (together with definitions) of the second order fragment ACA.
There are quite a few of them, including
ACA^+,ACA_0,ACA,ACA^',ACA^*.
Thank you, Jan Pax


Hi Jan-

Here's the short answer:

The _0 indicates induction restricted to Sigma^0_1 formulas.  No _0 indicates full induction.

The ^' indicates that the n^th Turing jump exists for all n.  The ^+ indicates the omega jump exists.



So this explains these combinations:

ACA_0 is RCA_0 plus comprehension for arithmetically defined sets.

ACA  is ACA_0 plus full induction.

ACA_0^' is ACA_0 plus a formalization of "for every X and n, the nth Turing jump of X exists."

        Note:  ACA_0^' is strictly between ACA_0 and ACA in strength.  ACA^' would be ACA_0^' plus full induction,
                  which is the same as ACA.

ACA_0^+ is ACA_0 plus a formalization of "for every X, the omega-jump of X exists."

ACA^+ is ACA_0^+ plus full induction.



ACA^* is a new one for me.  The * superscript usually indicates restriction of the induction scheme
to Sigma^0_0 formulas and appending exponentiation axioms.  (See section X.4 in Simpson's book.)
Arithmetical comprehension allows reduction of formulas with many quantifiers to formulas with
no quantifiers and one set parameter.  In this setting, ACA_0^* would be ACA_0.  Note that RCA_0^*
and WKL_0^* are weaker theories than RCA_0 (resp. WKL_0).

Simpson's book has definitions of ACA, ACA_0, ACA_0^+, and formalizations of Turing jumps.

Marcone and Montalban recently published an article entitled "The Veblen functions for computability
theorists" in the JSL  (Vol 66 no 2 (2011)  575-602) that uses a very elegant formalization of the jump.
That would be a good way to define ACA_0^' and ACA_0^+ (and equivalent to prior uses in the literature.)

Hope this helps...

-Jeff