Home Higher-Order Logic ExplorerTheorem List (p. 1 of 3) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  HOLE Home Page  >  Theorem List Contents       This page: Page List

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

0.1  Foundations

Syntaxtv 1 A var is a term.
term

Syntaxht 2 The type of all functions from type to type .
type

Syntaxhb 3 The type of booleans (true and false).
type

Syntaxhi 4 The type of individuals.
type

Syntaxkc 5 A combination (function application).
term

Syntaxkl 6 A lambda abstraction.
term

Syntaxke 7 The equality term.
term

Syntaxkt 8 Truth term.
term

Syntaxkbr 9 Infix operator.
term

Syntaxkct 10 Context operator.
term

SyntaxwffMMJ2 11 Internal axiom for mmj2 use.
wff

SyntaxwffMMJ2t 12 Internal axiom for mmj2 use.
wff

Theoremidi 13 The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.)

Theoremidt 14 The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.)

Axiomax-syl 15 Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsyl 16 Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-jca 17 Join common antecedents. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremjca 18 Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsyl2anc 19 Syllogism inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-simpl 20 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-simpr 21 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsimpl 22 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsimpr 23 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-id 24 The identity inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremid 25 The identity inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-trud 26 Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremtrud 27 Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theorema1i 28 Change an empty context into any context. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-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 where and are type variables, also ensures that and . Thus it is impossible to prove any theorem unless both and had been previously derived, so it is conservative to deduce from . The same remark applies to the construction of the theorem - there is only one rule that creates a formula of this type, namely wct 48, and it requires that and be previously established, so it is safe to reverse the process in wctl 33 and wctr 34. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-cb2 30 A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-wctl 31 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) Prefer wctl 33. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-wctr 32 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) Prefer wctr 34. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwctl 33 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwctr 34 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremmpdan 35 Modus ponens deduction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsyldan 36 Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsimpld 37 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremsimprd 38 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremtrul 39 Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-weq 40 The equality function has type , i.e. it is polymorphic over all types, but the left and right type must agree. (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremweq 41 The equality function has type , i.e. it is polymorphic over all types, but the left and right type must agree. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-refl 42 Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremwtru 43 Truth type. (Contributed by Mario Carneiro, 10-Oct-2014.)

Theoremtru 44 Tautology is provable. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-eqmp 45 Modus ponens for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-ded 46 Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-wct 47 The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.)

Theoremwct 48 The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-wc 49 The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.)

Theoremwc 50 The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-ceq 51 Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqcomx 52 Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremmpbirx 53 Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremancoms 54 Swap the two elements of a context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremadantr 55 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremadantl 56 Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremct1 57 Introduce a right conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.)

Theoremct2 58 Introduce a left conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.)

Theoremsylan 59 Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoreman32s 60 Commutation identity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremanasss 61 Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremanassrs 62 Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-wv 63 The type of a typed variable. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwv 64 The type of a typed variable. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-wl 65 The type of a lambda abstraction. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwl 66 The type of a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-beta 67 Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-distrc 68 Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-leq 69* Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-distrl 70* Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-wov 71 Type of an infix operator. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremwov 72 Type of an infix operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Definitiondf-ov 73 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. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremdfov1 74 Forward direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremdfov2 75 Reverse direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremweqi 76 Type of an equality. (Contributed by Mario Carneiro, 8-Oct-2014.)

Axiomax-eqtypi 77 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqtypi 78 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqcomi 79 Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Axiomax-eqtypri 80 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqtypri 81 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremmpbi 82 Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqid 83 Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremded 84 Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremdedi 85 Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremeqtru 86 If a statement is provable, then it is equivalent to truth. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremmpbir 87 Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremceq12 88 Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremceq1 89 Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremceq2 90 Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremleq 91* Equality theorem for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theorembeta 92 Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremdistrc 93 Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremdistrl 94* Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Theoremeqtri 95 Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theorem3eqtr4i 96 Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theorem3eqtr3i 97 Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremoveq123 98 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremoveq1 99 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)

Theoremoveq12 100 Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)

Page List