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

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

Type	Label	Description
Statement
Theorem	ax11 201*	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.
|- A:*   =>   |- T. |= [[x:al = y:al] ==> [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]]
Theorem	ax12 202*	Axiom of Quantifier Introduction. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint).
|- 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 203	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.
|- A:al   &   |- B:al   &   |- C:(al -> *)   =>   |- T. |= [[A = B] ==> [(CA) ==> (CB)]]
Theorem	ax14 204	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.
|- A:(al -> *)   &   |- B:(al -> *)   &   |- C:al   =>   |- T. |= [[A = B] ==> [(AC) ==> (BC)]]
Theorem	ax17 205*	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.
|- A:*   =>   |- T. |= [A ==> (A.\x:al A)]
Theorem	axext 206*	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.
|- A:(al -> *)   &   |- B:(al -> *)   =>   |- T. |= [(A.\x:al [(Ax:al) = (Bx:al)]) ==> [A = B]]
Theorem	axrep 207*	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19.
|- 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 208*	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory.
|- A:(al -> *)   =>   |- T. |= (E.\y:((al -> *) -> *) (A.\z:(al -> *) [(A.\x:al [(z:(al -> *)x:al) ==> (Ax:al)]) ==> (y:((al -> *) -> *)z:(al -> *))]))
Theorem	axun 209*	Axiom of Union. An axiom of Zermelo-Fraenkel set theory.
|- A:((al -> *) -> *)   =>   |- T. |= (E.\y:(al -> *) (A.\z:al [(E.\x:(al -> *) [(x:(al -> *)z:al) /\ (Ax:(al -> *))]) ==> (y:(al -> *)z:al)]))

< Previous  Wrap >