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:α)])) |