Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorSam Staton
    • CommentTimeMay 26th 2019

    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

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 26th 2019

    Thanks, 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+1A_0(m) = m+1, then I seem to get A 1(m)=A 0 m(1)=m+1A_1(m) = A_0^m(1) = m+1 as well. So maybe those other references use a slightly different recursive rule?

    • CommentRowNumber3.
    • CommentAuthorSam Staton
    • CommentTimeMay 27th 2019

    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

    • CommentRowNumber4.
    • CommentAuthorSam Staton
    • CommentTimeMay 27th 2019
    • (edited May 27th 2019)

    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 <ω ω\lt \omega^\omega, whereas the latter contains functions with termination ordinal <ε 0 \lt \epsilon_0. (In the sense of ordinal analysis.)

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 27th 2019
    • (edited May 27th 2019)

    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 n\mathbb{N}^n in SetSet 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.

    • CommentRowNumber6.
    • CommentAuthorSam Staton
    • CommentTimeMay 27th 2019

    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.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 3rd 2019

    I think the claim (here) that partial recursive functions give a Lawvere theory is incorrect, as the cartesian product k\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 m k+l\mathbb{N}^m \to \mathbb{N}^{k+l} induced from a pair of partial functions m k\mathbb{N}^m \to \mathbb{N}^k and m l\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?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 3rd 2019

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

    a morphism k1k \to 1 of the Lawvere theory is a function k 1\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 kk replaced by an arbitrary nn. It seems to me that we would get a Lawvere theory if we take this statement as written, only applying to the morphisms k1k\to 1, and then define the morphisms knk\to n to be what they have to be to make it a Lawvere theory, namely nn-tuples of partial recursive functions k 1\mathbb{N}^k \to \mathbb{N}^1 — which, as you note, are not the same as single partial recursive functions k n\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.

    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 4th 2019

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

    I will edit the entry to make this more clear.