| Description: Define a recursive
definition generator on On (the class of ordinal
numbers) 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 rec operation
(especially when df-recs 6195
that it is built on is also eliminated). But once we get past this
hurdle, definitions that would otherwise be recursive become relatively
simple. In classical logic it would be easier to divide this definition
into cases based on whether the domain of 𝑔 is zero, a successor, or
a limit ordinal. Cases do not (in general) work that way in
intuitionistic logic, so instead we choose a definition which takes the
union of all the results of the characteristic function for ordinals in
the domain of 𝑔. This means that this definition has
the expected
properties for increasing and continuous ordinal functions, which
include ordinal addition and multiplication.
For finite recursion we also define df-frec 6281 and for suitable
characteristic functions df-frec 6281 yields the same result as rec
restricted to ω, as seen at frecrdg 6298.
Note: We introduce rec 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 Jim Kingdon, 19-May-2019.) |
