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

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