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:(be -> (ga -> de))   &   |- A:be   &   |- B:al   &   |- C:ga   &   |- R |= [(\x:al FB) = F]   &   |- R |= [(\x:al AB) = A]   &   |- R |= [(\x:al CB) = C]   =>   |- R |= [(\x:al [AFC]B) = [AFC]]
Theorem	hbl 102*	Hypothesis builder for lambda abstraction.
|- A:ga   &   |- B:al   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al \y:be AB) = \y:be 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   &   |- T. |= [(\x:al By:al) = B]   &   |- T. |= [(\x:al Sy:al) = S]   &   |- [x:al = C] |= [A = B]   &   |- [x:al = C] |= [R = S]   =>   |- S |= B
Theorem	insti 104*	Instantiate a theorem with a new term.
|- C:al   &   |- B:*   &   |- R |= A   &   |- T. |= [(\x:al By:al) = B]   &   |- [x:al = C] |= [A = B]   =>   |- R |= B
Theorem	clf 105*	Evaluate a lambda expression.
|- A:be   &   |- C:al   &   |- [x:al = C] |= [A = B]   &   |- T. |= [(\x:al By:al) = B]   &   |- T. |= [(\x:al Cy:al) = C]   =>   |- T. |= [(\x:al AC) = B]
Theorem	cl 106*	Evaluate a lambda expression.
|- A:be   &   |- C:al   &   |- [x:al = C] |= [A = B]   =>   |- T. |= [(\x:al AC) = B]
Theorem	ovl 107*	Evaluate a lambda expression in a binary operation.
|- A:ga   &   |- S:al   &   |- T:be   &   |- [x:al = S] |= [A = B]   &   |- [y:be = T] |= [B = C]   =>   |- T. |= [[S\x:al \y:be AT] = C]
0.2  Add propositional calculus definitions
Syntax	tfal 108	Contradiction term.
term F.
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 A.
Syntax	tex 113	There exists term.
term E.
Syntax	tor 114	Disjunction term.
term \/
Syntax	teu 115	There exists unique term.
term E!
Definition	df-al 116*	Define the for all operator.
|- T. |= [A. = \p:(al -> *) [p:(al -> *) = \x:al T.]]
Definition	df-fal 117	Define the constant false.
|- T. |= [F. = (A.\p:* p:*)]
Definition	df-an 118*	Define the 'and' operator.
|- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Definition	df-im 119*	Define the implication operator.
|- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
Definition	df-not 120	Define the negation operator.
|- T. |= [~ = \p:* [p:* ==> F.]]
Definition	df-ex 121*	Define the existence operator.
|- T. |= [E. = \p:(al -> *) (A.\q:* [(A.\x:al [(p:(al -> *)x:al) ==> q:*]) ==> q:*])]
Definition	df-or 122*	Define the 'or' operator.
|- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
Definition	df-eu 123*	Define the 'exists unique' operator.
|- T. |= [E! = \p:(al -> *) (E.\y:al (A.\x:al [(p:(al -> *)x:al) = [x:al = y:al]]))]
Theorem	wal 124	For all type.
|- A.:((al -> *) -> *)
Theorem	wfal 125	Contradiction type.
|- F.:*
Theorem	wan 126	Conjunction type.
|- /\ :(* -> (* -> *))
Theorem	wim 127	Implication type.
|- ==> :(* -> (* -> *))
Theorem	wnot 128	Negation type.
|- ~ :(* -> *)
Theorem	wex 129	There exists type.
|- E.:((al -> *) -> *)
Theorem	wor 130	Disjunction type.
|- \/ :(* -> (* -> *))
Theorem	weu 131	There exists unique type.
|- E!:((al -> *) -> *)
Theorem	alval 132*	Value of the for all predicate.
|- F:(al -> *)   =>   |- T. |= [(A.F) = [F = \x:al T.]]
Theorem	exval 133*	Value of the 'there exists' predicate.
|- F:(al -> *)   =>   |- T. |= [(E.F) = (A.\q:* [(A.\x:al [(Fx:al) ==> q:*]) ==> q:*])]
Theorem	euval 134*	Value of the 'exists unique' predicate.
|- F:(al -> *)   =>   |- T. |= [(E!F) = (E.\y:al (A.\x:al [(Fx:al) = [x:al = y:al]]))]
Theorem	notval 135	Value of negation.
|- A:*   =>   |- T. |= [(~ A) = [A ==> F.]]
Theorem	imval 136	Value of the implication.
|- A:*   &   |- B:*   =>   |- T. |= [[A ==> B] = [[A /\ B] = A]]
Theorem	orval 137*	Value of the disjunction.
|- A:*   &   |- B:*   =>   |- T. |= [[A \/ B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
Theorem	anval 138*	Value of the conjunction.
|- A:*   &   |- B:*   =>   |- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Theorem	ax4g 139	If F is true for all x:al, then it is true for A.
|- F:(al -> *)   &   |- A:al   =>   |- (A.F) |= (FA)
Theorem	ax4 140	If A is true for all x:al, then it is true for A.
|- A:*   =>   |- (A.\x:al 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 |= (A.\x:al A)
Theorem	cla4v 142*	If A(x) is true for all x:al, then it is true for C = A(B).
|- A:*   &   |- B:al   &   |- [x:al = B] |= [A = C]   =>   |- (A.\x:al A) |= C
Theorem	pm2.21 143	A falsehood implies anything.
|- A:*   =>   |- F. |= A
Theorem	dfan2 144	An alternative defintion of the "and" term in terms of the context conjunction.
|- A:*   &   |- B:*   =>   |- T. |= [[A /\ B] = (A, B)]
Theorem	hbct 145	Hypothesis builder for context conjunction.
|- A:*   &   |- B:al   &   |- C:*   &   |- R |= [(\x:al AB) = A]   &   |- R |= [(\x:al CB) = C]   =>   |- R |= [(\x:al (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:*   =>   |- T. |= [(~ A) = [A = F.]]
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:(al -> *)   &   |- (R, (Fx:al)) |= T   =>   |- (R, (E.F)) |= T
Theorem	exlimdv 157*	Existential elimination.
|- (R, A) |= T   =>   |- (R, (E.\x:al A)) |= T
Theorem	ax4e 158	Existential introduction.
|- F:(al -> *)   &   |- A:al   =>   |- (FA) |= (E.F)
Theorem	cla4ev 159*	Existential introduction.
|- A:*   &   |- B:al   &   |- [x:al = B] |= [A = C]   =>   |- C |= (E.\x:al A)
Theorem	19.8a 160	Existential introduction.
|- A:*   =>   |- A |= (E.\x:al A)
0.3  Type definition mechanism
Syntax	wffMMJ2d 161	Internal axiom for mmj2 use.
wff typedef al(A, B)C
Syntax	wabs 162	Type of the abstraction function.
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- A:(al -> be)
Syntax	wrep 163	Type of the representation function.
|- B:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- R:(be -> al)
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 be and the definition will provide us with pair of bijections A, R mapping the new type be to the subset of the old type al 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:al   &   |- F:(al -> *)   &   |- T. |= (FB)   &   |- typedef be(A, R)F   =>   |- T. |= ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))
0.4  Extensionality
Axiom	ax-eta 165*	The eta-axiom: a function is determined by its values.
|- T. |= (A.\f:(al -> be) [\x:al (f:(al -> be)x:al) = f:(al -> be)])
Theorem	eta 166*	The eta-axiom: a function is determined by its values.
|- F:(al -> be)   =>   |- T. |= [\x:al (Fx:al) = F]
Theorem	cbvf 167*	Change bound variables in a lambda abstraction.
|- A:be   &   |- T. |= [(\y:al Az:al) = A]   &   |- T. |= [(\x:al Bz:al) = B]   &   |- [x:al = y:al] |= [A = B]   =>   |- T. |= [\x:al A = \y:al B]
Theorem	cbv 168*	Change bound variables in a lambda abstraction.
|- A:be   &   |- [x:al = y:al] |= [A = B]   =>   |- T. |= [\x:al A = \y:al B]
Theorem	leqf 169*	Equality theorem for lambda abstraction, using bound variable instead of distinct variables.
|- A:be   &   |- R |= [A = B]   &   |- T. |= [(\x:al Ry:al) = R]   =>   |- R |= [\x:al A = \x:al 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   &   |- T. |= [(\x:al Ry:al) = R]   =>   |- R |= (A.\x:al A)
Theorem	exlimd 171*	Existential elimination.
|- (R, A) |= T   &   |- T. |= [(\x:al Ry:al) = R]   &   |- T. |= [(\x:al Ty:al) = T]   =>   |- (R, (E.\x:al A)) |= T
Theorem	alimdv 172*	Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (R, A) |= B   =>   |- (R, (A.\x:al A)) |= (A.\x:al B)
Theorem	eximdv 173*	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (R, A) |= B   =>   |- (R, (E.\x:al A)) |= (E.\x:al B)
Theorem	alnex 174*	Theorem 19.7 of [Margaris] p. 89.
|- A:*   =>   |- T. |= [(A.\x:al (~ A)) = (~ (E.\x:al A))]
Theorem	exnal1 175*	Forward direction of exnal 188.
|- A:*   =>   |- (E.\x:al (~ A)) |= (~ (A.\x:al A))
Theorem	isfree 176*	Derive the metamath "is free" predicate in terms of the HOL "is free" predicate.
|- A:*   &   |- T. |= [(\x:al Ay:al) = A]   =>   |- T. |= [A ==> (A.\x:al 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.
|- @:((al -> *) -> al)
Definition	df-f11 181*	Define a one-to-one function.
|- T. |= [1-1 = \f:(al -> be) (A.\x:al (A.\y:al [[(f:(al -> be)x:al) = (f:(al -> be)y:al)] ==> [x:al = y:al]]))]
Definition	df-fo 182*	Define an onto function.
|- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
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.
|- T. |= (A.\p:(al -> *) (A.\x:al [(p:(al -> *)x:al) ==> (p:(al -> *)(@p:(al -> *)))]))
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:(al -> *)   &   |- A:al   =>   |- (FA) |= (F(@F))
Theorem	dfex2 185	Alternative definition of the "there exists" quantifier.
|- F:(al -> *)   =>   |- T. |= [(E.F) = (F(@F))]
Theorem	exmid 186	Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice.
|- A:*   =>   |- T. |= [A \/ (~ A)]
Theorem	notnot 187	Rule of double negation.
|- A:*   =>   |- T. |= [A = (~ (~ A))]
Theorem	exnal 188*	Theorem 19.14 of [Margaris] p. 90.
|- A:*   =>   |- T. |= [(E.\x:al (~ A)) = (~ (A.\x:al 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 iota.
|- T. |= (E.\f:(iota -> iota) [(1-1 f:(iota -> iota)) /\ (~ (onto f:(iota -> iota)))])
0.6  Rederive the Metamath axioms
Theorem	ax1 190	Axiom Simp. Axiom A1 of [Margaris] p. 49.
|- R:*   &   |- S:*   =>   |- T. |= [R ==> [S ==> R]]
Theorem	ax2 191	Axiom Frege. Axiom A2 of [Margaris] p. 49.
|- R:*   &   |- S:*   &   |- T:*   =>   |- T. |= [[R ==> [S ==> T]] ==> [[R ==> S] ==> [R ==> T]]]
Theorem	ax3 192	Axiom Transp. Axiom A3 of [Margaris] p. 49.
|- R:*   &   |- S:*   =>   |- T. |= [[(~ 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:*   &   |- T. |= R   &   |- T. |= [R ==> S]   =>   |- T. |= S
Theorem	ax5 194*	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
|- R:*   &   |- S:*   =>   |- T. |= [(A.\x:al [R ==> S]) ==> [(A.\x:al R) ==> (A.\x:al S)]]
Theorem	ax6 195*	Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.
|- R:*   =>   |- T. |= [(~ (A.\x:al R)) ==> (A.\x:al (~ (A.\x:al R)))]
Theorem	ax7 196*	Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint).
|- R:*   =>   |- T. |= [(A.\x:al (A.\y:al R)) ==> (A.\y:al (A.\x:al R))]
Theorem	axgen 197*	Rule of Generalization. See e.g. Rule 2 of [Hamilton] p. 74.
|- T. |= R   =>   |- T. |= (A.\x:al 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:al   &   |- B:al   &   |- C:al   =>   |- T. |= [[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:al   =>   |- T. |= (~ (A.\x:al (~ [x:al = A])))
Theorem	ax10 200*	Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).
|- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]