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

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

Theoremhbov 101 Hypothesis builder for binary operation.

Theoremhbl 102* Hypothesis builder for lambda abstraction.

Axiomax-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).

Theoreminsti 104* Instantiate a theorem with a new term.

Theoremclf 105* Evaluate a lambda expression.

Theoremcl 106* Evaluate a lambda expression.

Theoremovl 107* Evaluate a lambda expression in a binary operation.

term

Syntaxtan 109 Conjunction term.
term

Syntaxtne 110 Negation term.
term

Syntaxtim 111 Implication term.
term

Syntaxtal 112 For all term.
term

Syntaxtex 113 There exists term.
term

Syntaxtor 114 Disjunction term.
term

Syntaxteu 115 There exists unique term.
term

Definitiondf-al 116* Define the for all operator.

Definitiondf-fal 117 Define the constant false.

Definitiondf-an 118* Define the 'and' operator.

Definitiondf-im 119* Define the implication operator.

Definitiondf-not 120 Define the negation operator.

Definitiondf-ex 121* Define the existence operator.

Definitiondf-or 122* Define the 'or' operator.

Definitiondf-eu 123* Define the 'exists unique' operator.

Theoremwal 124 For all type.

Theoremwan 126 Conjunction type.

Theoremwim 127 Implication type.

Theoremwnot 128 Negation type.

Theoremwex 129 There exists type.

Theoremwor 130 Disjunction type.

Theoremweu 131 There exists unique type.

Theoremalval 132* Value of the for all predicate.

Theoremexval 133* Value of the 'there exists' predicate.

Theoremeuval 134* Value of the 'exists unique' predicate.

Theoremnotval 135 Value of negation.

Theoremimval 136 Value of the implication.

Theoremorval 137* Value of the disjunction.

Theoremanval 138* Value of the conjunction.

Theoremax4g 139 If is true for all , then it is true for .

Theoremax4 140 If is true for all , then it is true for .

Theoremalrimiv 141* If one can prove where does not contain , then is true for all .

Theoremcla4v 142* If is true for all , then it is true for .

Theorempm2.21 143 A falsehood implies anything.

Theoremdfan2 144 An alternative defintion of the "and" term in terms of the context conjunction.

Theoremhbct 145 Hypothesis builder for context conjunction.

Theoremmpd 146 Modus ponens.

Theoremimp 147 Importation deduction.

Theoremex 148 Exportation deduction.

Theoremnotval2 149 Another way two write , the negation of .

Theoremnotnot1 150 One side of notnot 187.

Theoremcon2d 151 A contraposition deduction.

Theoremcon3d 152 A contraposition deduction.

Theoremecase 153 Elimination by cases.

Theoremolc 154 Or introduction.

Theoremorc 155 Or introduction.

Theoremexlimdv2 156* Existential elimination.

Theoremexlimdv 157* Existential elimination.

Theoremax4e 158 Existential introduction.

Theoremcla4ev 159* Existential introduction.

Theorem19.8a 160 Existential introduction.

0.3  Type definition mechanism

SyntaxwffMMJ2d 161 Internal axiom for mmj2 use.
wff typedef

Syntaxwabs 162 Type of the abstraction function.
typedef

Syntaxwrep 163 Type of the representation function.
typedef

Axiomax-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 mapping the new type to the subset of the old type such that 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 that is not always false.
typedef

0.4  Extensionality

Axiomax-eta 165* The eta-axiom: a function is determined by its values.

Theoremeta 166* The eta-axiom: a function is determined by its values.

Theoremcbvf 167* Change bound variables in a lambda abstraction.

Theoremcbv 168* Change bound variables in a lambda abstraction.

Theoremleqf 169* Equality theorem for lambda abstraction, using bound variable instead of distinct variables.

Theoremalrimi 170* If one can prove where does not contain , then is true for all .

Theoremexlimd 171* Existential elimination.

Theoremalimdv 172* Deduction from Theorem 19.20 of [Margaris] p. 90.

Theoremeximdv 173* Deduction from Theorem 19.22 of [Margaris] p. 90.

Theoremalnex 174* Theorem 19.7 of [Margaris] p. 89.

Theoremexnal1 175* Forward direction of exnal 188.

Theoremisfree 176* Derive the metamath "is free" predicate in terms of the HOL "is free" predicate.

0.5  Axioms of infinity and choice

Syntaxtf11 177 One-to-one function.
term 1-1

Syntaxtfo 178 Onto function.
term onto

Syntaxtat 179 Indefinite descriptor.
term

Syntaxwat 180 The type of the indefinite descriptor.

Definitiondf-f11 181* Define a one-to-one function.
1-1

Definitiondf-fo 182* Define an onto function.
onto

Axiomax-ac 183* Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF.

Theoremac 184 Defining property of the indefinite descriptor: it selects an element from any type. This is equivalent to global choice in ZF.

Theoremdfex2 185 Alternative definition of the "there exists" quantifier.

Theoremexmid 186 Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice.

Theoremnotnot 187 Rule of double negation.

Theoremexnal 188* Theorem 19.14 of [Margaris] p. 90.

Axiomax-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 .
1-1 onto

0.6  Rederive the Metamath axioms

Theoremax1 190 Axiom Simp. Axiom A1 of [Margaris] p. 49.

Theoremax2 191 Axiom Frege. Axiom A2 of [Margaris] p. 49.

Theoremax3 192 Axiom Transp. Axiom A3 of [Margaris] p. 49.

Theoremaxmp 193 Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73.

Theoremax5 194* Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.

Theoremax6 195* Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.

Theoremax7 196* Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint).

Theoremaxgen 197* Rule of Generalization. See e.g. Rule 2 of [Hamilton] p. 74.

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

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

Theoremax10 200* Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).

Page List