09/28/2022, 04:57 PM
(09/22/2022, 12:19 PM)Daniel Wrote: Consider the Ackermann successor function \[\varphi(u)\] such that \[\varphi(a \uparrow ^m b)=a \uparrow ^{m+1} b\].
Is this well-defined? I mean to define it that way you would need something like: if \(a_1\uparrow^m b_1=a_2\uparrow^m b_2\) then \(a_1=a_2\) and \(b_1=b_2\) ?
