P. 3 of Theorem List - Higher-Order Logic Explorer

Theorem List for Higher-Order Logic Explorer - 201-222   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exnal 201*	Theorem 19.14 of [Margaris] p. 90. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [(E.\x:al (~ A)) = (~ (A.\x:al A))]
Axiom	ax-inf 202	The axiom of infinity: the set of "individuals" is not Dedekind-finite. Using the axiom of choice, we can show that this is equivalent to an embedding of the natural numbers in iota. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])
0.6  Rederive the Metamath axioms
Theorem	ax1 203	Axiom Simp. Axiom A1 of [Margaris] p. 49. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- R:*   &   |- S:*   =>   |- T. |= [R ==> [S ==> R]]
Theorem	ax2 204	Axiom Frege. Axiom A2 of [Margaris] p. 49. (Contributed by Mario Carneiro, 9-Oct-2014.)
|- R:*   &   |- S:*   &   |- T:*   =>   |- T. |= [[R ==> [S ==> T]] ==> [[R ==> S] ==> [R ==> T]]]
Theorem	ax3 205	Axiom Transp. Axiom A3 of [Margaris] p. 49. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- R:*   &   |- S:*   =>   |- T. |= [[(~ R) ==> (~ S)] ==> [S ==> R]]
Theorem	axmp 206	Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- S:*   &   |- T. |= R   &   |- T. |= [R ==> S]   =>   |- T. |= S
Theorem	ax5 207*	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- R:*   &   |- S:*   =>   |- T. |= [(A.\x:al [R ==> S]) ==> [(A.\x:al R) ==> (A.\x:al S)]]
Theorem	ax6 208*	Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- R:*   =>   |- T. |= [(~ (A.\x:al R)) ==> (A.\x:al (~ (A.\x:al R)))]
Theorem	ax7 209*	Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
|- R:*   =>   |- T. |= [(A.\x:al (A.\y:al R)) ==> (A.\y:al (A.\x:al R))]
Theorem	axgen 210*	Rule of Generalization. See e.g. Rule 2 of [Hamilton] p. 74. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= R   =>   |- T. |= (A.\x:al R)
Theorem	ax8 211	Axiom of Equality. Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:al   &   |- B:al   &   |- C:al   =>   |- T. |= [[A = B] ==> [[A = C] ==> [B = C]]]
Theorem	ax9 212*	Axiom of Equality. Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:al   =>   |- T. |= (~ (A.\x:al (~ [x:al = A])))
Theorem	ax10 213*	Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]
Theorem	ax11 214*	Axiom of Variable Substitution. It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [[x:al = y:al] ==> [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]]
Theorem	ax12 215*	Axiom of Quantifier Introduction. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
|- T. |= [(~ (A.\z:al [z:al = x:al])) ==> [(~ (A.\z:al [z:al = y:al])) ==> [[x:al = y:al] ==> (A.\z:al [x:al = y:al])]]]
Theorem	ax13 216	Axiom of Equality. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:al   &   |- B:al   &   |- C:(al -> *)   =>   |- T. |= [[A = B] ==> [(CA) ==> (CB)]]
Theorem	ax14 217	Axiom of Equality. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:(al -> *)   &   |- B:(al -> *)   &   |- C:al   =>   |- T. |= [[A = B] ==> [(AC) ==> (BC)]]
Theorem	ax17m 218*	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   =>   |- T. |= [A ==> (A.\x:al A)]
Theorem	axext 219*	Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It states that two sets are identical if they contain the same elements. Axiom Ext of [BellMachover] p. 461. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:(al -> *)   &   |- B:(al -> *)   =>   |- T. |= [(A.\x:al [(Ax:al) = (Bx:al)]) ==> [A = B]]
Theorem	axrep 220*	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:*   &   |- B:(al -> *)   =>   |- T. |= [(A.\x:al (E.\y:be (A.\z:be [(A.\y:be A) ==> [z:be = y:be]]))) ==> (E.\y:(be -> *) (A.\z:be [(y:(be -> *)z:be) = (E.\x:al [(Bx:al) /\ (A.\y:be A)])]))]
Theorem	axpow 221*	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:(al -> *)   =>   |- T. |= (E.\y:((al -> *) -> *) (A.\z:(al -> *) [(A.\x:al [(z:(al -> *)x:al) ==> (Ax:al)]) ==> (y:((al -> *) -> *)z:(al -> *))]))
Theorem	axun 222*	Axiom of Union. An axiom of Zermelo-Fraenkel set theory. (Contributed by Mario Carneiro, 10-Oct-2014.)
|- A:((al -> *) -> *)   =>   |- T. |= (E.\y:(al -> *) (A.\z:al [(E.\x:(al -> *) [(x:(al -> *)z:al) /\ (Ax:(al -> *))]) ==> (y:(al -> *)z:al)]))

< Previous  Wrap >