Home | Intuitionistic Logic Explorer Theorem List (p. 62 of 114) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rdgival 6101* | Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.) |
Theorem | rdgss 6102 | Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.) |
Theorem | rdgisuc1 6103* |
One way of describing the value of the recursive definition generator at
a successor. There is no condition on the characteristic function
other than
. Given that, the resulting expression
encompasses both the expected successor term
but also
terms that correspond to
the initial value and to limit ordinals
.
If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 6104. (Contributed by Jim Kingdon, 9-Jun-2019.) |
Theorem | rdgisucinc 6104* |
Value of the recursive definition generator at a successor.
This can be thought of as a generalization of oasuc 6179 and omsuc 6187. (Contributed by Jim Kingdon, 29-Aug-2019.) |
Theorem | rdgon 6105* | Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.) |
Theorem | rdg0 6106 | The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | rdg0g 6107 | The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.) |
Theorem | rdgexg 6108 | The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.) |
Syntax | cfrec 6109 | Extend class notation with the finite recursive definition generator, with characteristic function and initial value . |
frec | ||
Definition | df-frec 6110* |
Define a recursive definition generator on (the class of finite
ordinals) with characteristic function and initial value .
This rather amazing operation allows us to define, with compact direct
definitions, functions that are usually defined in textbooks only with
indirect self-referencing recursive definitions. A recursive definition
requires advanced metalogic to justify - in particular, eliminating a
recursive definition is very difficult and often not even shown in
textbooks. On the other hand, the elimination of a direct definition is
a matter of simple mechanical substitution. The price paid is the
daunting complexity of our frec operation (especially when df-recs 6024
that it is built on is also eliminated). But once we get past this
hurdle, definitions that would otherwise be recursive become relatively
simple; see frec0g 6116 and frecsuc 6126.
Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4392. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6127, this definition and df-irdg 6089 restricted to produce the same result. Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.) |
frec recs | ||
Theorem | freceq1 6111 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec frec | ||
Theorem | freceq2 6112 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec frec | ||
Theorem | frecex 6113 | Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.) |
frec | ||
Theorem | frecfun 6114 | Finite recursion produces a function. See also frecfnom 6120 which also states that the domain of that function is but which puts conditions on and . (Contributed by Jim Kingdon, 13-Feb-2022.) |
frec | ||
Theorem | nffrec 6115 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec | ||
Theorem | frec0g 6116 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
frec | ||
Theorem | frecabex 6117* | The class abstraction from df-frec 6110 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
Theorem | frecabcl 6118* | The class abstraction from df-frec 6110 exists. Unlike frecabex 6117 the function only needs to be defined on , not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.) |
Theorem | frectfr 6119* |
Lemma to connect transfinite recursion theorems with finite recursion.
That is, given the conditions
and on
frec , we
want to be able to apply tfri1d 6054 or tfri2d 6055,
and this lemma lets us satisfy hypotheses of those theorems.
(Contributed by Jim Kingdon, 15-Aug-2019.) |
Theorem | frecfnom 6120* | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
frec | ||
Theorem | freccllem 6121* | Lemma for freccl 6122. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.) |
recs frec | ||
Theorem | freccl 6122* | Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.) |
frec | ||
Theorem | frecfcllem 6123* | Lemma for frecfcl 6124. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.) |
recs frec | ||
Theorem | frecfcl 6124* | Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.) |
frec | ||
Theorem | frecsuclem 6125* | Lemma for frecsuc 6126. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.) |
frec frec | ||
Theorem | frecsuc 6126* | The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.) |
frec frec | ||
Theorem | frecrdg 6127* |
Transfinite recursion restricted to omega.
Given a suitable characteristic function, df-frec 6110 produces the same results as df-irdg 6089 restricted to . Presumably the theorem would also hold if were changed to . (Contributed by Jim Kingdon, 29-Aug-2019.) |
frec | ||
Syntax | c1o 6128 | Extend the definition of a class to include the ordinal number 1. |
Syntax | c2o 6129 | Extend the definition of a class to include the ordinal number 2. |
Syntax | c3o 6130 | Extend the definition of a class to include the ordinal number 3. |
Syntax | c4o 6131 | Extend the definition of a class to include the ordinal number 4. |
Syntax | coa 6132 | Extend the definition of a class to include the ordinal addition operation. |
Syntax | comu 6133 | Extend the definition of a class to include the ordinal multiplication operation. |
Syntax | coei 6134 | Extend the definition of a class to include the ordinal exponentiation operation. |
↑_{𝑜} | ||
Definition | df-1o 6135 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
Definition | df-2o 6136 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
Definition | df-3o 6137 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-4o 6138 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
Definition | df-oadd 6139* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
Definition | df-omul 6140* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
Definition | df-oexpi 6141* |
Define the ordinal exponentiation operation.
This definition is similar to a conventional definition of exponentiation except that it defines ↑_{𝑜} to be for all , in order to avoid having different cases for whether the base is or not. (Contributed by Mario Carneiro, 4-Jul-2019.) |
↑_{𝑜} | ||
Theorem | 1on 6142 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
Theorem | 1oex 6143 | Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.) |
Theorem | 2on 6144 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | 2on0 6145 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
Theorem | 3on 6146 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | 4on 6147 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
Theorem | df1o2 6148 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
Theorem | df2o3 6149 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | df2o2 6150 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
Theorem | 1n0 6151 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
Theorem | xp01disj 6152 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
Theorem | ordgt0ge1 6153 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
Theorem | ordge1n0im 6154 | An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.) |
Theorem | el1o 6155 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
Theorem | dif1o 6156 | Two ways to say that is a nonzero number of the set . (Contributed by Mario Carneiro, 21-May-2015.) |
Theorem | 2oconcl 6157 | Closure of the pair swapping function on . (Contributed by Mario Carneiro, 27-Sep-2015.) |
Theorem | 0lt1o 6158 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
Theorem | oafnex 6159 | The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.) |
Theorem | sucinc 6160* | Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.) |
Theorem | sucinc2 6161* | Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.) |
Theorem | fnoa 6162 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.) |
Theorem | oaexg 6163 | Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
Theorem | omfnex 6164* | The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.) |
Theorem | fnom 6165 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.) |
Theorem | omexg 6166 | Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
Theorem | fnoei 6167 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.) |
↑_{𝑜} | ||
Theorem | oeiexg 6168 | Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.) |
↑_{𝑜} | ||
Theorem | oav 6169* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | omv 6170* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Theorem | oeiv 6171* | Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.) |
↑_{𝑜} | ||
Theorem | oa0 6172 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | om0 6173 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | oei0 6174 | Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
↑_{𝑜} | ||
Theorem | oacl 6175 | Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim Kingdon, 26-Jul-2019.) |
Theorem | omcl 6176 | Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Constructive proof by Jim Kingdon, 26-Jul-2019.) |
Theorem | oeicl 6177 | Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.) |
↑_{𝑜} | ||
Theorem | oav2 6178* | Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.) |
Theorem | oasuc 6179 | Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | omv2 6180* | Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.) |
Theorem | onasuc 6181 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.) |
Theorem | oa1suc 6182 | Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.) |
Theorem | o1p1e2 6183 | 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.) |
Theorem | oawordi 6184 | Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.) |
Theorem | oawordriexmid 6185* | A weak ordering property of ordinal addition which implies excluded middle. The property is proposition 8.7 of [TakeutiZaring] p. 59. Compare with oawordi 6184. (Contributed by Jim Kingdon, 15-May-2022.) |
Theorem | oaword1 6186 | An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.) |
Theorem | omsuc 6187 | Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
Theorem | onmsuc 6188 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nna0 6189 | Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) |
Theorem | nnm0 6190 | Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) |
Theorem | nnasuc 6191 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nnmsuc 6192 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nna0r 6193 | Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
Theorem | nnm0r 6194 | Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnacl 6195 | Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nnmcl 6196 | Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Theorem | nnacli 6197 | is closed under addition. Inference form of nnacl 6195. (Contributed by Scott Fenton, 20-Apr-2012.) |
Theorem | nnmcli 6198 | is closed under multiplication. Inference form of nnmcl 6196. (Contributed by Scott Fenton, 20-Apr-2012.) |
Theorem | nnacom 6199 | Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Theorem | nnaass 6200 | Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |