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

Theorem List for Higher-Order Logic Explorer - 1-100   *Has distinct variable group(s)

Type	Label	Description
Statement
0.1  Foundations
Syntax	tv 1	A var is a term.
term x:al
Syntax	ht 2	The type of all functions from type al to type be.
type (al -> be)
Syntax	hb 3	The type of booleans (true and false).
type *
Syntax	hi 4	The type of individuals.
type iota
Syntax	kc 5	A combination (function application).
term (FT)
Syntax	kl 6	A lambda abstraction.
term \x:al T
Syntax	ke 7	The equality term.
term =
Syntax	kt 8	Truth term.
term T.
Syntax	kbr 9	Infix operator.
term [AFB]
Syntax	kct 10	Context operator.
term (A, B)
Syntax	wffMMJ2 11	Internal axiom for mmj2 use.
wff A |= B
Syntax	wffMMJ2t 12	Internal axiom for mmj2 use.
wff A:al
Theorem	idi 13	The identity inference.
|- R |= A   =>   |- R |= A
Theorem	idt 14	The identity inference.
|- A:al   =>   |- A:al
Axiom	ax-syl 15	Syllogism inference.
|- R |= S   &   |- S |= T   =>   |- R |= T
Theorem	syl 16	Syllogism inference.
|- R |= S   &   |- S |= T   =>   |- R |= T
Axiom	ax-jca 17	Join common antecedents.
|- R |= S   &   |- R |= T   =>   |- R |= (S, T)
Theorem	jca 18	Syllogism inference.
|- R |= S   &   |- R |= T   =>   |- R |= (S, T)
Theorem	syl2anc 19	Syllogism inference.
|- R |= S   &   |- R |= T   &   |- (S, T) |= A   =>   |- R |= A
Axiom	ax-simpl 20	Extract an assumption from the context.
|- R:*   &   |- S:*   =>   |- (R, S) |= R
Axiom	ax-simpr 21	Extract an assumption from the context.
|- R:*   &   |- S:*   =>   |- (R, S) |= S
Theorem	simpl 22	Extract an assumption from the context.
|- R:*   &   |- S:*   =>   |- (R, S) |= R
Theorem	simpr 23	Extract an assumption from the context.
|- R:*   &   |- S:*   =>   |- (R, S) |= S
Axiom	ax-id 24	The identity inference.
|- R:*   =>   |- R |= R
Theorem	id 25	The identity inference.
|- R:*   =>   |- R |= R
Axiom	ax-trud 26	Deduction form of tru 41.
|- R:*   =>   |- R |= T.
Theorem	trud 27	Deduction form of tru 41.
|- R:*   =>   |- R |= T.
Theorem	a1i 28	Change an empty context into any context.
|- R:*   &   |- T. |= A   =>   |- R |= A
Axiom	ax-cb1 29	A context has type boolean. This and the next few axioms are not strictly necessary, and are conservative on any theorem for which every variable has a specified type, but by adding this axiom we can save some typehood hypotheses in many theorems. The easy way to see that this axiom is conservative is to note that every axiom and inference rule that constructs a theorem of the form R |= A where R and A are type variables, also ensures that R:* and A:*. Thus it is impossible to prove any theorem |- R |= A unless both |- R:* and |- A:* had been previously derived, so it is conservative to deduce |- R:* from |- R |= A. The same remark applies to the construction of the theorem (A, B):*- there is only one rule that creates a formula of this type, namely wct 44, and it requires that A:* and B:* be previously established, so it is safe to reverse the process in wctl 31 and wctr 32.
|- R |= A   =>   |- R:*
Axiom	ax-cb2 30	A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.)
|- R |= A   =>   |- A:*
Syntax	wctl 31	Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)
|- (S, T):*   =>   |- S:*
Syntax	wctr 32	Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)
|- (S, T):*   =>   |- T:*
Theorem	mpdan 33	Modus ponens deduction.
|- R |= S   &   |- (R, S) |= T   =>   |- R |= T
Theorem	syldan 34	Syllogism inference.
|- (R, S) |= T   &   |- (R, T) |= A   =>   |- (R, S) |= A
Theorem	simpld 35	Extract an assumption from the context.
|- R |= (S, T)   =>   |- R |= S
Theorem	simprd 36	Extract an assumption from the context.
|- R |= (S, T)   =>   |- R |= T
Theorem	trul 37	Deduction form of tru 41.
|- (T., R) |= S   =>   |- R |= S
Syntax	weq 38	The equality function has type al -> al -> *, i.e. it is polymorphic over all types, but the left and right type must agree.
|- = :(al -> (al -> *))
Axiom	ax-refl 39	Reflexivity of equality.
|- A:al   =>   |- T. |= (( = A)A)
Theorem	wtru 40	Truth type.
|- T.:*
Theorem	tru 41	Tautology is provable.
|- T. |= T.
Axiom	ax-eqmp 42	Modus ponens for equality.
|- R |= A   &   |- R |= (( = A)B)   =>   |- R |= B
Axiom	ax-ded 43	Deduction theorem for equality.
|- (R, S) |= T   &   |- (R, T) |= S   =>   |- R |= (( = S)T)
Syntax	wct 44	The type of a context.
|- S:*   &   |- T:*   =>   |- (S, T):*
Syntax	wc 45	The type of a combination.
|- F:(al -> be)   &   |- T:al   =>   |- (FT):be
Axiom	ax-ceq 46	Equality theorem for combination.
|- F:(al -> be)   &   |- T:(al -> be)   &   |- A:al   &   |- B:al   =>   |- ((( = F)T), (( = A)B)) |= (( = (FA))(TB))
Theorem	eqcomx 47	Commutativity of equality.
|- A:al   &   |- B:al   &   |- R |= (( = A)B)   =>   |- R |= (( = B)A)
Theorem	mpbirx 48	Deduction from equality inference.
|- B:*   &   |- R |= A   &   |- R |= (( = B)A)   =>   |- R |= B
Theorem	ancoms 49	Swap the two elements of a context.
|- (R, S) |= T   =>   |- (S, R) |= T
Theorem	adantr 50	Extract an assumption from the context.
|- R |= T   &   |- S:*   =>   |- (R, S) |= T
Theorem	adantl 51	Extract an assumption from the context.
|- R |= T   &   |- S:*   =>   |- (S, R) |= T
Theorem	ct1 52	Introduce a right conjunct.
|- R |= S   &   |- T:*   =>   |- (R, T) |= (S, T)
Theorem	ct2 53	Introduce a left conjunct.
|- R |= S   &   |- T:*   =>   |- (T, R) |= (T, S)
Theorem	sylan 54	Syllogism inference.
|- R |= S   &   |- (S, T) |= A   =>   |- (R, T) |= A
Theorem	an32s 55	Commutation identity for context.
|- ((R, S), T) |= A   =>   |- ((R, T), S) |= A
Theorem	anasss 56	Associativity for context.
|- ((R, S), T) |= A   =>   |- (R, (S, T)) |= A
Theorem	anassrs 57	Associativity for context.
|- (R, (S, T)) |= A   =>   |- ((R, S), T) |= A
Syntax	wv 58	The type of a typed variable.
|- x:al:al
Syntax	wl 59	The type of a lambda abstraction.
|- T:be   =>   |- \x:al T:(al -> be)
Axiom	ax-beta 60	Axiom of beta-substitution.
|- A:be   =>   |- T. |= (( = (\x:al Ax:al))A)
Axiom	ax-distrc 61	Distribution of combination over substitution.
|- A:be   &   |- B:al   &   |- F:(be -> ga)   =>   |- T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
Axiom	ax-leq 62*	Equality theorem for abstraction.
|- A:be   &   |- B:be   &   |- R |= (( = A)B)   =>   |- R |= (( = \x:al A)\x:al B)
Axiom	ax-distrl 63*	Distribution of lambda abstraction over substitution.
|- A:ga   &   |- B:al   =>   |- T. |= (( = (\x:al \y:be AB))\y:be (\x:al AB))
Syntax	wov 64	Type of an infix operator.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- [AFB]:ga
Definition	df-ov 65	Infix operator. This is a simple metamath way of cleaning up the syntax of all these infix operators to make them a bit more readable than the curried representation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   =>   |- T. |= (( = [AFB])((FA)B))
Theorem	dfov1 66	Forward direction of df-ov 65.
|- F:(al -> (be -> *))   &   |- A:al   &   |- B:be   &   |- R |= [AFB]   =>   |- R |= ((FA)B)
Theorem	dfov2 67	Reverse direction of df-ov 65.
|- F:(al -> (be -> *))   &   |- A:al   &   |- B:be   &   |- R |= ((FA)B)   =>   |- R |= [AFB]
Theorem	weqi 68	Type of an equality.
|- A:al   &   |- B:al   =>   |- [A = B]:*
Syntax	eqtypi 69	Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)
|- A:al   &   |- R |= [A = B]   =>   |- B:al
Theorem	eqcomi 70	Commutativity of equality.
|- A:al   &   |- R |= [A = B]   =>   |- R |= [B = A]
Syntax	eqtypri 71	Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)
|- A:al   &   |- R |= [B = A]   =>   |- B:al
Theorem	mpbi 72	Deduction from equality inference.
|- R |= A   &   |- R |= [A = B]   =>   |- R |= B
Theorem	eqid 73	Reflexivity of equality.
|- R:*   &   |- A:al   =>   |- R |= [A = A]
Theorem	ded 74	Deduction theorem for equality.
|- (R, S) |= T   &   |- (R, T) |= S   =>   |- R |= [S = T]
Theorem	dedi 75	Deduction theorem for equality.
|- S |= T   &   |- T |= S   =>   |- T. |= [S = T]
Theorem	eqtru 76	If a statement is provable, then it is equivalent to truth.
|- R |= A   =>   |- R |= [T. = A]
Theorem	mpbir 77	Deduction from equality inference.
|- R |= A   &   |- R |= [B = A]   =>   |- R |= B
Theorem	ceq12 78	Equality theorem for combination.
|- F:(al -> be)   &   |- A:al   &   |- R |= [F = T]   &   |- R |= [A = B]   =>   |- R |= [(FA) = (TB)]
Theorem	ceq1 79	Equality theorem for combination.
|- F:(al -> be)   &   |- A:al   &   |- R |= [F = T]   =>   |- R |= [(FA) = (TA)]
Theorem	ceq2 80	Equality theorem for combination.
|- F:(al -> be)   &   |- A:al   &   |- R |= [A = B]   =>   |- R |= [(FA) = (FB)]
Theorem	leq 81*	Equality theorem for lambda abstraction.
|- A:be   &   |- R |= [A = B]   =>   |- R |= [\x:al A = \x:al B]
Theorem	beta 82	Axiom of beta-substitution.
|- A:be   =>   |- T. |= [(\x:al Ax:al) = A]
Theorem	distrc 83	Distribution of combination over substitution.
|- F:(be -> ga)   &   |- A:be   &   |- B:al   =>   |- T. |= [(\x:al (FA)B) = ((\x:al FB)(\x:al AB))]
Theorem	distrl 84*	Distribution of lambda abstraction over substitution.
|- A:ga   &   |- B:al   =>   |- T. |= [(\x:al \y:be AB) = \y:be (\x:al AB)]
Theorem	eqtri 85	Transitivity of equality.
|- A:al   &   |- R |= [A = B]   &   |- R |= [B = C]   =>   |- R |= [A = C]
Theorem	3eqtr4i 86	Transitivity of equality.
|- A:al   &   |- R |= [A = B]   &   |- R |= [S = A]   &   |- R |= [T = B]   =>   |- R |= [S = T]
Theorem	3eqtr3i 87	Transitivity of equality.
|- A:al   &   |- R |= [A = B]   &   |- R |= [A = S]   &   |- R |= [B = T]   =>   |- R |= [S = T]
Theorem	oveq123 88	Equality theorem for binary operation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [F = S]   &   |- R |= [A = C]   &   |- R |= [B = T]   =>   |- R |= [[AFB] = [CST]]
Theorem	oveq1 89	Equality theorem for binary operation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [A = C]   =>   |- R |= [[AFB] = [CFB]]
Theorem	oveq12 90	Equality theorem for binary operation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [A = C]   &   |- R |= [B = T]   =>   |- R |= [[AFB] = [CFT]]
Theorem	oveq2 91	Equality theorem for binary operation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [B = T]   =>   |- R |= [[AFB] = [AFT]]
Theorem	oveq 92	Equality theorem for binary operation.
|- F:(al -> (be -> ga))   &   |- A:al   &   |- B:be   &   |- R |= [F = S]   =>   |- R |= [[AFB] = [ASB]]
Axiom	ax-hbl1 93	x is bound in \xA.
|- A:ga   &   |- B:al   =>   |- T. |= [(\x:al \x:be AB) = \x:be A]
Theorem	hbl1 94	Inference form of ax-hbl1 93.
|- A:ga   &   |- B:al   &   |- R:*   =>   |- R |= [(\x:al \x:be AB) = \x:be A]
Axiom	ax-17 95*	If x does not appear in A, then any substitution to A yields A again, i.e. \xA is a constant function.
|- A:be   &   |- B:al   =>   |- T. |= [(\x:al AB) = A]
Theorem	a17i 96*	Inference form of ax-17 95.
|- A:be   &   |- B:al   &   |- R:*   =>   |- R |= [(\x:al AB) = A]
Theorem	hbxfrf 97*	Transfer a hypothesis builder to an equivalent expression.
|- T:be   &   |- B:al   &   |- R |= [T = A]   &   |- (S, R) |= [(\x:al AB) = A]   =>   |- (S, R) |= [(\x:al TB) = T]
Theorem	hbxfr 98*	Transfer a hypothesis builder to an equivalent expression.
|- T:be   &   |- B:al   &   |- R |= [T = A]   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al TB) = T]
Theorem	hbth 99*	Hypothesis builder for a theorem.
|- B:al   &   |- R |= A   =>   |- R |= [(\x:al AB) = A]
Theorem	hbc 100	Hypothesis builder for combination.
|- F:(be -> ga)   &   |- A:be   &   |- B:al   &   |- R |= [(\x:al FB) = F]   &   |- R |= [(\x:al AB) = A]   =>   |- R |= [(\x:al (FA)B) = (FA)]