Sorry, copying the definitions from Wikipedia did not work properly. Here are the definitions again (hopefully readable now):
a(0,m) = m+1 a(n+1,0) = a(n,1) a(n+1,m+1) = a (n,a(n+1,m)) and A_1(n) = 2n for n >= 1, A_k(1) = 2 for k >= 2, A_k(n) = A_(k-1)(A_k(n-1)) for n >= 2, k >= 2. Alexander van der Vekens schrieb am Sonntag, 28. April 2024 um 11:13:45 UTC+2: > I wonder how the Ackermann function (see Wikipedia > https://en.wikipedia.org/wiki/Ackermann_function) can be defined in > Methamath/set.mm. > > The Ackermann function with two arguments (introduced by Rózsa Péter) is > defined recursively: > > [image: {\displaystyle {\begin{array}{lcl}\operatorname {a} > (0,m)&=&m+1\\\operatorname {a} (n+1,0)&=&\operatorname {a} > (n,1)\\\operatorname {a} (n+1,m+1)&=&\operatorname {a} (n,\operatorname {a} > (n+1,m))\end{array}}}] > > Maybe the following variant of the Ackermann function (with only one > argument) is easier to be defined with the means of set.mm (and could > serve as a starting point): > > [image: {\displaystyle {\begin{array}{lcl}A_{1}(n)&=&2n&{\text{wenn > }}n\geq 1,\\A_{k}(1)&=&2&{\text{wenn }}k\geq > 2,\\A_{k}(n)&=&A_{k-1}(A_{k}(n-1))&{\text{wenn }}n\geq 2,k\geq > 2.\end{array}}}] > > I am not so familiar with the definitions `recs` (see -df-recs) or `rec` > (see ~df-rec) for transfinite recursion, so I have no idea how to start. > Were/are there already any attempts to formalize the Ackermann funktion > with Metamath? Is there any material (beyond the comments in set.mm and > the Metamath Book) how to formalize such recursive definitions? > > I would like to prove some properties of the Ackermann function, but for > this, I need an appropriate definition first... > -- 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/fa53217b-f3ee-4933-be5d-75756431d7fen%40googlegroups.com.
