I successfully defined the Ackermann function in set.mm as proposed by Thierry, see Git repository, PR #3979. Some adjustments of the suggestion were necessary, especially for the "initial values" of the sequence builder `seq`. Another oddity is the second argument i e. _V which is needed, but not used. Since I had problems with it first, I started with `rec` and the theorems provided in section "Finite recursion". I was very successful with this approach, but its results were based on the ordinal numbers `_om` and not the nonnegative numbers `NN0`, which made calculations with numbers greater than 5 difficult. Therefore, I switched to the approach using `seq`, and the initial extra work paid off at the end.
For more information see https://github.com/metamath/set.mm/pull/3979 [email protected] schrieb am Sonntag, 28. April 2024 um 16:35:45 UTC+2: > On 4/28/24 06:29, 'Thierry Arnoux' via Metamath wrote: > > Maybe I would try as follows, using the seq operator instead of recs, and > the definition as an iterated 1-ary function > <https://en.wikipedia.org/wiki/Ackermann_function#Definition:_as_iterated_1-ary_function> > : > > I didn't try to check every step, but this looks about right. > > As for the larger question of how to formalize recursive definitions, > generally via seq somehow. It can be a bit hard to get your head around > how seq is being used in a particular proof, but using seq is almost > always easier than trying to use recs or rec directly. > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1d12a3a4-f7ad-4b4f-a54c-990dba4ffdban%40googlegroups.com.
