[FOM] Variants of ACA

[pax0 at seznam.cz]

Hi Jeff
what is the typical theorem which can be proved in ACA but not in ACA0?More generally:
is there a list of theorems such that n-th entry can be proved in ACA with Sigma^0-n-induction 
but not in ACA with (n-1)-Sigma^0 induction?
Thank you, Jan Pax

>  
>  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
>  
>  
>  
>  _______________________________________________
>  FOM mailing list
>  FOM at cs.nyu.edu
>  http://www.cs.nyu.edu/mailman/listinfo/fom
>  
>  
>