The Ackermann function was already mentioned before in this Google group (in the context of Metamath Zero, see https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/Y8mGHAW8AQAJ):
- *The one thing that is a bit complicated is non-primitive induction and recursion. Wikipedia says that functions like the Ackermann function are definable in PA, but it's not obvious to me how to do this. I'm assuming we have an iota operator, so that we can extract functions from unique existence proofs. If we have a predicate that says "the Ackermann function is defined at (m,n)" then we can prove this predicate by double induction, but I don't know how to define this predicate. Any ideas?* Does this help somehow? Alexander van der Vekens schrieb am Sonntag, 28. April 2024 um 11:21:11 UTC+2: > 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/a74a9fd3-8572-4a1f-8a2f-36d7d6e20172n%40googlegroups.com.
