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.
Hello all,
I am very interested in, and have been thinking for a while now about, trying to give a categorical proof, and indeed even formulate a nice categorical statement, of Gödel’s second incompleteness theorem. There was a recent post here in which this cropped up: as mentioned in that post, Joyal announced a proof in the 1970s, but details have never been given. It seems to me that many people would be interested in a proof, including several who read and write posts to the nForum. Therefore, I would like to propose that we try to come up with a proof in this thread.
Just for a little more motivation, perhaps I can also mention that I was somewhat surprised, when attempting to find a good exposition of a proof of the second incompleteness theorem, that in fact this seems to be next to impossible! Gödel himself did not give details, and every exposition that I have seen skips some: the standard approach makes use of the fact that certain conditions variously ascribed to Hilbert, Bernays, or Gödel (usually the first two) hold, but showing that these conditions indeed hold appears to be rather horrific. A good, conceptual proof would, I feel, be really worth having.
I hope that it may be possible to avoid these conditions, and find an alternative way of proceeding, in a categorical setting. The rough idea is to ’carry out the proof of the first incompleteness theorem inside one’s formal system’, but putting this into practise is another thing entirely: I hope that a categorical approach may lead to an elegant way to proceed.
I am happy to take responsibility for writing up any proof that is arrived at, assigning authorship to all contributors, or to an appropriate group title, or in any other way that is considered most appropriate. Others would be welcome of course to write it up too in their own style (I would use a public git repository to post the source code).
I have some ideas about how to approach a proof. Rather than write an enormous post attempting to cover everything in one go, I will instead try to get the ball rolling with one question, which I feel is actually the key to the story: how can Gödel numbering be understood in a good way from a categorical point of view?
A nice categorical proof of the first incompleteness theorem was outlined by Lawvere in the 1960s, and indeed has been written up in one form on the nLab. However, such proofs are not complete, exactly because they skip over the construction of a Gödel numbering. Whilst the ordinary construction of a Gödel numbering would no doubt suffice to complete such proofs, I find this unsatisfactory: I would not regard such a proof as truly categorical. I feel that there should be a better conceptual formalism in which to understand Gödel numbering from a categorical point of view.
I do not have an answer to my question yet, just some ’very early stage ideas’. These may very well have flaws, but I hope that through discussing these ideas, or alternative ones that people can suggest, we will be able to refine them.
Let us first fix a category T to which we would like Gödel’s second incompleteness theorem to apply. This category should ’have a sufficiently nice internal logic, and contain enough arithmetic’. Joyal’s arithmetic universes seem intended to be such categories, but 40 years on, it seems to me that one should just follow one’s nose. A Heyting pretopos with a parameterised natural numbers object seems like a good place to begin. For reasons that I hope to explain at a later time, slightly stronger properties of the logic of T may be needed, but we can ignore this for now.
I feel that it may be conceptually nicer, however, to work with the hyperdoctrine associated to T rather than T itself. An idea that I have regarding a possible way to understand Gödel numbering is: as a ’morphism of hyperdoctrines from T to an ’hyperdoctrine internal to T’ which itself is a rich enough theory of arithmetic’.
There are, however, many things to make precise here. Even the notion of a morphism of hyperdoctrines does not seem to have been studied in depth in the literature, but it shouldn’t be too difficult to formulate an appropriate one for the purposes at hand.
More difficult would seem to be the ’internal’ aspect. One can try to ignore the hyperdoctrinal point of view (or to pass to and fro between it and just working with T), and try to work with a category internal to T which has similar properties. But it still seems to me that there is work to do: can logical theories be ’internalised’ in this way? How to construct the relevant category/hyperdoctrine internal to T? And the question that I feel that I understand least: how to make sense of a ’morphism of hyperdoctrines from the hyperdoctrine associated to T to the internal category/hyperdoctrine’?
There are other important aspects. I have written ’hyperdoctrine’, but there are various choices to be made as to the kind of hyperdoctrine to be used. An important part of Gödel numbering is of course that proofs must be arithmetised, and therefore it would seem to me that the hyperdoctrine should be ’proof relevant’, namely land in (appropriate) categories rather than (appropriate) posets.
Actually carrying out the Gödel numbering itself would seem to me straightforward along the lines of Gödel’s original approach, given an appropriate categorical context in which to understand it.
Thoughts/pointing out of flaws/alternative ideas are very welcome!
Alas, this had been the subject of the thesis I was working on until I chose to leave grad school (for personal reasons), but I never found the discipline to complete writing up my ideas. I still hoped to eventually force myself to write it and still, I suppose, entertain the fantasy of thus completing my Ph.D., but perhaps I may never develop the relevant willpower. I may as well sketch out some of the basic ideas (I am quickly copying and pasting some snippets from emails here before commuting to work, out of the fear that these starting ideas are such low-hanging fruit that once anyone else begins thinking about the problem, they would independently strike upon the same thoughts; I will return later to edit this post to make the markup prettier and the exposition clearer; this may be unreadable to start with):
I trust you understand the concepts of an “internal category”, “internal category with finite limits”, etc.; that is, the concepts of “category”, “category with (chosen) finite limits”, and so on are given by essentially algebraic theories, and thus can be given models as suitable finite-limit diagrams inside any category with finite limits.
Given a model M of [whatever essentially algebraic theory] internal to finite-limit category T, and a finite-limit preserving functor f : T -> T’, we get also a model f[M] internal to T’, taking the image in the obvious way. In particular, we can take f : T -> Set to be the global sections functor Glob = Hom_T(1, -), and thus obtain, from any finite-limit category C internal to T, a genuine finite-limit category Glob[C].
What’s more, there’s a finite-limit preserving functor from Glob[C] to T given as follows: take an object X in Glob[C] (amounting to a morphism : 1 -> Ob(C) in T) to the object Hom_C(1, X) in T (the subobject of Mor(C) constructed by appropriate finite limit), with corresponding action on the morphisms of Glob[C] using the composition structure of C. This basically amounts to an internal version of the global sections functor [more generally, we have such a functor from Hom_T(X, -)[C] to the slice category T/X for each object X, comprising a natural transformation between the corresponding functors from T to the category of finite-limit categories and on-the-nose finite-limit functors]. Let’s call this functor G_C for now, till I come up with a better name.
By an “introspective theory”, I mean:
A) a category T with finite limits [i.e., an essentially algebraic theory]
B) a category V with finite limits internal to T
C) a finite-limit preserving functor S from T to Glob[V]
D) a natural transformation J from the identity functor on T to the composition G_V . S
The idea here is that an introspective theory amounts to a theory extending the theory of finite-limit categories, with furthermore the property that every model of this theory has also an internal model of this theory, and a homomorphism into the global sections of that internal model.
Note that the theory of introspective theories is itself essentially algebraic. In particular, there is an initial introspective theory. I call this the theory of “Goedel-Loeb categories”.
Next, recall how, given a category with terminal object C internal to category with finite limits T, we defined a functor G_C from Glob[C] to T amounting to taking an object of Glob[C] to the T-definable set of its global sections. Well, I should have noted in somewhat more generality that in exactly the same way, we have a functor “Hom_C” from Glob[C]^{op} x Glob[C] to T, taking a pair of objects in Glob[C] to the T-definable set of C-morphisms between them.
From now on for a while, we’ll be working within the context of an arbitrary given introspective theory <T, V, S, J>. I’ll frequently speak in the “internal logic” of T for convenience.
Note that S[V] is a category internal to Glob[V]; in the internal logic of T, we might well say S[V] describes a category internal to V. When adopting this perspective, I shall refer to S[V] as V_1.
Note also that the action of J induces a map from Mor(V) to (G_V . S) Mor(V). That is, in the internal logic of T, we have an object S(Mor(V)) = Mor(V_1) in V, whose global sections comprise the set (G_V . S) Mor(V), into which there is a mapping from the set Mor(V). The naturality diagrams for J, along with the morphisms in T giving the FinLimCat structure of V, will cause this mapping to amount to a finite limit preserving functor from V to Glob[V_1]. Let’s call this functor f for now.
Accordingly, we can define a bifunctor of type V^{op} x V -> V given by the rule (a, b) |-> Hom_{V_1} (f(a), f(b)), the output of which I’ll refer to as [](a -> b) for evocative reasons. In the particular special case when a = 1, we will write simply []b.
(N.B.: I’ve not defined any such thing as “a -> b” on its own; there’s no assumption of cartesian closure anywhere. It is important to me to note that all the basics can be carried out in a very minimal context. For that matter, I do not impose any arithmetic structure at any point; it is even more important to me to note that the essence of Goedel coding is not to do with arithmetic, though that happens to be one medium through which it can be realized.)
I’ve hit character limits on a single post, so I’ll stop there for now, but outline some of what comes next: It is relatively straightforward to show that [] acts as a K4 modal operator, in that in addition to its bifunctoriality, it preserves finite limits in its second argument, and also comes with a canonical natural transformation from [](a -> b) to [][](a -> b) = [](1 -> [](a -> b)), which is the analogue of the modal axiom 4.
With a fair amount of more work, we can also show that it satisfies the analogue of Loeb’s theorem. Loeb’s theorem is usually stated as something like “[]([]A -> A) |- []A” (Goedel’s Second Incompleteness Theorem is the special case where A is thought of as definitional falsehood; i.e., an initial object). But I’ll want to note, first of all, that if we think of x |-> [](x -> A) as a presheaf P, that Loeb’s theorem can instead be looked at as P(P(1)) |- P(1). And indeed, we’ll have a version of Loeb’s theorem applying to suitably internal presheaves more generally than simply the representable ones.
And, secondly, I’ll state ominously that when we do get around to establishing Loeb’s theorem in this context, since we are in a category and not a mere preorder, we can further ask nontrivially about equations satisfied of the morphism taking the place of the turnstile. And what will be of particular note to us will be that the morphism we construct to establish Loeb’s theorem will act as a modalized fixed point combinator. And this will lead into various discussions of fixed point uniqueness results under various conditions. The crowning accomplishment in my eyes was the establishment of modal fixed points in certain quite general cases which are simultaneously initial algebras and terminal coalgebras.
(Also of some interest, one of the fixed points we can get in this fashion is an object X ~= [](X -> Omega), where Omega acts as a type of truth values. This models a certain pseudo-naive modal set theory (furthermore, because of the initiality and terminality results, the model will satisfy versions of both Foundation and Anti-foundation). One interesting observation is that in such a pseudo-naive modal set theory, the analogue of Russell’s paradox ends up leading not to inconsistency, but just to Goedel’s incompleteness theorem again.)
Anyway, I’ll have to wait till later to talk about any of that (or, again, to make any of this readable; I understand that it probably is just a dump of text right now).
Paul Taylor pointed out on MO that Joyal proved that
In the initial arithmetic universe $\mathcal{A}$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal{A}$.
Thank you very much, Sridhar, for your thoughts! This all sounds very interesting, and I would very much like to hear more.
I wish you the best of luck with writing up your PhD if you find the opportunity and wish to do so! It seems that your approach is a little different from the one I have in mind, which is great: I would be interested to explore both possibilities. It also means that I can hopefully avoid pursuing some line of thought which might overlap with material that you would like to include in your PhD, which I would not wish to do.
I would like to say that I agree entirely with the parenthetical remark at the end of your first comment: I also would like to abstract away from arithmetic, and it is important to me to carry out the proof in a predicative constructive setting.
Just a couple of questions for now.
1) Could you give an example (or more than one) of an introspective theory? I appreciate that this may not be easy, but it could be very helpful.
2) A related but presumably harder question: can you describe the ’theory of Gödel-Löb categories’ explicitly?
I think I see very roughly how you are trying to construct your modal operator, but get a bit lost in your second comment! If you would be able to elaborate upon the overall structure of your argument, being as precise as possible (just pointing out where there are things that need to be checked/which are just ideas at this stage), that would be extremely helpful.
To compare this approach with what I had in mind, perhaps one could say that what I am proposing is from one (but only one: what you are describing looks equally interesting) point of view more radical: I am trying to do away with the Löb’s theorem/Hilbert-Bernays-Gödel conditions path to the second incompleteness theorem altogether. In outline, what I would like to do is the following:
1) Express the internal logic of T in an ’arithmetic theory S internal to T’, namely understand Gödel numbering in a good way in categorical logic. As you say, ’arithmetic’ should not ultimately be necessary, but I’ll keep it for simplicity for now. This point is the one which seems most crucial to me, and is the one which my original post was about.
2) Carry out Lawvere’s diagonal argument to prove the first incompleteness theorem in T, namely using the internal logic of T instead of the usual ’external’ reasoning. I am reasonably confident that this step can be carried out without too much trouble given the first step.
That remark of Taylor is too cryptic to be helpful to me, I’m afraid, David!
If someone could explain carefully how this statement (or the slightly different one in a different comment of Taylor on MathOverflow) expresses Gödel’s second incompleteness theorem, that would be a very good start!
I gather it is something like as follows: An arithmetic universe is, we gather, the minimal theory that contains an internal model of itself and can interpret arithmetic. If the initial/free arithmetic universe exists and is nontrivial, then it has an internal model of itself in which 0=1. But Taylor is not exactly responsive to comments/questions at his answer, for whatever reason.
Thank you, yes, I would guess that what you describe is roughly the statement that Taylor describes in his other comment. I would guess that the statement in the comment you linked to is roughly that there is no proof of falsity.
However, it is the precise details that are unclear to me. Particularly the distinction between logic in the starting category (say the initial arithmetic universe) and the logic in the internal model: making this precise is one of my questions in my original post, and I feel that it is the key to the story.
One fundamental question is: what is meant precisely by ’an internal model’ here?
A related, but very basic, question of a more general nature, which I have not yet thought carefully through myself, but which could help to clarify things, is the following: is there a good notion of internal logic of an internal category? How does this work precisely? What are the assumptions on the external category?
Maybe the idea is then that the internal model is some kind of internal category which (in the case of the initial arithmetic universe) has the same logic as the external one (again, one important point would be to make this precise, perhaps using the formalism of hyperdoctrines).
If the previous paragraph can be made precise, then it seems to me that Taylor’s two statements both express (in different ways) the inconsistency of the logic of the external category. I don’t see how they express Gödel’s second incompleteness theorem, and indeed it would seem to me that Taylor claims in the first MathOverflow comment, the one I have linked to, that Joyal proves that the logic of the external category is inconsistent, which would of course be nonsense (or revolutionary)!
Presumably something I have written is therefore not what Joyal/Taylor have in mind. Perhaps the ’internal logic’ does not agree with the external one, and the consistency statement says something about the internal logic. But then: what exactly does it say? How does proving that something (internal or external) is inconsistent correspond to the second incompleteness theorem?
I would rather think that, using the diagonal argument and a Gödel numbering as I outlined above, one would show that an assumption of consistency leads to a contradiction (or show something analogous, that may be better from a constructive point of view).
Hopefully it is clear from all this that clarifying the basic questions around internal logic and internal models seems crucial.
One has to read carefully.
In the initial arithmetic universe $\mathcal{A}$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal{A}$.
On the one hand, that means $A (1, 0)$ is not empty. On the other hand, $A (1, 0)$ is not inhabited. So it follows that, in the internal logic of $\mathcal{A}$, the theory of arithmetic universes is neither consistent (i.e. “every arithmetic universe is non-degenerate”) nor inconsistent (i.e. “every arithmetic universe is degenerate”).
Thank you, Zhen Lin, this is helpful. I was referring to the other statement of Taylor, in the comment that I linked to, but your point still stands. I believe that I now understand the structure of the argument, namely:
1) one proves that $G \cong 0$ does not hold (in the statement in Taylor’s first comment), or that $A(1,0)$ is not empty (in the statement in Taylor’s second comment), noting, as you remark, that this does not imply that the internal logic of the initial arithmetic universe is inconsistent, just that it is not provably consistent;
2) if the internal logic of the initial arithmetic universe contained a proof of its own consistency, we would have a proof that $G \cong 0$ (respectively $A(1,0)$ is empty).
We conclude from 1) and 2) that the internal arithmetic universe does not contain a proof of its own consistency, as we wished to establish.
If this is correct (and, again, the fifth paragraph of my previous post can be made precise), then I see now how Joyal/Taylor’s statement expresses the second incompleteness theorem.
My idea for proving 1) would still be as in message #5 in this thread, except that, given a precise understanding of internal model/its internal logic, some things have been resolved with regards to the first part of proof idea. It would remain to carry out the Gödel numbering, and then to try to carry out the second part, namely an internalisation of the diagonal argument à la Lawvere.
Re #8
what is meant precisely by ’an internal model’ here?
the theory of an arithmetic universe is, I gather (modulo precise implementation details), expressible in precisely the internal logic available in an arithmetic universe. I’m sorry for being so brief, but I only have the comments of Taylor and (in her articles) of Maietti to work from, neither of which actually cover Joyal’s result, merely formalising the notion of arithmetic universe, based on examples in Joyal’s talk.
No problem, I realise that this is the case. My questions were intended for anyone who might wish to chip in, and indeed partly rhetorical.
I think that I begin to see how the formalism of internal models, and so on, needed here can be defined. I plan to continue to work on the details of trying to internalise Lawvere’s diagonal argument, and will write again once I have something to add. In the meantime, thoughts and discussion are of course welcome!
Back then I had missed the point alluded to by Sridhar Ramesh in #2 and #3 above, regarding the perspective on incompleteness via Löb’s theorem.
I have given it a stub entry Löb’s theorem and linked to it from “incompleteness theorem”. Experts please check and expand
Re #2:
Alas, this had been the subject of the thesis I was working on until I chose to leave grad school (for personal reasons), but I never found the discipline to complete writing up my ideas. I still hoped to eventually force myself to write it and still, I suppose, entertain the fantasy of thus completing my Ph.D., but perhaps I may never develop the relevant willpower.
This story has a happy ending! (Well, I shouldn’t call it an ending, but a happy continuation!). I did in fact eventually complete writing this thesis, and thus I completed my PhD at long last this summer. In particular, I am profusely grateful to the nLab’s own Michael Shulman, who read my dissertation in great detail, offered many helpful suggestions, and served on my defense committee.
Anyone curious can see the filed dissertation here. That said, I will be incorporating more of Michael’s revision suggestions for a cleaned-up version which I will put on arXiv, and also as I work to turn this into papers to submit to journals. So it may be better to wait for those, for easier reading.
Still, I am very excited to have been able to do this!
Just seeing this now. Belated congratulations to you, Sridhar!
Thank you, Todd!
1 to 16 of 16