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:∗    ⇒   ⊢ ⊤⊧[[x:α = y:α] ⇒ [(∀λy:α A) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]]
Theorem	ax12 202*	Axiom of Quantifier Introduction. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint).
⊢ ⊤⊧[(¬ (∀λz:α [z:α = x:α])) ⇒ [(¬ (∀λz:α [z:α = y:α])) ⇒ [[x:α = y:α] ⇒ (∀λz:α [x:α = y:α])]]]
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:α    &   ⊢ B:α    &   ⊢ C:(α → ∗)    ⇒   ⊢ ⊤⊧[[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:(α → ∗)    &   ⊢ B:(α → ∗)    &   ⊢ C:α    ⇒   ⊢ ⊤⊧[[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:∗    ⇒   ⊢ ⊤⊧[A ⇒ (∀λx:α 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:(α → ∗)    &   ⊢ B:(α → ∗)    ⇒   ⊢ ⊤⊧[(∀λx:α [(Ax:α) = (Bx:α)]) ⇒ [A = B]]
Theorem	axrep 207*	Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory. Axiom 5 of [TakeutiZaring] p. 19.
⊢ A:∗    &   ⊢ B:(α → ∗)    ⇒   ⊢ ⊤⊧[(∀λx:α (∃λy:β (∀λz:β [(∀λy:β A) ⇒ [z:β = y:β]]))) ⇒ (∃λy:(β → ∗) (∀λz:β [(y:(β → ∗)z:β) = (∃λx:α [(Bx:α) ∧ (∀λy:β A)])]))]
Theorem	axpow 208*	Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory.
⊢ A:(α → ∗)    ⇒   ⊢ ⊤⊧(∃λy:((α → ∗) → ∗) (∀λz:(α → ∗) [(∀λx:α [(z:(α → ∗)x:α) ⇒ (Ax:α)]) ⇒ (y:((α → ∗) → ∗)z:(α → ∗))]))
Theorem	axun 209*	Axiom of Union. An axiom of Zermelo-Fraenkel set theory.
⊢ A:((α → ∗) → ∗)    ⇒   ⊢ ⊤⊧(∃λy:(α → ∗) (∀λz:α [(∃λx:(α → ∗) [(x:(α → ∗)z:α) ∧ (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]))

< Previous  Wrap >