Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
At incompleteness theorem, the category 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.
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.
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.
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.
@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?)
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.
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.
[…] 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 […]
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.
Nikolaj, point taken. Let me do a little rewriting. (Done; please have a look.)
Whoever put Deligne completeness theorem in the article as a related concept: in what way is it related? It’s not clear to me.
Gödel’s completeness theorem is a consequence of Deligne’s, is it not? Mac Lane and Moerdijk even say they are equivalent.
Yes, that’s Goedel’s completeness theorem. Not Goedel’s incompleteness theorem.
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.
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.
For what it’s worth, the pointer to Deligne’s completness theorem was added in revision 10.
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 be a fixed point”, it could profitably have “which is guaranteed to exist by 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”?
Sure. If you want to put that instead, that’s fine. And remark 1 would seem to fit better after theorem 1, I agree.
Okay, thanks. I have made the edit.
1 to 18 of 18