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.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 25th 2014

    At incompleteness theorem, the category PRAPRA is defined to be the initial Lawvere theory containing a parameterised NNO (the generalisation of an NNO from a cartesian closed category to a finite-product category). In Maietti’s article Joyal’s arithmetic universe as list-arithmetic pretopos she calls such a thing a Skolem theory. She has subsequent definitions:

    • a category is arithmetic lextensive if it is lextensive with a parameterised NNO. One could take the initial such, though Maietti doesn’t

    • an arithmetic pretopos is a pretopos with parameterised NNO. Again, one can consider the initial such.

    • a list-arithmetic pretopos is a pretopos with parameterised list objects (i.e. pullback-stable free monoid on all objects).

    The initial list-arithmetic pretopos has an internal language strong enough so that it contains an internal initial list-arithmetic pretopos, and apparently this is how Joyal proved Gödel’s result (infamously not published!) I wonder if the proof at incompleteness theorem is a distillation of that (I guess Lawvere might have seen some details at some point), or independently arrived at.

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 25th 2014
    • (edited Nov 25th 2014)

    Robin Cockett wrote in 1989 that the initial arithmetic universe is the exact completion of the equaliser completion of the initial Skolem theory. Amusingly, he also wrote that it was a pity Joyal’s work wasn’t yet published :-)

    Maietti says that her notion of the initial list-arithmetic pretopos turns out to be the same as Joyal’s (I guess this is what Cockett is describing), though the exact implementation of the definition of arithmetic universe is not pinned down due to Joyal’s only having given examples (which are all examples of her notion), rather than a definition.

    For what it’s worth, Cockett also says that an arithmetic universe has free internal categories on internal graphs. I guess this is how one builds up the initial internal arithmetic universe, via several completion steps after some free internal category starting from the NNO of the ambient category.

    • CommentRowNumber3.
    • CommentAuthorThomas Holder
    • CommentTimeNov 25th 2014
    • (edited Nov 25th 2014)

    Just for the record: Joyal gave a talk théorème d’incomplètude de Goedel et univers arithmétique at the Amiens conference in July 1973 . Unfortunately, no abstract seems to appear in the proceedings.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 25th 2014

    Well, I wrote up most of the details seen at incompleteness theorem and it wasn’t done with any knowledge of what Joyal had done, which sounds very beautiful indeed. Mainly I just put it together myself, with a peek at Yanofsky’s paper and some course notes by Stephen Simpson which I could probably find.

    If you or someone could add details on Joyal’s approach, that would be fabulous.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 26th 2014

    @Todd that’s the problem: Joyal’s approach is not written down anywhere. Paul Taylor wrote:

    I went to his office in Montréal in 1991 to get [the notes], but just came away with a copy of Lawvere’s thesis.

    I can write up some details of arithmetic universes as Cockett, Maietti and Taylor describe them, but that is about all.

    I suspect that your write-up is an external perspective on the matter—Lawvere’s theorem is about a category and its objects seen from the outside—but Joyal’s is an internal perspective, using the internal logic of arithmetic universes. Or, most likely, your write-up can be internalised in an arithmetic universe, rather than using the metalogic that Lawvere does (I guess some sort of first-order theory of categories with finite products? Does he need more?)

    • CommentRowNumber6.
    • CommentAuthorRichard Williamson
    • CommentTimeNov 26th 2014
    • (edited Nov 26th 2014)

    Yes, whilst I do not know anything in detail about Joyal’s work on this, I would imagine that you are correct. Lawvere’s argument is very simple and beautiful, and I would have thought is completely independent of Joyal’s work: if there is any relationship, I would have thought that it would be Joyal’s work that would build upon Lawvere’s. The technical part is of course to construct a Gödel numbering: given this, the first incompleteness theorem follows immediately by Lawvere’s argument.

    I would imagine that Joyal’s work is rather about the second incompleteness theorem. I have no idea what exactly Joyal does, but it would for instance be enough to construct a Gödel numbering and be able to carry out Lawvere’s argument ’internally’ to some category. This means roughly that one needs to construct a topos (or something weaker: a hyperdoctrine would be enough) with a natural numbers object ’inside’ another topos (or, again, something weaker). I would guess that arithmetic universes and so on are a way to carry out this idea and make it precise.

    One thing that I would be very interested in is to what extent this programme can be carried out in a predicative constructive setting.

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTimeNov 26th 2014
    • (edited Nov 26th 2014)

    Perhaps I can also add that I am pretty certain that a Gödel numbering can be constructed ’externally’ in a nice enough category with a natural numbers object, following exactly Gödel’s original approach.

    • CommentRowNumber8.
    • CommentAuthorNikolajK
    • CommentTimeNov 26th 2014
    • (edited Nov 26th 2014)
    The second paragraph of Incompleteness theorem says

    […] but in some sense the phenomenon had been known long before. For example, axiom systems for Euclidean geometry which do not include the parallel postulate […]

    […] But the sweeping and ubiquitous nature of incompleteness phenomena only became fully appreciated after Gödel’s work.

    I feel as written down, this comparison undermines the theorem. If I wouldn’t know it, and read this elaboration, I’d not learn that the point is that you can’t fix arithmetic to cure what you want to be cured.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 26th 2014
    • (edited Nov 26th 2014)

    Nikolaj, point taken. Let me do a little rewriting. (Done; please have a look.)

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 27th 2014

    Whoever put Deligne completeness theorem in the article as a related concept: in what way is it related? It’s not clear to me.

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 27th 2014

    Gödel’s completeness theorem is a consequence of Deligne’s, is it not? Mac Lane and Moerdijk even say they are equivalent.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 27th 2014

    Yes, that’s Goedel’s completeness theorem. Not Goedel’s incompleteness theorem.

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 27th 2014

    One might say they are related, by being category-theoretic approaches to foundational logic theorems of Gödel. But I’m not passionate about keeping it there if you feel it is out of place.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 27th 2014

    My feeling is that there ought to be a note on terminology (about completeness vs. incompleteness) in the article – in my mind they are about rather different things, but I am open to other opinions. In any event, we ought to have a dedicated article on Gödel completeness in the nLab where Deligne completeness theorem would be related of course. I seem to recall that the Elephant has details on the exact manner in which these completeness theorems are related, through Morleyization; it would be nice also to have that online.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 27th 2014

    For what it’s worth, the pointer to Deligne’s completness theorem was added in revision 10.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeApr 19th 2016
    • (edited Apr 19th 2016)

    I notice that at incompleteness theorem, then by just chasing back pointers to previous lemmas, it remains unclear what theorem 2 has to do with theorem 1, and why remark 1 appears below theorem 2 as opposed to right after theorem 1.

    I suppose that in the proof of theorem 2, after “let ss be a fixed point”, it could profitably have “which is guaranteed to exist by theorem 1”?

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 20th 2016

    I suppose that in the proof of theorem 2, after “let ss be a fixed point”, it could profitably have “which is guaranteed to exist by theorem 1”?

    Sure. If you want to put that instead, that’s fine. And remark 1 would seem to fit better after theorem 1, I agree.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeApr 20th 2016

    Okay, thanks. I have made the edit.