Home Higher-Order Logic ExplorerTheorem List (p. 1 of 3) < Previous  Next > Browser slow? Try the Unicode version.

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.

Theoremidt 14 The identity inference.

Axiomax-syl 15 Syllogism inference.

Theoremsyl 16 Syllogism inference.

Axiomax-jca 17 Join common antecedents.

Theoremjca 18 Syllogism inference.

Theoremsyl2anc 19 Syllogism inference.

Axiomax-simpl 20 Extract an assumption from the context.

Axiomax-simpr 21 Extract an assumption from the context.

Theoremsimpl 22 Extract an assumption from the context.

Theoremsimpr 23 Extract an assumption from the context.

Axiomax-id 24 The identity inference.

Theoremid 25 The identity inference.

Axiomax-trud 26 Deduction form of tru 41.

Theoremtrud 27 Deduction form of tru 41.

Theorema1i 28 Change an empty context into any context.

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 44, and it requires that and be previously established, so it is safe to reverse the process in wctl 31 and wctr 32.

Axiomax-cb2 30 A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.)

Syntaxwctl 31 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)

Syntaxwctr 32 Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.)

Theoremmpdan 33 Modus ponens deduction.

Theoremsyldan 34 Syllogism inference.

Theoremsimpld 35 Extract an assumption from the context.

Theoremsimprd 36 Extract an assumption from the context.

Theoremtrul 37 Deduction form of tru 41.

Syntaxweq 38 The equality function has type , i.e. it is polymorphic over all types, but the left and right type must agree.

Axiomax-refl 39 Reflexivity of equality.

Theoremwtru 40 Truth type.

Theoremtru 41 Tautology is provable.

Axiomax-eqmp 42 Modus ponens for equality.

Axiomax-ded 43 Deduction theorem for equality.

Syntaxwct 44 The type of a context.

Syntaxwc 45 The type of a combination.

Axiomax-ceq 46 Equality theorem for combination.

Theoremeqcomx 47 Commutativity of equality.

Theoremmpbirx 48 Deduction from equality inference.

Theoremancoms 49 Swap the two elements of a context.

Theoremadantr 50 Extract an assumption from the context.

Theoremadantl 51 Extract an assumption from the context.

Theoremct1 52 Introduce a right conjunct.

Theoremct2 53 Introduce a left conjunct.

Theoremsylan 54 Syllogism inference.

Theoreman32s 55 Commutation identity for context.

Theoremanasss 56 Associativity for context.

Theoremanassrs 57 Associativity for context.

Syntaxwv 58 The type of a typed variable.

Syntaxwl 59 The type of a lambda abstraction.

Axiomax-beta 60 Axiom of beta-substitution.

Axiomax-distrc 61 Distribution of combination over substitution.

Axiomax-leq 62* Equality theorem for abstraction.

Axiomax-distrl 63* Distribution of lambda abstraction over substitution.

Syntaxwov 64 Type of an infix operator.

Definitiondf-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.

Theoremdfov1 66 Forward direction of df-ov 65.

Theoremdfov2 67 Reverse direction of df-ov 65.

Theoremweqi 68 Type of an equality.

Syntaxeqtypi 69 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)

Theoremeqcomi 70 Commutativity of equality.

Syntaxeqtypri 71 Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)

Theoremmpbi 72 Deduction from equality inference.

Theoremeqid 73 Reflexivity of equality.

Theoremded 74 Deduction theorem for equality.

Theoremdedi 75 Deduction theorem for equality.

Theoremeqtru 76 If a statement is provable, then it is equivalent to truth.

Theoremmpbir 77 Deduction from equality inference.

Theoremceq12 78 Equality theorem for combination.

Theoremceq1 79 Equality theorem for combination.

Theoremceq2 80 Equality theorem for combination.

Theoremleq 81* Equality theorem for lambda abstraction.

Theorembeta 82 Axiom of beta-substitution.

Theoremdistrc 83 Distribution of combination over substitution.

Theoremdistrl 84* Distribution of lambda abstraction over substitution.

Theoremeqtri 85 Transitivity of equality.

Theorem3eqtr4i 86 Transitivity of equality.

Theorem3eqtr3i 87 Transitivity of equality.

Theoremoveq123 88 Equality theorem for binary operation.

Theoremoveq1 89 Equality theorem for binary operation.

Theoremoveq12 90 Equality theorem for binary operation.

Theoremoveq2 91 Equality theorem for binary operation.

Theoremoveq 92 Equality theorem for binary operation.

Axiomax-hbl1 93 is bound in .

Theoremhbl1 94 Inference form of ax-hbl1 93.

Axiomax-17 95* If does not appear in , then any substitution to yields again, i.e. is a constant function.

Theorema17i 96* Inference form of ax-17 95.

Theoremhbxfrf 97* Transfer a hypothesis builder to an equivalent expression.

Theoremhbxfr 98* Transfer a hypothesis builder to an equivalent expression.

Theoremhbth 99* Hypothesis builder for a theorem.

Theoremhbc 100 Hypothesis builder for combination.

Page List