[FOM] Arithmetic Axiom Systems for annotations
John Burgess
jburgess at princeton.edu
Wed May 15 11:57:15 EDT 2013
ad (1) PFA in this context cannot mean "proper forcing axiom" since
it is supposed to denote a weaker system than (2). It must mean
something like "Peano functional arithmetic": the system that removes
induction from PA WITHOUT adding exponentiation
ad (22) & (23) the name of a single system, Delta-superscript-1-
subscript-1-dash-CA, has been divided into two pieces; the answer to
question 2 is "nothing by itself, it is part of a longer name"
there are many similar pairs below, and questions 3, 4, 5 are all to
be answered the same way
On May 15, 2013, at 10:09 AM, zhangyinsheng wrote:
> Dear Sir.,
>
>
> The following list of Arithmetic Axiom Systems is proposed by FOM
> without annotations. I tried to give some annotations yet 9
> QUESTIONS left for your answers (and if any annotation wrong you are
> welcome to correct it)!
>
>
>
> Godel Hierarchy
> (Arithmetic Axiom Systems,whose consistensy is stronger in top-down)
>
> (1) PFA:Proper Forcing Axiom.
> (2) EFA: Elementary Functional Arithmetic,which removes induction
> from PA,so exponentiation
> must be added as "Ax (x ^ y' )=x ^y multi x".[1]
> (3) SEFA:Superexponential Function Arithmetic.
> (4) PRA:Primitive Recursive Arithmetic.
> (5) RCA_0:Recursive Comprehension Axiom,subscript "0" indicates
> restrict induction[2]
> "AxEy phi(x,y) implies Ef Ax phi(x,phi(x))".[3]
> (6) I sigma _2: Induction of sigma _2, sub "2" indicates one
> occurance of E-A in a Skolem prenex form of a formulas.
> (7) I sigma _3.
> (8) PA:Peano Arithmetic.
> (9) ACA _0:Arithmetical Comprehension Axiom,the subscript 0
> indicates that it includes only
> a restricted portion of the full second-order induction
> scheme. [2,pp.6-9]
> ACA=KL_0+ACA
> KL_0: Koenig Lemma. [3, pp.114]
> (10) ACA _0 + (An,X)(TJ(n,X)):ACA_ 0 + "for all n,X, the n-th Turing
> jump of X exists". Turing jump TJ(X)is complete recuisively
> enumaerable set relative to X.
> Turing jump TJ(n,X)is recuisively defined by TJ(0,X)=X,TJ(n
> +1,X)=TJ(TJ(n,X)).[2,pp.6-9]
> (11) ACA:Arithmetical Comprehension Axiom.
> (12) RCA _0 + TJ(omega): Omega is the set of natural numbers.
> (13) ACA _0 + TJ(omega).
> (14) ACA + TJ(omega).
> (15) ACA _ 0 + (Ax)(TJ(omega,x)).
> (16) ACA _ 0 + {(alpha,x)(TJ(alpha,x)):alpha < omega ^omega }.
> (17) ACA _ 0 + {(alpha<omega^omega )(Ax) (TJ(alpha,x))}.
> (18) RCA _ 0 + TJ(omega ^omega ).
> (19) ACA _ 0 + TJ(omega ^omega ).
> (20) ACA _ 0 + {(Ax)(TJ(omega ^omega,x))}.
> (21) ACA _0 + {(Ax)(TJ(alpha,x)):alpha < OE_0}. (QUESTION 1: What
> does "OE _0" mean?)
> (22) Delta _ 1:Bounded Arithmetics that comprehension scheme
> consists of the formulas of the form An(phi(n) double-direction
> implies psi(n)) implies EX An(n?X double-direction
> implies phi(n))),where phi(n) is the form of An phi(n) and psi(n) is
> of En phi (n) [2,pp.25]
> (23) Sub 1-CA: (QUESTION 2: What does "sub 1" mean ?)
> (24) RCA _ 0 + TJ(OE _0 ).
> (25) ACA _ 0 + TJ(OE _0 ).
> (26) ACA + TJ(OE _ 0 ).
> (27) ACA _0 + (Ax)(TJ(OE_0 ,x)).
> (28) {ATI(alpha):alpha < Gamma _0 }:Gamma _0 is the smallest
> impredicative ordinal.(Bill Tait in FOM)
> (29) ATR_0.Arithmetical transfinite recursion,"sub 0" indicates
> restricted induction.
> (30) ATI( < gamma _0 ).
> (31) ATR:Arithmetical Transfinite Recursion.
> (32) Pi _ 1.
> (33) sub-2-TI_0 : (QUESTION 3:What do "sub 2" and "sub 0" mean ? )
> (32) Pi _1.
> (34) sub 2-TI.
> (35) TI: Transfinite Induction
> (36) ID _2 :
> ID_1: theory of inductive definitions (first level). This has the
> same strength as the Kleene-Vesley system FIM.
> This is what Wim Veldman used for his proof of the Kruskal theorem.
> ID2, ID3, etc.:
> All of these count as predicative in type theory.(Bas in FOM)
> (37) ID _< omega.
> (32) Pi _1.
> (38)sub 1-CA _0:
> (32) Pi _1.
> (39) sub 1-CA
> (32) Pi _1.
> (40)sub 1-CA+TI
> (32) Pi _1.
> (41) ) sub 1-TR sub 0 : (QUESTION 4:What is _1-TR_0 ?)
> (32) Pi _1.
> (42) sub 1-TR.
> (32) Pi_1.
> (43) sub 2-CA_0.
> (32) Pi_1.
> (44) sub 2-CA+TI.
> (45) Z_ 2: Second-Order Arithmetic.
> (46) Z _3 (QUESTION 5:What does "_ 3" mean ?)
> (47) Type Theory.
> (48) Weak Zermelo.
> (49) ZC:Zermelo+Choice Axiom
> (50) ZC + (A alpha < omega _ 1)(V(alpha)) :omega _ 1 is the first
> uncountable ordinal. alpha is any ordinals.[5. pp.5]
> V is the set-theoretic universe which is viewed as the cumulative
> hierarchy, open ended and under-determined by the set-theoritic
> axioms,and inviting further postulations based on reflection and
> generalization. [6.pp.XVII]
> (51) KP(#): Kripke Platek set theory.The theory KP is an elementary
> first order theory in the vocabulary {epsilon}.
> It is a weakening of ZF set theory where the power set axiom is
> removed, and the seperation and collection axiom acheme are
> restricted to "delta _ 0" formulas.
> The "delta _ 0" formulas are the mmbers of the smallest class of
> formulas that contains the atomic formulas in the vocabulary
> {epsilon} and is closed under finite conjunction and
> disjunction,bound quantifiers (Ex epsilon u) and (Ax epsilon u),and
> negation.[7]
> (QUESTION 6:What does the Sharp symbol mean ?)
> (52) ZFC: Zermelo–Fraenkel +Choice Axiom.
> (53) ZFC + strongly inaccesible.
> (54) ZFC + strongly Mahlo:there exists an Mahlo cardinal.
> (55) ZFC + {strongly n-Mahlo: n < omega }:there exists an n-Mahlo
> cardinal,n < omega.
> (56) ZFC + (An < omega )(strongly n-Mahlo).
> (57) ZFC + (weakly compact).
> (58) ZFC + (indescribable).
> (59) ZFC + (subtle):ZFC + "there exists a subtle cardinal."
> (60) ZFC + (almost ineffable):ZFC + "there exists an almost
> ineffable cardinal".
> (61) ZFC + (ineffable).
> (62) ZFC + {n-subtle: n < omega}
> (63) ZFC + (An < omega)(n-subtle).
> (64) ZFC + k emptyset omega :(QUESTION 7:What does "k emptyset
> omega" mean ?)
> (65) ZFC + (A alpha < omega_1)(k emptyset alpha ).
> (66) ZFC + 0 # ."ZFC + 0 sharp "is a subset of omega satisfying
> Gaifman Theorem [8,pp.99]
> (67) ZFC + (Ax pi omega)(x #):ZFC + "for all x containing omega, x
> sharp exists."(QUESTION 8:What does # mean ?)
> (68) ZFC + k emptyset omega _1.(Question 8:What does "+ k emptyset
> omega_1" mean?)
> (69) ZFC + Ramsey.
> (70) ZFC + Measurable:ZFC + "there exists a measurable cardinal".
> (71) ZFC + Concentrating Measurable.
> (72) ZFC + Strong.
> (73) ZFC + Woodin.
> (74) ZFC + Superstrong.
> (75) ZFC + Supercompact.
> (76) ZFC + Extendible.
> (77) ZFC + Vopenka.
> (78) ZFC + Almost Huge.
> (79) ZFC + Huge.
> (80) ZFC + Superhuge.
> (81) ZFC + (An < omega)(n-huge).
> (82) ZFC + Rank into Itself.
> (83) ZFC + Rank + 1 into Itself.
> (84) VB + V into V. (Question 9:What does it mean?)
>
>
>
> Reference:
> [1]http://planetmath.org/ElementaryFunctionalArithmetic
> [2] Stephen G.Simpson. "Subsystems of Second Order Arithmetic",https://www.math.psu.edu/simpson/sosoa/chapter1.pdf
> .
> [3]H.Jerome Keisler.Nonstandard arithmetic and reverse
> mathematics.The Bulletine of Symbolic,Volume 12,Number 1,2006.
> [4]Stephen G.Simpson.Friedman's research on subsystems of second
> order arithmetic, Harvey Friedman's research on the Foundations of
> Mathematics, Elsevier Science Publishers B.V.1985pp.137-160
> [5] H.Jerome Keisler and Julia Knight.Barwise:infinitary logic and
> admissible sets,The Bulletine of Symbolic,Volume 10,Number 1,2004.
> [6] Akihiro Kanamori.The Higher Infinite,Large Cardinals in Set
> Theory from Their Beginnings,Second Edition,`1994,Springer-Verlag.
> [7]H.Jerome Keisler and Julia F.Knight.Barwise:infinitary logic and
> admissible sets,Bulletin of Symbolic Volume 10.Number 1,March
> 2004.pp.14
> [8] Gaifman. Measurable cardinals and constructible sets
> (abstract).NAMS 11(1964),771.XX.99
>
>
>
>
>
>
>
>
>
>
> Zhang Yinsheng,Ph.D
>
> Support Center of Information Technology
> Institute of Scientific & Technical Information of China
> No.15 Fuxing Road, Beijing，Haidian District, China, 100038
> e-mail: zhangyinsheng at istic.ac.cn
> Tel:86-10-58882074
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130515/9002c61d/attachment-0001.html>
More information about the FOM
mailing list