In[]:=
allaxioms=Keys[KeySelect[setmm["Statements"],StringStartsQ["ax-"]]]
Out[]=
{ax-mp,ax-1,ax-2,ax-3,ax-gen.1,ax-gen,ax-4,ax-5,ax-6,ax-7,ax-8,ax-9,ax-10,ax-11,ax-12,ax-13,ax-ext,ax-rep,ax-sep,ax-nul,ax-pow,ax-pr,ax-un,ax-reg,ax-inf,ax-inf2,ax-cc,ax-dc,ax-ac,ax-ac2,ax-groth,ax-cnex,ax-resscn,ax-1cn,ax-icn,ax-addcl,ax-addrcl,ax-mulcl,ax-mulrcl,ax-mulcom,ax-addass,ax-mulass,ax-distr,ax-i2m1,ax-1ne0,ax-1rid,ax-rnegex,ax-rrecex,ax-cnre,ax-pre-lttri,ax-pre-lttrn,ax-pre-ltadd,ax-pre-mulgt0,ax-pre-sup,ax-addf,ax-mulf,ax-hilex,ax-hfvadd,ax-hvcom,ax-hvass,ax-hv0cl,ax-hvaddid,ax-hfvmul,ax-hvmulid,ax-hvmulass,ax-hvdistr1,ax-hvdistr2,ax-hvmul0,ax-hfi,ax-his1,ax-his2,ax-his3,ax-his4,ax-hcompl,ax-xrssca,ax-xrsvsca,ax-7d,ax-8d,ax-9d1,ax-9d2,ax-10d,ax-11d,ax-prv1.1,ax-prv1,ax-prv2,ax-prv3,ax-luk1,ax-luk2,ax-luk3,ax-wl-13v,ax-wl-11v,ax-c5,ax-c4,ax-c7,ax-c10,ax-c11,ax-c11n,ax-c15,ax-c9,ax-c14,ax-c16,ax-riotaBAD,ax-frege1,ax-frege2,ax-frege8,ax-frege28,ax-frege31,ax-frege41,ax-frege52a,ax-frege54a,ax-frege58a,ax-frege52c,ax-frege54c,ax-frege58b,ax-bgbltosilva,ax-hgprmladder,ax-tgoldbachgt,ax-bgbltosilvaOLD,ax-hgprmladderOLD,ax-tgoldbachgtOLD}
In[]:=
ParallelMap[#->StringCases[Import["http://us.metamath.org/mpeuni/"<>#<>".html","Plaintext"],___~~"Description: "~~Shortest[x__]~~"."~~___->x]&,allaxioms]
Out[]=
ax-mp{Rule of Modus Ponens},ax-1{Axiom Simp },ax-2{Axiom Frege },ax-3{Axiom Transp },ax-gen.1{},ax-gen{Rule of Generalization},ax-4{Axiom of Quantified Implication},ax-5{Axiom of Distinctness},ax-6{Axiom of Existence},ax-7{Axiom of Equality},ax-8{Axiom of Left Equality for Binary Predicate},ax-9{Axiom of Right Equality for Binary Predicate},ax-10{Axiom of Quantified Negation},ax-11{Axiom of Quantifier Commutation},ax-12{Axiom of Substitution},ax-13{Axiom of Quantified Equality},ax-ext{Axiom of Extensionality},ax-rep{Axiom of Replacement},ax-sep{The Axiom of Separation of ZF set theory},ax-nul{The Null Set Axiom of ZF set theory},ax-pow{Axiom of Power Sets},ax-pr{The Axiom of Pairing of ZF set theory},ax-un{Axiom of Union},ax-reg{Axiom of Regularity},ax-inf{Axiom of Infinity},ax-inf2{A standard version of Axiom of Infinity of ZF set theory},ax-cc{The axiom of countable choice (CC), also known as the axiom of denumerable choice},ax-dc{Dependent Choice},ax-ac{Axiom of Choice},ax-ac2{In order to avoid uses of ax-reg 8494 for derivation of AC equivalents, we provide ax-ac2 9282 , which is equivalent to the standard AC of textbooks},ax-groth{The Tarski-Grothendieck Axiom},ax-cnex{The complex numbers form a set},ax-resscn{The real numbers are a subset of the complex numbers},ax-1cn{1 is a complex number},ax-icn{i is a complex number},ax-addcl{Closure law for addition of complex numbers},ax-addrcl{Closure law for addition in the real subfield of complex numbers},ax-mulcl{Closure law for multiplication of complex numbers},ax-mulrcl{Closure law for multiplication in the real subfield of complex numbers},ax-mulcom{Multiplication of complex numbers is commutative},ax-addass{Addition of complex numbers is associative},ax-mulass{Multiplication of complex numbers is associative},ax-distr{Distributive law for complex numbers (left-distributivity)},ax-i2m1{i-squared equals -1 (expressed as i-squared plus 1 is 0)},ax-1ne0{1 and 0 are distinct},ax-1rid{1 is an identity element for real multiplication},ax-rnegex{Existence of negative of real number},ax-rrecex{Existence of reciprocal of nonzero real number},ax-cnre{A complex number can be expressed in terms of two reals},ax-pre-lttri{Ordering on reals satisfies strict trichotomy},ax-pre-lttrn{Ordering on reals is transitive},ax-pre-ltadd{Ordering property of addition on reals},ax-pre-mulgt0{The product of two positive reals is positive},ax-pre-sup{A nonempty, bounded-above set of reals has a supremum},ax-addf{Addition is an operation on the complex numbers},ax-mulf{Multiplication is an operation on the complex numbers},ax-hilex{This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory},ax-hfvadd{Vector addition is an operation on ℋ },ax-hvcom{Vector addition is commutative},ax-hvass{Vector addition is associative},ax-hv0cl{The zero vector is in the vector space},ax-hvaddid{Addition with the zero vector},ax-hfvmul{Scalar multiplication is an operation on and ℋ },ax-hvmulid{Scalar multiplication by one},ax-hvmulass{Scalar multiplication associative law},ax-hvdistr1{Scalar multiplication distributive law},ax-hvdistr2{Scalar multiplication distributive law},ax-hvmul0{Scalar multiplication by zero},ax-hfi{Inner product maps pairs from ℋ to },ax-his1{Conjugate law for inner product},ax-his2{Distributive law for inner product},ax-his3{Associative law for inner product},ax-his4{Identity law for inner product},ax-hcompl{Completeness of a Hilbert space},ax-xrsscaAssume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set},ax-xrsvscaAssume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set},ax-7d{Distinct variable version of ax-11 2033 },ax-8d{Distinct variable version of ax-7 1934 },ax-9d1{Distinct variable version of ax-6 1887 , equal variables case},ax-9d2{Distinct variable version of ax-6 1887 , distinct variables case},ax-10d{Distinct variable version of axc11n 2306 },ax-11d{Distinct variable version of ax-12 2046 },ax-prv1.1{},ax-prv1{First property of three of the provability predicate},ax-prv2{Second property of three of the provability predicate},ax-prv3{Third property of three of the provability predicate},ax-luk1{1 of 3 axioms for propositional calculus due to Lukasiewicz},ax-luk2{2 of 3 axioms for propositional calculus due to Lukasiewicz},ax-luk3{3 of 3 axioms for propositional calculus due to Lukasiewicz},ax-wl-13v{A version of ax13v 2246 with a distinctor instead of a distinct variable expression},ax-wl-11v{Version of ax-11 2033 with distinct variable conditions},ax-c5{Axiom of Specialization},ax-c4{Axiom of Quantified Implication},ax-c7{Axiom of Quantified Negation},ax-c10{A variant of ax6 2250 },ax-c11{Axiom ax-c11 34015 was the original version of ax-c11n 34016 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 34016 could replace it},ax-c11n{Axiom of Quantifier Substitution},ax-c15Axiom ax-c15 34017 was the original version of ax-12 2046 , before it was discovered (in Jan},ax-c9{Axiom of Quantifier Introduction},ax-c14{Axiom of Quantifier Introduction},ax-c16{Axiom of Distinct Variables},ax-riotaBAD{Define restricted description binder},ax-frege1The case in which 𝜑 is denied, 𝜓 is affirmed, and 𝜑 is affirmed is excluded,ax-frege2If a proposition 𝜒 is a necessary consequence of two propositions 𝜓 and 𝜑 and one of those, 𝜓 , is in turn a necessary consequence of the other, 𝜑 , then the proposition 𝜒 is a necessary consequence of the latter one, 𝜑 , alone,ax-frege8{Swap antecedents},ax-frege28{Contraposition},ax-frege31{𝜑 cannot be denied and (at the same time ) ¬ ¬ 𝜑 affirmed},ax-frege41{The affirmation of 𝜑 denies the denial of 𝜑 },ax-frege52aThe case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed ( in this specific case the identity logical funtion ) and the same proposition, this time where we substituted the content of 𝜓 , is denied does not take place,ax-frege54a{Reflexive equality of wffs},ax-frege58aIf ∀ 𝑥 𝜑 is affirmed, [ 𝑦 / 𝑥 ] 𝜑 cannot be denied,ax-frege52c{One side of dfsbcq 3435 },ax-frege54c{Reflexive equality of sets (as classes)},ax-frege58bIf ∀ 𝑥 𝜑 is affirmed, [ 𝑦 / 𝑥 ] 𝜑 cannot be denied,ax-bgbltosilva{The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [ OeSilva ] p},ax-hgprmladder{There is a partition ("ladder") of primes from 7 to 8},ax-tgoldbachgt{Temporary duplicate of tgoldbachgt 30732 , provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than ( ; 10↑ ; 27) have at least a representation as a sum of three odd primes},ax-bgbltosilvaOLD{Obsolete version of ax-bgbltosilva 41484 as of 9-Sep-2021},ax-hgprmladderOLD{Obsolete version of ax-hgprmladder 41488 as of 9-Sep-2021},ax-tgoldbachgtOLD{Obsolete version of ax-tgoldbachgt 41485 as of 9-Sep-2021}
In[]:=
usedaxioms
Out[]=
{ax-1,ax-10,ax-11,ax-12,ax-13,ax-1cn,ax-1ne0,ax-1rid,ax-2,ax-3,ax-4,ax-5,ax-6,ax-7,ax-8,ax-9,ax-ac2,ax-addass,ax-addcl,ax-addf,ax-addrcl,ax-cc,ax-cnex,ax-cnre,ax-distr,ax-ext,ax-gen,ax-i2m1,ax-icn,ax-inf2,ax-mp,ax-mulass,ax-mulcl,ax-mulcom,ax-mulf,ax-mulrcl,ax-nul,ax-pow,ax-pr,ax-pre-ltadd,ax-pre-lttri,ax-pre-lttrn,ax-pre-mulgt0,ax-pre-sup,ax-rep,ax-resscn,ax-rnegex,ax-rrecex,ax-sep,ax-un}
In[]:=
Length[usedaxioms]
Out[]=
50
In[]:=
KeySelect[Association[%391],!MemberQ[usedaxioms,#]&]
Out[]=
ax-gen.1{},ax-reg{Axiom of Regularity},ax-inf{Axiom of Infinity},ax-dc{Dependent Choice},ax-ac{Axiom of Choice},ax-groth{The Tarski-Grothendieck Axiom},ax-hilex{This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory},ax-hfvadd{Vector addition is an operation on ℋ },ax-hvcom{Vector addition is commutative},ax-hvass{Vector addition is associative},ax-hv0cl{The zero vector is in the vector space},ax-hvaddid{Addition with the zero vector},ax-hfvmul{Scalar multiplication is an operation on and ℋ },ax-hvmulid{Scalar multiplication by one},ax-hvmulass{Scalar multiplication associative law},ax-hvdistr1{Scalar multiplication distributive law},ax-hvdistr2{Scalar multiplication distributive law},ax-hvmul0{Scalar multiplication by zero},ax-hfi{Inner product maps pairs from ℋ to },ax-his1{Conjugate law for inner product},ax-his2{Distributive law for inner product},ax-his3{Associative law for inner product},ax-his4{Identity law for inner product},ax-hcompl{Completeness of a Hilbert space},ax-xrsscaAssume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set},ax-xrsvscaAssume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set},ax-7d{Distinct variable version of ax-11 2033 },ax-8d{Distinct variable version of ax-7 1934 },ax-9d1{Distinct variable version of ax-6 1887 , equal variables case},ax-9d2{Distinct variable version of ax-6 1887 , distinct variables case},ax-10d{Distinct variable version of axc11n 2306 },ax-11d{Distinct variable version of ax-12 2046 },ax-prv1.1{},ax-prv1{First property of three of the provability predicate},ax-prv2{Second property of three of the provability predicate},ax-prv3{Third property of three of the provability predicate},ax-luk1{1 of 3 axioms for propositional calculus due to Lukasiewicz},ax-luk2{2 of 3 axioms for propositional calculus due to Lukasiewicz},ax-luk3{3 of 3 axioms for propositional calculus due to Lukasiewicz},ax-wl-13v{A version of ax13v 2246 with a distinctor instead of a distinct variable expression},ax-wl-11v{Version of ax-11 2033 with distinct variable conditions},ax-c5{Axiom of Specialization},ax-c4{Axiom of Quantified Implication},ax-c7{Axiom of Quantified Negation},ax-c10{A variant of ax6 2250 },ax-c11{Axiom ax-c11 34015 was the original version of ax-c11n 34016 ("n" for "new"), before it was discovered (in May 2008) that the shorter ax-c11n 34016 could replace it},ax-c11n{Axiom of Quantifier Substitution},ax-c15Axiom ax-c15 34017 was the original version of ax-12 2046 , before it was discovered (in Jan},ax-c9{Axiom of Quantifier Introduction},ax-c14{Axiom of Quantifier Introduction},ax-c16{Axiom of Distinct Variables},ax-riotaBAD{Define restricted description binder},ax-frege1The case in which 𝜑 is denied, 𝜓 is affirmed, and 𝜑 is affirmed is excluded,ax-frege2If a proposition 𝜒 is a necessary consequence of two propositions 𝜓 and 𝜑 and one of those, 𝜓 , is in turn a necessary consequence of the other, 𝜑 , then the proposition 𝜒 is a necessary consequence of the latter one, 𝜑 , alone,ax-frege8{Swap antecedents},ax-frege28{Contraposition},ax-frege31{𝜑 cannot be denied and (at the same time ) ¬ ¬ 𝜑 affirmed},ax-frege41{The affirmation of 𝜑 denies the denial of 𝜑 },ax-frege52aThe case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we s