Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
  
  
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorSam Staton
   • CommentTimeMay 26th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexComment about Ackermann function. I don't know what Ackermann originally wrote, but most texts use A_0(m)=m+1, if I understand correctly. <a href="https://ncatlab.org/nlab/revision/diff/partial+recursive+function/18">diff</a>, <a href="https://ncatlab.org/nlab/revision/partial+recursive+function/18">v18</a>, <a href="https://ncatlab.org/nlab/show/partial+recursive+function">current</a>

   Comment about Ackermann function. I don’t know what Ackermann originally wrote, but most texts use A_0(m)=m+1, if I understand correctly.

   diff, v18, current

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 26th 2019
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThanks, Sam. The definition I wrote comes from the lecture notes of Stephen Simpson that I put in the references. Let's see: if $A_0(m) = m+1$, then I seem to get $A_1(m) = A_0^m(1) = m+1$ as well. So maybe those other references use a slightly different recursive rule?

   Thanks, Sam. The definition I wrote comes from the lecture notes of Stephen Simpson that I put in the references.

   Let’s see: if , then I seem to get as well. So maybe those other references use a slightly different recursive rule?

3. • CommentRowNumber3.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexThanks, you're right, they put an extra f in the inductive step. This is the version I learnt as a student, and also the version on wikipedia. I don't know a case for using one or the other, though. <a href="https://ncatlab.org/nlab/revision/diff/partial+recursive+function/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/partial+recursive+function/19">v19</a>, <a href="https://ncatlab.org/nlab/show/partial+recursive+function">current</a>

   Thanks, you’re right, they put an extra f in the inductive step. This is the version I learnt as a student, and also the version on wikipedia. I don’t know a case for using one or the other, though.

   diff, v19, current

4. • CommentRowNumber4.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • (edited May 27th 2019)
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexIncidentally, my understanding of the fact that Ackermann is not definable in the free category with products and a natural numbers object, but is definable in the free ccc with a natural numbers object, is that the former category contains functions with termination ordinal $\lt \omega^\omega$, whereas the latter contains functions with termination ordinal $ \lt \epsilon_0$. (In the sense of [[https://ncatlab.org/nlab/show/ordinal+analysis|ordinal analysis]].)

   Incidentally, my understanding of the fact that Ackermann is not definable in the free category with products and a natural numbers object, but is definable in the free ccc with a natural numbers object, is that the former category contains functions with termination ordinal , whereas the latter contains functions with termination ordinal . (In the sense of ordinal analysis.)

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 27th 2019
   • (edited May 27th 2019)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexYes, thanks. I don't know if you looked carefully at the nLab article, but I did record a detailed proof there that Ackermann cannot live in the standard category whose objects are finite powers $\mathbb{N}^n$ in $Set$ and whose morphisms are primitive recursive maps between them. If it lived in the initial category with products and a *parametrized* NNO, then you could transfer it along the product-preserving map over to the standard category. Meanwhile, at the Café I explicitly wrote down a definition of Ackermann in the free CCC with NNO, which I assume you saw (because otherwise, it'd be quite a coincidence that you started this thread just now), but in case not, it's [here](https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html#c055900). Meanwhile, I've added another Café comment [here](https://golem.ph.utexas.edu/category/2019/05/polyadic_boolean_algebras.html#c055903).

   Yes, thanks. I don’t know if you looked carefully at the nLab article, but I did record a detailed proof there that Ackermann cannot live in the standard category whose objects are finite powers in and whose morphisms are primitive recursive maps between them. If it lived in the initial category with products and a parametrized NNO, then you could transfer it along the product-preserving map over to the standard category. Meanwhile, at the Café I explicitly wrote down a definition of Ackermann in the free CCC with NNO, which I assume you saw (because otherwise, it’d be quite a coincidence that you started this thread just now), but in case not, it’s here.

   Meanwhile, I’ve added another Café comment here.

6. • CommentRowNumber6.
   • CommentAuthorSam Staton
   • CommentTimeMay 27th 2019
   • PermaLink
   Author: Sam Staton
   Format: MarkdownItexSorry, yes, I came from the café, and your nice definition of Ackermann in the free ccc! That was indeed the context of my comment #4, which should perhaps have gone on the cafe instead.

   Sorry, yes, I came from the café, and your nice definition of Ackermann in the free ccc! That was indeed the context of my comment #4, which should perhaps have gone on the cafe instead.

7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 3rd 2019
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI think the claim ([here](https://ncatlab.org/nlab/show/partial+recursive+function#Lawvere)) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product $\mathbb{N}^k$ is not the product in any category whose objects are finite powers of $\mathbb{N}$ and whose morphisms are some class of partial functions closed under composition and including projections and diagonals. There is a unique partial function $\mathbb{N}^m \to \mathbb{N}^{k+l}$ induced from a pair of partial functions $\mathbb{N}^m \to \mathbb{N}^k$ and $\mathbb{N}^m \to \mathbb{N}^l$, but the usual triangles don't commute! The cartesian product here is only a 'restriction product', namely a lax product in the locally posetal 2-category determined by the given category of partial functions. Since the primitive recursive functions are total and include projections, that's not a problem. I'm not sure what I want to put in place of the current statement: a disclaimer? an explanation of what goes wrong? An attempt at outlining a generalisation of a Lawvere theory?

   I think the claim (here) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product is not the product in any category whose objects are finite powers of and whose morphisms are some class of partial functions closed under composition and including projections and diagonals. There is a unique partial function induced from a pair of partial functions and , but the usual triangles don’t commute! The cartesian product here is only a ’restriction product’, namely a lax product in the locally posetal 2-category determined by the given category of partial functions.

   Since the primitive recursive functions are total and include projections, that’s not a problem.

   I’m not sure what I want to put in place of the current statement: a disclaimer? an explanation of what goes wrong? An attempt at outlining a generalisation of a Lawvere theory?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeOct 3rd 2019
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexInteresting point. I notice, though, that the claim as stated only says that > a morphism $k \to 1$ of the Lawvere theory is a function $\mathbb{N}^k \to \mathbb{N}^1$ belonging to the class [of partial recursive functions] whereas you seem to be objecting to a version of this statement with $k$ replaced by an arbitrary $n$. It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms $k\to 1$, and then *define* the morphisms $k\to n$ to be what they have to be to make it a Lawvere theory, namely $n$-tuples of partial recursive functions $\mathbb{N}^k \to \mathbb{N}^1$ --- which, as you note, are not the same as single partial recursive functions $\mathbb{N}^k \to \mathbb{N}^n$. Put differently, partial recursive functions "naturally" form a cartesian operad, which we can then make into its equivalent Lawvere theory.

   Interesting point. I notice, though, that the claim as stated only says that

   a morphism of the Lawvere theory is a function belonging to the class [of partial recursive functions]

   whereas you seem to be objecting to a version of this statement with replaced by an arbitrary . It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms , and then define the morphisms to be what they have to be to make it a Lawvere theory, namely -tuples of partial recursive functions — which, as you note, are not the same as single partial recursive functions .

   Put differently, partial recursive functions “naturally” form a cartesian operad, which we can then make into its equivalent Lawvere theory.

9. • CommentRowNumber9.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 4th 2019
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexOh, I see, defining the problem away! Neat. (I think you mean "with $1$ replaced by an arbitrary $n$") I will edit the entry to make this more clear.

   Oh, I see, defining the problem away! Neat. (I think you mean “with replaced by an arbitrary ”)

   I will edit the entry to make this more clear.