New posts will be coming, based on discussions in the virtual seminar on Slack.

# The Free Introspective Theory; aka, the theory of GL-categories

Let us say a GL-category \footnote{so named for reasons to be explained later} is a structure <L, L’, F, F’> (which, in typical abuse of language, we may sometimes identify with simply the name of L) of the following sort:

A) A lexcategory L

A’) A lexcategory L’ internal to L

B) A lexfunctor F from L to Glob(L’) \footnote{Presentational TODO: it will be useful at some point to specify a convention that a functor from an actual category to an internal category always means a functor from the former to the globalization of the latter; once establishing this convention, we can drop the distracting explicit “Glob”s of the sort here.

In a similar vein, it will also be useful to explicitly establish the convention that a lexfunctor H : C \to D can also be implicitly regarded as a homomorphism : Glob(C’) \to Glob(H[C’]) for any structure C’ internal to C in the natural way}

B’) A lexfunctor F’ from L’ to F[L’] internal to L

C) Such that F(F(x)) = F'(F(x)) for any object/morphism x in L, construed appropriately (I’m writing with some abuse of notation (see previous footnote), but this condition is similar to the third condition in the description of introspective theory homomorphisms)

C’) Such that, in the internal logic of L, we have that F'(F'(x)) = F[F’](F'(x)) for any object/morphism x in F[L’]

Note that the theory of GL-categories is essentially algebraic and can thus be identified with a lexcategory (the generic lexcategory with an internal GL-category), which for now let us call TheoryGL.

In the standard way as for any essentially algebraic theory, we also get a notion of GL-category homomorphism; a GL-category homomorphism between GL-categories <L_1, L_1′, F_1, F_1′> and <L_2, L_2′, F_2, F_2′> is

- A lex functor H : L_1 \to L_2
- Such that H[L_1′] = L_2′
- Such that H[F_1(x)] = F_2(H(x)) for any object/morphism x in L_1, where the H on the left acts as a functor from Glob(L_1′) to Glob(H[L_1′]) = Glob(L_2′) in the natural fashion
- Such that H[F_1′] = F_2′

Now observe that TheoryGL (the generic lexcategory with an internal GL-category) can be equipped as an introspective theory <TheoryGL, L, S, Q> as follows:

- TheoryGL is the generic lexcategory with an internal GL-category <L, L’, F, F’>.
- L, thus, is the underlying lexcategory of that internal GL-category.
- To specify S now is, by the nature of TheoryGL and of S as a lexfunctor from TheoryGL to Glob(L), to specify an L-internal GL-category; specifically, we will take S to correspond to the L-internal GL-category <L’, F[L’], F’, F[F’]>. Note that this choice is indeed a GL-category, with structure/conditions A, B, and C in such S corresponding to structure/conditions A’, B’, and C’ in <L, L’, F, F’>, and further structure/conditions A’, B’, and C’ in S obtained by application of F to the former, respectively. [TODO: Though this is indeed a complete description of what is going on here, this language may be clunky… Perhaps reword in some fashion]
- Finally, to specify Q is to specify a GL-category homomorphism from our generic GL-category <L, L’, F, F’> to the globalization (within TheoryGL) of the L-internal GL-category S = <L’, F[L’], F’, F[F’]>. For this, we take the underlying lexfunctor of that homomorphism to be F. Verifying that F is indeed a GL-category homomorphism requires verifying three further conditions (as in the bulleted list above), which in this case come out to F[L’] = F[L’] (trivially true), F(F(x)) = F'(F(x)) interpreted suitably (true by condition C for L as a GL-category), and F[F’] = F[F’] (again, trivially true).

This completes the definition of <TheoryGL, L, S, Q> and demonstration of it as an introspective theory.

Next, I intend to show that this is in fact the initial introspective theory; that is, that it has a unique introspective theory homomorphism into any other introspective theory <T, T’, S_2, Q_2>. [TODO: I really need to learn how to pick better names for variables…]

Such a homomorphism amounts to a lexfunctor H from TheoryGL to T satisfying certain conditions (specifically, that H[L] = T’ and that the identity H(S(x)) = S_2(H(x)) holds, suitably interpreted), which is to say (by the nature of TheoryGL) such a homomorphism amounts to a T-internal GL-category <T’, . [TODO: Finish]

[TODO: Discuss more generally the free introspective theory extending a given essentially algebraic theory extending the theory of lexcategories, given in essentially the same manner (replacing lexcat with whatever, lexfunc with whatever-homomorphism), giving rise to GL-(whatevers) (e.g., GL-toposes, GL-(lex)categories with coproducts, etc.)]

Finally, let us show that given any introspective theory <T, T’, S, Q>, we have that T can be interpreted as a GL-category as well; specifically, we will have a GL-category <T, T’, S, Q interpreted suitably> [TODO: Finish]

# GLS-categories

This is a slight digression of no immediate relevance, but it’s something to mention at some point anyway:

Recall that, by design, if <T, T’, S, Q> is an introspective theory, then from every model M of T (in the sense of a lexfunctor from T to Set), we obtain another model M’ of T internal to M (this is induced by S), and a homomorphism f_M : M -> Glob(M’) (this is induced by Q). [For convenience, I shall refer to Glob(M’) as M* in the rest of this post.]

It may be that f_M is an isomorphism or not. (This corresponds to the question of whether |- []A reliably entails |- A or not). Let’s call those M with this property GLS-categories, for their connection to GLS modal logic (above and beyond mere GL).

It’s too much to hope for, for G2IT/Loeb’s theorem type reasons, that f_M be an isomorphism in every model of T. Nonetheless, this may be true in particular models. At any rate:

Given any model M of T, we obtain in the above fashion a chain M –f_M–> M* –f_{M*}–> M** –f_{M**}–> … of models of T and homomorphisms from each into the next.

Taking the colimit of this chain, we obtain a model N of T such that f_N is indeed an isomorphism (this is a consequence of the finitary nature of lex-logic: each piece of structure in N* ends up coming from M***… for some finite positive number of *s, and thus in the image of f_{M**…} for some finite number of *s, and thus in the image of f_{N}).

Conversely, of course, if f_M were already an isomorphism, the entire chain would be trivial and its colimit would be M again.

Thus, we see that the GLS-categories form a reflective full subcategory of the GL-categories, with the above process of obtaining N from M as the reflector.

# Introspective Theory Homomorphisms

Recall that an introspective theory consists of four pieces of data <a lexcat T, a lexcat T’ internal to T, a lexfunctor S from T to Glob(T’), and a natural transformation Q>. The full definition was given in a previous post. Of note, the definition is essentially algebraic. Thus, in a completely standard way, we can work out a corresponding notion of homomorphism between introspective theories. The purpose of this note is to make that notion explicit, as preparation for describing free introspective theories in an upcoming note.

Given two introspective theories <T1, T1′, S1, Q1> and <T2, T2′, S2, Q2>, an introspective theory homomorphism between them consists of:

*) A lexfunctor f from T1 to T2 [footnote: this functor will be taken for our purposes to preserve lex structure on the nose (sending chosen limits to chosen limits). This is what using the standard notion of essentially algebraic to formalize lexcats yields; as noted before, we would like eventually to generalize away from this, but doing so in a fully satisfactory way would require dipping our toes into infinity categories and therefore complicate this initial exploration unduly].

*) Such that f[T1′] = T2′

*) And such that Glob(f) . S1 = S2 . f, where Glob(f) : Glob(T1′) -> Glob(T2′) is the functor induced by f in the obvious way.

(In other words, for any morphism (or object, but it suffices to consider morphisms) in T1, we get the same result whether we first turn it into a global section of Mor(T1′) by applying S1, then turning it into a global section of Mor(T2′) by applying f, as we do if we first turn it into a morphism of T2 by applying f, then turn it into a global section of Mor(T2′) by applying S2.

In other words, we have a commutative square where the top-left node is Mor(T1), the top-right node is Hom_{T_1}(1, Mor(T1′)), the bottom-left node is Mor(T2), and the bottom-right node is Hom_{T_2}(1, Mor(T2′)). The map from top-left to top-right is the action of S1 on morphisms. The map from bottom-left to bottom-right is the action of S2 on morphisms. And on both sides there are maps from top to bottom being the action of f on morphisms (that this is “well-typed” on the right follows from the previous condition that f[T1′] = T2′)

[At some point, for this and other commutative diagrams, I will either draw them out by hand and upload a photo, make diagrams nicely with Paul Taylor’s package and upload a photo, or learn how to make diagrams nicely with some other package that directly interfaces with the WordPress blog])

*) And, finally, such that for any object A in T1, we have that f(Q1_A) = Q2_{f(A)}.

Coming up next: an explicit (or more explicit than just “It is what it is”) construction of the free introspective theory.

# Towards a Categorical Loeb’s Theorem (Pt. 1)

(This post isn’t quite ready yet, but I’m posting it anyway to demonstrate that I’m getting at least a modicum of stuff done and perhaps buoy me to get more done in response to feedback.)

Some background and notation:

For objects A, B of an introspective theory T with designated internal category T’ and lex functor S : T -> Glob(T’), we define the object [](A -> B) of T as Hom_{T’}(S(A), S(B)). [In general, it will be convenient to suppress such uses of S where obvious and necessary to consider objects of T as objects of T’, etc.; thus, I might instead have written, as abuse of notation, Hom_{T’}(A, B)].

Note that this is genuinely a binary operation: I do not presume there is any such object as A -> B and apply some unary operator [] to it; in particular, I do not presume cartesian closure of T. I have chosen this [](A -> B) notation, which is potentially misleading in this regard, because it is nonetheless fruitfully suggestive of certain analogies with modal logic which we will explore in the future.

It will, however, be convenient to use the shorthand []A for [](1 -> A) as well. (In the special case where we DO make cartesian closure assumptions, it will turn out that the bifunctor [](A -> B) is naturally isomorphic to []Exp(A, B) (i.e., [](1 -> Exp(A, B))), where Exp(A, B) is the exponential given by the cartesian closed structure. But, again, we do not need such assumptions.)

Note that [](A -> B) is contravariantly functorial in A, and covariantly lex-functorial in B.

Finally, recall that the fourth axiom defining an introspective theory gives us a natural transformation 4_A : A |- []A [the name “4” here serves as a coincidental pun: we obtain this natural transformation by the fourth axiom defining introspective theories, but it also corresponds to the axiom standardly considered under the name “4” in modal logic].

Alright, that is all the background we need for now. Here is the observation (again, this is a special case which we shall seek to generalize):

Suppose given a morphism e : Z |- [](Z -> A) and d : [](Z -> A) |- Z such that e . d = id. (That is, suppose that we have some [](Z -> A) as a retract of Z).

Then, let w : [](Z -> A) |- []A be defined by first constructing the map 4_Z . d : [](Z -> A) |- []Z and combining this with the identity [](Z -> A) |- [](Z -> A) to get a map [](Z -> A) |- [](Z -> A) & []Z, and finally, finishing off with the composition operator on T’ of type [](Z -> A) & [](1 -> Z) |- [](1 -> A) to get, overall, a map [](Z -> A) |- []A. (Does that make sense? Basically, w(m) = m [a morphism from Z to A] composed in T’ with 4_Z(d(m)) [a morphism from 1 to Z] to get a morphism from 1 to A which is something like “the self-application of” m).

Now suppose given f : []A |- A. We can then construct f . w . e : Z |- A.

Applying S to this (taking morphisms in T to morphisms in Glob(T’)), we get a globally defined element q = S[f . w . e] of the object [](Z -> A). [Footnote: There is a slight ambiguity/difficulty in saying things like “S[f . w . e]”, in that we can interpret this as a morphism in Glob(T’) from Z to A, or a morphism in T from 1 to [](Z -> A). In this case, it is the latter perspective I am interested in at the moment. Ideally, I would develop better language for dealing with this sort of issue…]

We can now apply f . w : [](Z -> A) |- A to q to get a globally defined element f . w . q of A.

I intend now to demonstrate that w . q = S[f . w . q], and thus we have that f . w . q is a fixed point of the map x |-> f . S[x].

To demonstrate this, observe that w . q = w . S[f . w . e] = S[f . w . e] (a global element of [](Z -> A)) composed in T’ with 4_Z . d . S[f . w . e] (a global element of []Z).

By naturality of 4, we have that 4_Z . d . x = S[d] composed in T’ with 4 x, for any global element x. [TODO: Clarify]

By functoriality of S, we have that S[f . w . e] composed in T’ with S[d] composed in T’ with 4 S[f . w . e] = S[f . w . e . d] composed in T’ with 4 S[f . w . e].

As e . d = id and S[f . w . e] = q, this comes out to S[f . w] composed in T’ with 4 q. Which comes out to S[f . w. q] as desired. [TODO: What exactly is going on here? Clarify].

This completes the proof of the stated theorem. Note that this provides a strengthened analog to Loeb’s theorem (given f : []A |- A, we conclude the existence of f . w . q : 1 |- A, but with furthermore a fixed point property which goes unnoticed in mere propositional logic where we do not care about equalities of parallel such sequents-as-morphisms).

Note also that we only ever use the object A in terms of the maps into A; we will see soon that we can generalize from A to any suitably definable presheaf.

(TODO: Talk also about how to obtain Z, [](Z -> A), e, d via bootstrapping this theorem, getting Z isomorphic to [](Z -> A) with application of this theorem to suitable presheaf. This will require also talking about generalization where e needn’t quite be a proper morphism.)

# A Categorical Account of Self-Reference

Goedel’s incompleteness theorems (and associated phenomena such as Loeb’s Theorem) are well-known to have to do with a certain kind of formal logical “self-reference”, and in giving a categorical account/generalization of these phenomena, we will want to capture, at the best level of abstraction, exactly the structures exhibiting the relevant sort of “self-reference”. In this post, we will begin describing the categorical structures which do so.

Specifically, we will be interested in logical theories T whose models have the ability to “refer” to themselves, in the sense that any model M of T has “embedded” [TODO: get rid of new notion of “embedded”; rephrase in terms of “internal”, where M itself is viewed as a category] within it some designated model M’ of T which “acts like” M.

Let’s unwrap this. What do we mean when we ask for M’ to “act like” M? It turns out that, for our purposes, what we require is just that we also have some designated homomorphism from M to M’.

And what do we mean by terms like “logical theory”, “embedded model”, “homomorphism”, etc.?

- Well, we shall be interested in an account of “logical theory” which is particularly categorically natural: by the informal term “logical theory” above, what we mean is a category with finite limits (what is also called a “lex category” or a “lex theory”). This is thought of as consisting of the sorts, definable terms, and provable equalities of our theory, which we shall assume to be suitably rich as to contain product and equalizer sorts.
- A model of a lex theory T is then a finite-limit-preserving functor (i.e., “lex functor”) from T to some other lex theory S. An ordinary model takes S here to be Set, the category of “actual” sets, functions, and equalities, but as categorical logicians, we are just as well interested in models valued in other categories. (The general case, with codomain S, is sometimes called an S-valued model of T, or a model of T internal to S)
- Note that any S-valued model of T gives rise to an ordinary model of T, by composing with the lex functor Hom(1, -) from S to Set. We shall call this the “globalization” of the model [footnote: this is a new term I am coining, by analogy with the standard term “global sections functor” for Hom(1, -)].
- Note that, for any lex theory T, the identity functor from T to itself will count as a model; indeed, in some sense, this is the simplest, archetypal, or “generic” model of T.

- And a homomorphism between two models M and M’ of T valued within the same category amounts to a natural transformation between the two corresponding parallel functors. (One might think we need to say “lex natural transformation” here, but it conveniently turns out the appropriate notion of “lex natural transformation” is identical to “natural transformation” simpliciter)
- Given an ordinary model M of T, and an S-valued model M’ of T, we may, with slight looseness of language, use “homomorphism from M to M’ ” to mean “homomorphism from M to the globalization of M’ “.

- A model of a lex theory T is then a finite-limit-preserving functor (i.e., “lex functor”) from T to some other lex theory S. An ordinary model takes S here to be Set, the category of “actual” sets, functions, and equalities, but as categorical logicians, we are just as well interested in models valued in other categories. (The general case, with codomain S, is sometimes called an S-valued model of T, or a model of T internal to S)

- Note that the theory of categories is itself given by a lex theory. In fact, for that matter, the theory of lex categories [footnote: with chosen finite limits] is also given by a lex theory [footnote: the corresponding interpretation of “homomorphism”, in the sense we’ve indicated for lex theories in general, will be “lex functor preserving finite limits on the nose”. We can also axiomatize via a lex theory the concept of “two lex categories and a functor between them which preserves finite limits not necessarily on the nose”, but this will not be the default notion of homomorphism for the lex theory describing lex categories. This discrepancy is one of the slight blemishes of doing the work we are doing in the context of ordinary categories rather than an infinity-categorical context, but will not be a major issue for our purposes.]. Thus, we can speak not only of actual (lex) categories (that is, lex functors from the lex theory of (lex) categories to Set), but also of (lex) categories internal to any lex category S (that is, lex functors from the lex theory of (lex) categories to S).
- [Yes, I know this is a little confusing, with various concepts being repeated on both an object- and meta-level (and even this noting of the source of the confusion may itself be confusing); I apologize, and don’t yet know how to make this clearer. TODO: Make this clearer.]

- By an “embedded model” [footnote: This is a non-standard term which I am now coining] of T within S, what I mean is a model of T valued in the globalization of S’, for some lex category S’ internal to S. (Note that this is distinct from an “internal model of T within S”, in the standard jargon [i.e., a lex functor from T to S]).
- Note that an S-embedded model of T induces an S-valued model of T, via an analogue of the “globalization” procedure discussed above (with S generalizing the role previous played by Set) . [TODO: Discuss this at more length/with more explicit details in separate post on “globalization”]
- Continuing in this vein of generalization, given an S-valued model M of T, and an S-embedded model M’ of T (i.e., a Globalization(S’)-valued model of T for some S’ internal to T), we may, with looseness of language, use “homomorphism from M to M’ ” to mean “homomorphism from M to the globalization (in the sense of the previous bullet point) of M’ “. [This is precisely analogous to the previously discussed looseness, with S generalizing the role played by Set]

So let us now return to, and formalize, the topic of interest we set out at the beginning of this post: logical theories T whose models have the ability to “refer” to themselves, in the sense that any model M of T has “embedded” within it some designated model M’ of T with a designated homomorphism from M.

- We see now that this T is to be a lex category
- Among the models of T is, automatically, the generic model M given by the identity functor from T to itself
- This generic model is to have “embedded” within it another model M’ of T; this means T must have some internal lex category C, and M’ is to be a model of T internal to C
- I.e., we must also have a lex functor from T to the globalization of C
- (Note that this M’ embedded within this generic model of T automatically induces a corresponding embedded model of T within any other model of T as well)

- Finally, this generic model M is to have a designated homomorphism H to M’
- Formally, this amounts to a natural transformation from the identity functor on T (which defines the model M) to the endofunctor on T corresponding to the “globalization” of M’ [TODO: make this more clear; refer to separate “globalization” post]
- (Again, note that having this in the generic model automatically induces a corresponding homomorphism in every model of T)

Such a structure (consisting of the data specifying T, as well as C, M’, and H) we shall call an “introspective theory”. [footnote: It was cheekily suggested by Lawrence Valby and Alex Kruckman to refer to this as an SR-category, the “SR” standing for “self-reference”. You may use that name as well if you like…].

- Note that, though we did not do explicitly, it is straightforward and mechanical from the kind of description we gave to see that the theory of introspective theories is itself a lex theory. This gives us free constructions syntactically in the traditional fashion.
- In particular, there is a free (i.e., initial) introspective theory, which I shall refer to as the theory of “GL-categories”, for lack of a better name (the “GL” here standing for “Goedel-Loeb”).
- In future posts, we will find an alternate, in some sense more direct or explicit description of how to recognize GL-categories (that is, models of the free introspective theory) in the wild.

- In particular, there is a free (i.e., initial) introspective theory, which I shall refer to as the theory of “GL-categories”, for lack of a better name (the “GL” here standing for “Goedel-Loeb”).