Theorem List for Higher-Order Logic Explorer - 101-200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | hbov 101 |
Hypothesis builder for binary operation.
|
⊢ F:(β → (γ → δ))
& ⊢ A:β
& ⊢ B:α
& ⊢ C:γ
& ⊢ R⊧[(λx:α
FB) =
F]
& ⊢ R⊧[(λx:α
AB) =
A]
& ⊢ R⊧[(λx:α
CB) =
C] ⇒ ⊢ R⊧[(λx:α
[AFC]B) = [AFC]] |
|
Theorem | hbl 102* |
Hypothesis builder for lambda abstraction.
|
⊢ A:γ
& ⊢ B:α
& ⊢ R⊧[(λx:α
AB) =
A] ⇒ ⊢ R⊧[(λx:α
λy:β AB) =
λy:β A] |
|
Axiom | ax-inst 103* |
Instantiate a theorem with a new term. The second and third hypotheses
are the HOL equivalent of set.mm "effectively not free in"
predicate
(see set.mm's ax-17, or ax17 205).
|
⊢ R⊧A
& ⊢ ⊤⊧[(λx:α
By:α) =
B]
& ⊢ ⊤⊧[(λx:α
Sy:α) =
S]
& ⊢ [x:α = C]⊧[A =
B]
& ⊢ [x:α = C]⊧[R =
S] ⇒ ⊢ S⊧B |
|
Theorem | insti 104* |
Instantiate a theorem with a new term.
|
⊢ C:α
& ⊢ B:∗
& ⊢ R⊧A
& ⊢ ⊤⊧[(λx:α
By:α) =
B]
& ⊢ [x:α = C]⊧[A =
B] ⇒ ⊢ R⊧B |
|
Theorem | clf 105* |
Evaluate a lambda expression.
|
⊢ A:β
& ⊢ C:α
& ⊢ [x:α = C]⊧[A =
B]
& ⊢ ⊤⊧[(λx:α
By:α) =
B]
& ⊢ ⊤⊧[(λx:α
Cy:α) =
C] ⇒ ⊢ ⊤⊧[(λx:α
AC) =
B] |
|
Theorem | cl 106* |
Evaluate a lambda expression.
|
⊢ A:β
& ⊢ C:α
& ⊢ [x:α = C]⊧[A =
B] ⇒ ⊢ ⊤⊧[(λx:α
AC) =
B] |
|
Theorem | ovl 107* |
Evaluate a lambda expression in a binary operation.
|
⊢ A:γ
& ⊢ S:α
& ⊢ T:β
& ⊢ [x:α = S]⊧[A =
B]
& ⊢ [y:β = T]⊧[B =
C] ⇒ ⊢ ⊤⊧[[Sλx:α
λy:β AT] = C] |
|
0.2 Add propositional calculus
definitions
|
|
Syntax | tfal 108 |
Contradiction term.
|
term
⊥ |
|
Syntax | tan 109 |
Conjunction term.
|
term
∧ |
|
Syntax | tne 110 |
Negation term.
|
term
¬ |
|
Syntax | tim 111 |
Implication term.
|
term
⇒ |
|
Syntax | tal 112 |
For all term.
|
term
∀ |
|
Syntax | tex 113 |
There exists term.
|
term
∃ |
|
Syntax | tor 114 |
Disjunction term.
|
term
∨ |
|
Syntax | teu 115 |
There exists unique term.
|
term
∃! |
|
Definition | df-al 116* |
Define the for all operator.
|
⊢ ⊤⊧[∀ = λp:(α
→ ∗) [p:(α → ∗) =
λx:α ⊤]] |
|
Definition | df-fal 117 |
Define the constant false.
|
⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)] |
|
Definition | df-an 118* |
Define the 'and' operator.
|
⊢ ⊤⊧[ ∧ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗))
[p:∗f:(∗ → (∗ →
∗))q:∗] =
λf:(∗ →
(∗ → ∗)) [⊤f:(∗ → (∗ →
∗))⊤]]] |
|
Definition | df-im 119* |
Define the implication operator.
|
⊢ ⊤⊧[ ⇒ =
λp:∗
λq:∗ [[p:∗ ∧
q:∗] = p:∗]] |
|
Definition | df-not 120 |
Define the negation operator.
|
⊢ ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]] |
|
Definition | df-ex 121* |
Define the existence operator.
|
⊢ ⊤⊧[∃ = λp:(α
→ ∗) (∀λq:∗ [(∀λx:α
[(p:(α → ∗)x:α)
⇒ q:∗]) ⇒ q:∗])] |
|
Definition | df-or 122* |
Define the 'or' operator.
|
⊢ ⊤⊧[
∨ = λp:∗
λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])] |
|
Definition | df-eu 123* |
Define the 'exists unique' operator.
|
⊢ ⊤⊧[∃! = λp:(α
→ ∗) (∃λy:α
(∀λx:α
[(p:(α → ∗)x:α) =
[x:α = y:α]]))] |
|
Theorem | wal 124 |
For all type.
|
⊢ ∀:((α → ∗) →
∗) |
|
Theorem | wfal 125 |
Contradiction type.
|
⊢ ⊥:∗ |
|
Theorem | wan 126 |
Conjunction type.
|
⊢ ∧ :(∗
→ (∗ → ∗)) |
|
Theorem | wim 127 |
Implication type.
|
⊢ ⇒ :(∗ → (∗ →
∗)) |
|
Theorem | wnot 128 |
Negation type.
|
⊢ ¬ :(∗ →
∗) |
|
Theorem | wex 129 |
There exists type.
|
⊢ ∃:((α → ∗) →
∗) |
|
Theorem | wor 130 |
Disjunction type.
|
⊢ ∨ :(∗
→ (∗ → ∗)) |
|
Theorem | weu 131 |
There exists unique type.
|
⊢ ∃!:((α → ∗) →
∗) |
|
Theorem | alval 132* |
Value of the for all predicate.
|
⊢ F:(α →
∗) ⇒ ⊢ ⊤⊧[(∀F) =
[F = λx:α
⊤]] |
|
Theorem | exval 133* |
Value of the 'there exists' predicate.
|
⊢ F:(α →
∗) ⇒ ⊢ ⊤⊧[(∃F) = (∀λq:∗ [(∀λx:α
[(Fx:α)
⇒ q:∗]) ⇒ q:∗])] |
|
Theorem | euval 134* |
Value of the 'exists unique' predicate.
|
⊢ F:(α →
∗) ⇒ ⊢ ⊤⊧[(∃!F) = (∃λy:α
(∀λx:α
[(Fx:α) =
[x:α = y:α]]))] |
|
Theorem | notval 135 |
Value of negation.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[(¬ A) = [A ⇒
⊥]] |
|
Theorem | imval 136 |
Value of the implication.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ ⊤⊧[[A ⇒ B] =
[[A ∧
B] = A]] |
|
Theorem | orval 137* |
Value of the disjunction.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ ⊤⊧[[A ∨ B] = (∀λx:∗ [[A
⇒ x:∗] ⇒ [[B ⇒ x:∗] ⇒ x:∗]])] |
|
Theorem | anval 138* |
Value of the conjunction.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ ⊤⊧[[A ∧ B] = [λf:(∗ → (∗ → ∗))
[Af:(∗ → (∗ →
∗))B] = λf:(∗ → (∗ → ∗))
[⊤f:(∗ → (∗
→ ∗))⊤]]] |
|
Theorem | ax4g 139 |
If F is true for all x:α, then it is true for A.
|
⊢ F:(α → ∗) & ⊢ A:α ⇒ ⊢ (∀F)⊧(FA) |
|
Theorem | ax4 140 |
If A is true for all x:α, then it is true for A.
|
⊢ A:∗ ⇒ ⊢ (∀λx:α
A)⊧A |
|
Theorem | alrimiv 141* |
If one can prove R⊧A where R does not contain x, then
A is true for all
x.
|
⊢ R⊧A ⇒ ⊢ R⊧(∀λx:α
A) |
|
Theorem | cla4v 142* |
If A(x) is true for all x:α, then it is true for
C = A(B).
|
⊢ A:∗
& ⊢ B:α
& ⊢ [x:α = B]⊧[A =
C] ⇒ ⊢ (∀λx:α
A)⊧C |
|
Theorem | pm2.21 143 |
A falsehood implies anything.
|
⊢ A:∗ ⇒ ⊢ ⊥⊧A |
|
Theorem | dfan2 144 |
An alternative defintion of the "and" term in terms of the context
conjunction.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ ⊤⊧[[A ∧ B] = (A,
B)] |
|
Theorem | hbct 145 |
Hypothesis builder for context conjunction.
|
⊢ A:∗
& ⊢ B:α
& ⊢ C:∗
& ⊢ R⊧[(λx:α
AB) =
A]
& ⊢ R⊧[(λx:α
CB) =
C] ⇒ ⊢ R⊧[(λx:α
(A, C)B) =
(A, C)] |
|
Theorem | mpd 146 |
Modus ponens.
|
⊢ T:∗
& ⊢ R⊧S
& ⊢ R⊧[S
⇒ T] ⇒ ⊢ R⊧T |
|
Theorem | imp 147 |
Importation deduction.
|
⊢ S:∗
& ⊢ T:∗
& ⊢ R⊧[S
⇒ T] ⇒ ⊢ (R,
S)⊧T |
|
Theorem | ex 148 |
Exportation deduction.
|
⊢ (R,
S)⊧T ⇒ ⊢ R⊧[S
⇒ T] |
|
Theorem | notval2 149 |
Another way two write ¬ A, the negation of A.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[(¬ A) = [A =
⊥]] |
|
Theorem | notnot1 150 |
One side of notnot 187.
|
⊢ A:∗ ⇒ ⊢ A⊧(¬ (¬ A)) |
|
Theorem | con2d 151 |
A contraposition deduction.
|
⊢ T:∗
& ⊢ (R,
S)⊧(¬ T) ⇒ ⊢ (R,
T)⊧(¬ S) |
|
Theorem | con3d 152 |
A contraposition deduction.
|
⊢ (R,
S)⊧T ⇒ ⊢ (R, (¬
T))⊧(¬ S) |
|
Theorem | ecase 153 |
Elimination by cases.
|
⊢ A:∗
& ⊢ B:∗
& ⊢ T:∗
& ⊢ R⊧[A
∨ B]
& ⊢ (R,
A)⊧T
& ⊢ (R,
B)⊧T ⇒ ⊢ R⊧T |
|
Theorem | olc 154 |
Or introduction.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ B⊧[A
∨ B] |
|
Theorem | orc 155 |
Or introduction.
|
⊢ A:∗
& ⊢ B:∗ ⇒ ⊢ A⊧[A
∨ B] |
|
Theorem | exlimdv2 156* |
Existential elimination.
|
⊢ F:(α → ∗) & ⊢ (R,
(Fx:α))⊧T ⇒ ⊢ (R, (∃F))⊧T |
|
Theorem | exlimdv 157* |
Existential elimination.
|
⊢ (R,
A)⊧T ⇒ ⊢ (R, (∃λx:α
A))⊧T |
|
Theorem | ax4e 158 |
Existential introduction.
|
⊢ F:(α → ∗) & ⊢ A:α ⇒ ⊢ (FA)⊧(∃F) |
|
Theorem | cla4ev 159* |
Existential introduction.
|
⊢ A:∗
& ⊢ B:α
& ⊢ [x:α = B]⊧[A =
C] ⇒ ⊢ C⊧(∃λx:α
A) |
|
Theorem | 19.8a 160 |
Existential introduction.
|
⊢ A:∗ ⇒ ⊢ A⊧(∃λx:α
A) |
|
0.3 Type definition mechanism
|
|
Syntax | wffMMJ2d 161 |
Internal axiom for mmj2 use.
|
wff
typedef α(A, B)C |
|
Syntax | wabs 162 |
Type of the abstraction function.
|
⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ A:(α → β) |
|
Syntax | wrep 163 |
Type of the representation function.
|
⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ R:(β → α) |
|
Axiom | ax-tdef 164* |
The type definition axiom. The last hypothesis corresponds to the actual
definition one wants to make; here we are defining a new type β and
the definition will provide us with pair of bijections A, R
mapping
the new type β to
the subset of the old type α such that
Fx is true. In order for this to be a valid
(conservative)
extension, we must ensure that the new type is non-empty, and for that
purpose we need a witness B that F is not always false.
|
⊢ B:α
& ⊢ F:(α → ∗) & ⊢ ⊤⊧(FB) & ⊢ typedef β(A,
R)F ⇒ ⊢ ⊤⊧((∀λx:β
[(A(Rx:β)) = x:β]),
(∀λx:α
[(Fx:α) =
[(R(Ax:α)) = x:α]])) |
|
0.4 Extensionality
|
|
Axiom | ax-eta 165* |
The eta-axiom: a function is determined by its values.
|
⊢ ⊤⊧(∀λf:(α
→ β) [λx:α
(f:(α → β)x:α) =
f:(α → β)]) |
|
Theorem | eta 166* |
The eta-axiom: a function is determined by its values.
|
⊢ F:(α → β) ⇒ ⊢ ⊤⊧[λx:α
(Fx:α) =
F] |
|
Theorem | cbvf 167* |
Change bound variables in a lambda abstraction.
|
⊢ A:β
& ⊢ ⊤⊧[(λy:α
Az:α) =
A]
& ⊢ ⊤⊧[(λx:α
Bz:α) =
B]
& ⊢ [x:α = y:α]⊧[A = B] ⇒ ⊢ ⊤⊧[λx:α
A = λy:α
B] |
|
Theorem | cbv 168* |
Change bound variables in a lambda abstraction.
|
⊢ A:β
& ⊢ [x:α = y:α]⊧[A = B] ⇒ ⊢ ⊤⊧[λx:α
A = λy:α
B] |
|
Theorem | leqf 169* |
Equality theorem for lambda abstraction, using bound variable instead of
distinct variables.
|
⊢ A:β
& ⊢ R⊧[A =
B]
& ⊢ ⊤⊧[(λx:α
Ry:α) =
R] ⇒ ⊢ R⊧[λx:α
A = λx:α
B] |
|
Theorem | alrimi 170* |
If one can prove R⊧A where R does not contain x, then
A is true for all
x.
|
⊢ R⊧A
& ⊢ ⊤⊧[(λx:α
Ry:α) =
R] ⇒ ⊢ R⊧(∀λx:α
A) |
|
Theorem | exlimd 171* |
Existential elimination.
|
⊢ (R,
A)⊧T
& ⊢ ⊤⊧[(λx:α
Ry:α) =
R]
& ⊢ ⊤⊧[(λx:α
Ty:α) =
T] ⇒ ⊢ (R, (∃λx:α
A))⊧T |
|
Theorem | alimdv 172* |
Deduction from Theorem 19.20 of [Margaris] p.
90.
|
⊢ (R,
A)⊧B ⇒ ⊢ (R, (∀λx:α
A))⊧(∀λx:α
B) |
|
Theorem | eximdv 173* |
Deduction from Theorem 19.22 of [Margaris] p.
90.
|
⊢ (R,
A)⊧B ⇒ ⊢ (R, (∃λx:α
A))⊧(∃λx:α
B) |
|
Theorem | alnex 174* |
Theorem 19.7 of [Margaris] p. 89.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[(∀λx:α
(¬ A)) = (¬ (∃λx:α
A))] |
|
Theorem | exnal1 175* |
Forward direction of exnal 188.
|
⊢ A:∗ ⇒ ⊢ (∃λx:α
(¬ A))⊧(¬ (∀λx:α
A)) |
|
Theorem | isfree 176* |
Derive the metamath "is free" predicate in terms of the HOL "is
free"
predicate.
|
⊢ A:∗
& ⊢ ⊤⊧[(λx:α
Ay:α) =
A] ⇒ ⊢ ⊤⊧[A ⇒ (∀λx:α
A)] |
|
0.5 Axioms of infinity and
choice
|
|
Syntax | tf11 177 |
One-to-one function.
|
term
1-1 |
|
Syntax | tfo 178 |
Onto function.
|
term
onto |
|
Syntax | tat 179 |
Indefinite descriptor.
|
term
ε |
|
Syntax | wat 180 |
The type of the indefinite descriptor.
|
⊢ ε:((α → ∗) → α) |
|
Definition | df-f11 181* |
Define a one-to-one function.
|
⊢ ⊤⊧[1-1 = λf:(α
→ β) (∀λx:α
(∀λy:α
[[(f:(α → β)x:α) =
(f:(α → β)y:α)]
⇒ [x:α = y:α]]))] |
|
Definition | df-fo 182* |
Define an onto function.
|
⊢ ⊤⊧[onto = λf:(α
→ β) (∀λy:β (∃λx:α
[y:β = (f:(α
→ β)x:α)]))] |
|
Axiom | ax-ac 183* |
Defining property of the indefinite descriptor: it selects an element
from any type. This is equivalent to global choice in ZF.
|
⊢ ⊤⊧(∀λp:(α
→ ∗) (∀λx:α
[(p:(α → ∗)x:α)
⇒ (p:(α → ∗)(εp:(α
→ ∗)))])) |
|
Theorem | ac 184 |
Defining property of the indefinite descriptor: it selects an element
from any type. This is equivalent to global choice in ZF.
|
⊢ F:(α → ∗) & ⊢ A:α ⇒ ⊢ (FA)⊧(F(εF)) |
|
Theorem | dfex2 185 |
Alternative definition of the "there exists" quantifier.
|
⊢ F:(α →
∗) ⇒ ⊢ ⊤⊧[(∃F) =
(F(εF))] |
|
Theorem | exmid 186 |
Diaconescu's theorem, which derives the law of the excluded middle from
the axiom of choice.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[A ∨ (¬
A)] |
|
Theorem | notnot 187 |
Rule of double negation.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[A = (¬ (¬ A))] |
|
Theorem | exnal 188* |
Theorem 19.14 of [Margaris] p. 90.
|
⊢ A:∗ ⇒ ⊢ ⊤⊧[(∃λx:α
(¬ A)) = (¬ (∀λx:α
A))] |
|
Axiom | ax-inf 189 |
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 ι.
|
⊢ ⊤⊧(∃λf:(ι → ι) [(1-1 f:(ι → ι)) ∧ (¬ (onto f:(ι → ι)))]) |
|
0.6 Rederive the Metamath
axioms
|
|
Theorem | ax1 190 |
Axiom Simp. Axiom A1 of [Margaris] p.
49.
|
⊢ R:∗
& ⊢ S:∗ ⇒ ⊢ ⊤⊧[R ⇒ [S
⇒ R]] |
|
Theorem | ax2 191 |
Axiom Frege. Axiom A2 of [Margaris]
p. 49.
|
⊢ R:∗
& ⊢ S:∗
& ⊢ T:∗ ⇒ ⊢ ⊤⊧[[R ⇒ [S
⇒ T]] ⇒ [[R ⇒ S]
⇒ [R ⇒ T]]] |
|
Theorem | ax3 192 |
Axiom Transp. Axiom A3 of [Margaris]
p. 49.
|
⊢ R:∗
& ⊢ S:∗ ⇒ ⊢ ⊤⊧[[(¬ R) ⇒ (¬ S)] ⇒ [S
⇒ R]] |
|
Theorem | axmp 193 |
Rule of Modus Ponens. The postulated inference rule of propositional
calculus. See e.g. Rule 1 of [Hamilton] p. 73.
|
⊢ S:∗
& ⊢ ⊤⊧R
& ⊢ ⊤⊧[R ⇒ S] ⇒ ⊢ ⊤⊧S |
|
Theorem | ax5 194* |
Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
|
⊢ R:∗
& ⊢ S:∗ ⇒ ⊢ ⊤⊧[(∀λx:α
[R ⇒ S]) ⇒ [(∀λx:α
R) ⇒ (∀λx:α
S)]] |
|
Theorem | ax6 195* |
Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.
|
⊢ R:∗ ⇒ ⊢ ⊤⊧[(¬ (∀λx:α
R)) ⇒ (∀λx:α
(¬ (∀λx:α
R)))] |
|
Theorem | ax7 196* |
Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448
(p. 16 of the preprint).
|
⊢ R:∗ ⇒ ⊢ ⊤⊧[(∀λx:α
(∀λy:α
R)) ⇒ (∀λy:α
(∀λx:α
R))] |
|
Theorem | axgen 197* |
Rule of Generalization. See e.g. Rule 2 of [Hamilton] p. 74.
|
⊢ ⊤⊧R ⇒ ⊢ ⊤⊧(∀λx:α
R) |
|
Theorem | ax8 198 |
Axiom of Equality. Axiom scheme C8' in [Megill] p. 448
(p. 16 of the preprint). Also appears as Axiom C7 of
[Monk2] p. 105.
|
⊢ A:α
& ⊢ B:α
& ⊢ C:α ⇒ ⊢ ⊤⊧[[A = B] ⇒
[[A = C] ⇒ [B =
C]]] |
|
Theorem | ax9 199* |
Axiom of Equality. Axiom scheme C8' in [Megill] p. 448
(p. 16 of the preprint). Also appears as Axiom C7 of
[Monk2] p. 105.
|
⊢ A:α ⇒ ⊢ ⊤⊧(¬ (∀λx:α
(¬ [x:α = A]))) |
|
Theorem | ax10 200* |
Axiom of Quantifier Substitution. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
|
⊢ ⊤⊧[(∀λx:α
[x:α = y:α])
⇒ (∀λy:α
[y:α = x:α])] |