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>:
Let's say F : NN0 --> NN0 is a function we want to apply repeatedly. Then B = ( f e. _V |-> seq 0 ( ( g e. _V , i e. _V |-> ( f o. g ) ) , _I ) ) should be the n-th iterate of f: ( ( B ` f ) ` 3 ) = ( f o. ( f o. f ) ) ) We can then define the Ackermann function as follows: Ack = seq 0 ( ( f e. _V , i e, _V |-> ( n e. NN0 |-> ( ( ( B ` f ) ` n ) ` 1 ) ) , ( n e. NN0 |-> ( n + 1 ) ) ) That is, we would have: * Using *~seq1* : ( Ack ` 0 ) = ( n e. NN0 |-> ( n + 1 ) ) * Using *~seqp1* : ( ( Ack ` ( m + 1 ) ) ` n ) = ( ( ( B ` ( Ack ` m ) ) ` n ) ` 1 ) Then I would derive the other definition of the Ackermann function as a property. BR, _ Thierry On 28/04/2024 11:25, 'Alexander van der Vekens' via Metamath wrote:
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 <http://set.mm>. The Ackermann function with two arguments (introduced by Rózsa Péter) is defined recursively: {\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 <http://set.mm> (and could serve as a starting point): {\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 <http://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 <https://groups.google.com/d/msgid/metamath/a74a9fd3-8572-4a1f-8a2f-36d7d6e20172n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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/d3b117fe-27de-4716-9572-ba3ad9bfdf79%40gmx.net.
