# Questions tagged [categorical-logic]

The tag has no usage guidance.

40 questions
104 views

### How to turn a limit sketch into an essentially algebraic theory?

An essentially algebraic theoery, according to Adamek and Rosicky (second definition on nlab), consists of a many-sorted signature $\Sigma$ (consisting of function symbols on sorts $S$), a set $E$ of ...
97 views

### Internal equality for Eq-fibrations' morphisms

I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here. In Jacob's Categorical logic and Type ...
916 views

### Formalizations of the idea that something is a function of something else?

I'll state my questions upfront and attempt to motivate/explain them afterwards. Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory? More ...
487 views

### Set-theoretical multiverses and their representation as functors? Why *the* multiverse?

In some related MO questions like The set-theoretic multiverse as a (bi)category it is discussed how one might represent the multiverse (see The set-theoretic multiverse) in a category theoretic way, ...
626 views

### Does foundation/regularity have any categorical/structural consequences, in ZF?

(Prompted by reflection on this old answer, and its suggestion of the “harmlessness” of the axiom of regularity.) In ZFC, one may justify the axiom of foundation (AF, aka the axiom of regularity) as ...
404 views

### Proof assistant for working in weaker foundations?

In some of my works I need to prove some results within the internal logic of categories with not much structures (like pretoposes or even just categories with finite limits). The kind of things I ...
2k views

### How do we construct the Gödel’s sentence in Martin-Löf type theory?

In Martin-Löf dependent type theory (MLTT), under the proposition-as-types correspondence, we sometimes say that a proposition $A$ is true if the type $A$ is inhabited. However, there is no doubt that ...
688 views

### Grothendieck toposes and logic

I am searching results in which one can extract logic information from a topological (Grothendieck topos) perspective (such as Gödel's Completeness Theorem and Deligne's Theorem ("theorem by P. ...
501 views

### Model existence theorem in topos theory

One of most classical and somehow striking result in classical model theory states: A consistent first order theory $T$ has a model. Few considerations are needed. This result is not true for ...
134 views

### What does the localic reflection of a classifying topos classify?

Let $\mathbb{T}$ be a geometric theory. Let $\mathrm{Set}[\mathbb{T}]$ be its classifying topos, such that geometric morphisms from any (cocomplete) topos $\mathcal{E}$ into $\mathrm{Set}[\mathbb{T}]$ ...
942 views

### Precise relationship between elementary and Grothendieck toposes?

Elementary toposes form an elementary class in that they are axiomatizable by (finitary) first-order sentences in the "language of categories" (consisting of a sort for objects, a sort for morphisms, ...
284 views

### Geometric Theories have models in any Grothendieck Topos?

This question is linked to this one. My question is: Is it true any consistent geometric (here I mean coherent theory, different books have different standards) theory $T$ has a model in a ...
376 views

### Brouwer's Theorem in the free topos?

In Introduction to Higher-Order Categorical Logic, Lambek & Scott remark that Brouwer's Theorem (all functions $\mathbb{R}\to\mathbb{R}$ are continuous) holds in the free topos $\mathcal{T}$. ...
276 views

### Constructing a topos from a Heyting algebra

It is true that, given any topos $\mathcal{C}$ with a terminal object $1_\mathcal{C}$, $Sub(1_\mathcal{C})$ is a Heyting algebra. Now suppose that we start with a Heyting algebra $H$. Is it always ...
210 views

### Diagrams in an Elementary Topos

Let $T$ be a sheaf topos and $I$ a small category. Then the functor category $[I,T]$ is also a sheaf topos. Now let $E$ be an elementary topos (cartesian closed category with finite limits + subobject ...
385 views

649 views

### Is it possible for a theorem to be constructive only in a non-constructive metatheory?

There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of ...
213 views

### Validity of equations in a topos

To simplify consider simple algebraic theories (universal algebra) A and L, but the question applies to geometric theories. 1) Syntactically, we can interpret L in A if we can define the operations ...
1k views

### Internal logic of the topos of simplicial sets

I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, ...
196 views

### Sketches for categories of models of complete theories

In Accessible categories : the foundations of categorical model theory, chapter 3 p.58, Makkai and Paré claim that there is "an (obvious) identification of a class of sketches so that the categories ...
946 views

### On Joyal's completeness theorem for first order logic

In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first ...
411 views

### Further relation between monads and theories

This question want to be a follow up of the following question. In that thread I was interested in understanding relation between various presentation of algebraic theories. In particular in Eduardo ...
2k views

### Is there a categorical proof of Gödel's incompleteness theorem?

A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new ...
376 views

### Proof by contradiction in a topos

In a topos which is not Boolean topos, can we use proof by contradiction?
2k views

### What can be expressed in and proved with the internal logic of a topos?

The title of this post expresses what I really want, which is to learn how to wield the internal logic of a topos more effectively. However, to bring it down to earth, I'll ask a few basic questions ...
661 views

### Category of Judgements?

I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...
2k views

### The set-theoretic multiverse as a (bi)category

Joel Hamkin's The set-theoretic multiverse has featured in MO questions before, e.g., here and here. But I was wondering about the best category theoretic angle to take on it. In the paper Joel ...
2k views

### What do coherent topoi have to do with completeness?

There is a theorem of Deligne in SGA4 that a "coherent" topos (e.g. one on a site where all objects are quasi-compact and quasi-separated) has enough points (i.e. isomorphisms can be detected via ...
4k views

### Au revoir, law of excluded middle?

In what way and with what utility is the law of excluded middle usually disposed of in intuitionistic type theory and its descendants? I am thinking here of topos theory and its ilk, namely synthetic ...
7k views

### Lawvere's “Some thoughts on the future of category theory.”

In Lecture Notes in Mathematics 1488, Lawvere writes the introduction to the Proceedings for a 1990 conference in Como. In this article, Lawvere, the inventor of Toposes and Algebraic Theories, ...