# Questions tagged [categorical-logic]

The categorical-logic tag has no usage guidance.

67
questions

29
votes

2
answers

1k
views

### Applications of Categorical Logic to Logic

This is definitely a very open ended question.
I have been studying Categorical Logic for a while now --- I've read Sheaves in Geometry and Logic, Adámek & Rosický's Presentable Categories, ...

11
votes

1
answer

420
views

### Are flat functors out of a finite category necessarily finite?

Note: I've originally asked this question on math stack exchange, but I have learnt that this is the better place to ask for research level questions, so I have deleted the original question there.
...

12
votes

0
answers

239
views

### Intuitionistic proofs of propositional formulae versus natural transformations between finite sets

The setup: Given a formula $\varphi$ of intuitionistic propositional logic (i.e., made from the connectors $\Rightarrow$, $\land$, $\lor$, $\top$ and $\bot$ from propositional variables $A,B,C,\ldots$)...

3
votes

1
answer

90
views

### How to represent morphisms in a fibration in the internal type theory

Given a fibration $p:\mathcal{E \to B}$, we can work with a minimal type theory with semantics in $p:\mathcal{E \to B}$, its internal type theory.
The type theory for $p$ is dependent, with contexts ...

7
votes

1
answer

411
views

### The idempotence of Mike Shulman's "Stack semantics"

I am struggling to understand lemma 7.20 of the paper Stack Semantics and the Comparison of Material and Structural Set Theories by Mike Shulman (arXiv:1004.3802). It contains formal sequents of the ...

14
votes

0
answers

342
views

### Comparing algebraic and analytic spaces through the universal property of classifying topoi

$\newcommand\kAlg{k\mathrm{Alg}}\DeclareMathOperator\Zar{Zar}\newcommand\Mnf{\mathrm{Mnf}}$I apologize beforehand if my question is naïve. I must admit that I do not know much about analytic/smooth ...

4
votes

0
answers

264
views

### Morally free toposes are free?

Let $C$ be a category with finite limits. Sometimes people say that $\mathsf{Psh}(C)$ is a free topos, and indeed such a name is consistent with the framework of lex colimits by Garner and Lack, or ...

6
votes

1
answer

289
views

### Linear logic and linearly distributive categories

I asked this question ten days ago on MathStackexchange (see here). Despite having placed a bounty on the question, I have not received any answers or comments until now. Following Nick Champion's ...

13
votes

1
answer

547
views

### Ultracategories with one object

Historically, the theory of ultracategories was invented by Makkai to prove a strong conceptual completeness theorem for first-order logic, roughly: if $T$ and $S$ are two first-order theories such ...

5
votes

2
answers

229
views

### Why does the category of definable sets of $T^\mathrm{eq}$ have coproducts?

For each first-order theory $T$ there is an associated weak syntactic category, sometimes also called "the category of definable sets of $T$" and denoted $\mathrm{Def}(T)$.
Also, for each ...

11
votes

2
answers

383
views

### Equivalence between geometric theories and frames internal to the free topos

What is a reference for "the equivalence between geometric theories and frames internal to the free topos"? [1] This seems to be an extremely interesting theorem.
[1] André Joyal, “A crash ...

5
votes

1
answer

229
views

### Internal language proof of Lawvere's fixed point theorem for cartesian closed categories

This proof of Lawvere's fixed point theorem suggests (since it uses $\lambda$ notation) that it is written in the internal language of cartesian closed categories (which is the $\lambda$-calculus, as ...

5
votes

3
answers

617
views

### What are some interesting hyperdoctrines that are not classical models?

Short version: what are some interesting hyperdoctrines for classical (not intuitionistic) first-order logic, that are not models in the traditional sense? (Where the terminal and initial ...

5
votes

1
answer

383
views

### What structure do all kinds of theories, models, interpretations, proofs and all that form?

This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only ...

3
votes

1
answer

150
views

### Images of complemented subobjects in hyperconnected toposes over Boolean bases

Let $S$ be a Boolean topos.
Let ${f : E \rightarrow S}$ be a hyperconnected geometric morphism.
For $s$ in $S$ and $x$ in $E$ let ${\pi : f^* s \times x \rightarrow x}$ be the obvious projection in $E$...

6
votes

2
answers

310
views

### Images of complemented subobjects in toposes

Let ${f : E \rightarrow S}$ be a geometric morphism (between toposes).
For $s$ in $S$ and $x$ in $E$ let ${\pi : f^* s \times x \rightarrow x}$ be the obvious projection in $E$.
Let ${u \rightarrow f^*...

5
votes

1
answer

258
views

### Universal property of the codomain fibration

Let $\mathcal{C}$ a category with pullbacks. Does $\mathsf{cod}: \mathcal{C}^{\to}\to\mathcal{C}$ have any kind of universal property in the category of (co)fibrations over $\mathcal{C}$? I'd want it ...

13
votes

0
answers

239
views

### Birkhoff's HSP theorem in categories other than $\mathbf{Set}$

Fix a category $C$ with finite products and a set $L$ of function symbols (each equipped with an arity in $\mathbb N$).
An $L$-algebra in $C$, $\mathbf A=(A,(f^\mathbf{A})_{f\in L})$, is given by some ...

10
votes

0
answers

386
views

### How do properties of a partial order $\mathbb{P}$ affect the logic of the functor category $\mathsf{Set}^\mathbb{P}$?

$\DeclareMathOperator\true{\mathsf{true}}$I am very suspicious the answer to this (family of) question(s) is well-known, but I couldn't find anything after a bit of searching so I'll ask anyway.
I am ...

13
votes

4
answers

1k
views

### Two interpretations of implication in categorical logic?

I am a bit confused about the interpretation of "implication" in the standard treatment of categorical logic, for example in [Bart Jacobs 1999] "Categorical Logic and Type Theory".
...

7
votes

0
answers

160
views

### Examples of Heyting categories that are not toposes?

When explaining how Heyting categories can model first order logic it would be nice to be able to give some small example and contrast it with Set-semantics. I realized however that I don't know of ...

5
votes

0
answers

68
views

### Relative completeness of a relative cocompletion of a subcategory

I'm going to use the language from Lack and Rosicky's Notions of Lawvere theory, but I won't be touching on actual enriched category theory.
Suppose I have a category $\mathbb{C}$ with a class of ...

1
vote

0
answers

106
views

### Aggregations (e.g., cardinality, indexed sums/products) internal to a syntactic category?

Note: Expanded and rephrased, per Todd's question below.
Suppose that we have a set-valued functor $S:\mathcal{C}\to\mathbf{Sets}$, and an arrow $p:Y\to X$ such that $S(p)$ has finite fibers.
From ...

10
votes

0
answers

374
views

### Internal logic in topos theory, monoidal categories, and quantum mechanics

To obtain the internal logic of a topos (roughly speaking), we associate a type of free variable with an object, and a statement about such a variable with a subobject of that object. Intuitively, the ...

9
votes

1
answer

434
views

### Free models of finitely presented essentially algebraic theories in elementary toposes?

The following result is well-known in folklore (I think), but I’ve been unable to find a reference in the literature:
Let $T$ be a finitely presented essentially algebraic theory, and $\newcommand{\...

10
votes

1
answer

385
views

### Examples of Kreisel-Putnam topological spaces

Let us say that a topological space $X$ is a Kreisel-Putnam space when it satisfies the following property:
For all open sets $V_1, V_2$ and regular open set $W$ of $X$, if a point $x\in X$ has a ...

3
votes

1
answer

241
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 ...

3
votes

1
answer

128
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 ...

27
votes

5
answers

3k
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 ...

11
votes

1
answer

689
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, ...

15
votes

2
answers

1k
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 ...

33
votes

1
answer

745
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 ...

28
votes

5
answers

3k
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 ...

8
votes

2
answers

1k
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. ...

12
votes

1
answer

934
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 ...

12
votes

0
answers

409
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}]$ ...

24
votes

2
answers

1k
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, ...

2
votes

0
answers

389
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 ...

14
votes

2
answers

756
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}$.
...

14
votes

0
answers

476
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 ...

6
votes

1
answer

302
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 ...

10
votes

1
answer

519
views

### Which algebraic theories are co-sites?

Given a category $C$, I'll say that a set $J$ of families $\{f_i\colon A\to B_i\mid i\in I\}\;$ is a co-coverage if their opposites $\{f_i^{op}\colon B_i\to A\mid i\in I\}\;$ form a coverage on $C^{op}...

6
votes

2
answers

167
views

### Stable unions without stable images

A regular category is one with finite limits and pullback-stable images (i.e. (regular epi, mono) factorizations). A coherent category is a regular category that also has pullback-stable finite ...

11
votes

3
answers

882
views

### "Spatial (geometrical)" realization of Elementary topos?

It is well known that (Grothendieck) Topos (in fact, Model topos too) has many good geometrical properties. In many senses reflects general forms of generic geometry.
Note: Grothendieck view of Topos ...

4
votes

0
answers

112
views

### Ref request: modelling regular theories as an injectivity condition

The background to the following observation is standard material in categorical logic, and I thought this was was too — I don’t remember learning it, but I don’t think it is original — but I can’t now ...

25
votes

1
answer

2k
views

### A geometric theory of Blueprints? (Algebras over the field with one element)

In my attempt to tackle the various approaches of defining algebraic geometry over $\mathbb F_1$, I was just reading through Lorscheid's paper The geometry of blueprints. I certainly like the idea a ...

3
votes

0
answers

426
views

### Topos Theory, internal Heyting Algebra

Given a topos $\mathcal{E}$ with subobject classifier $\Omega$.
If we denote by $N\Omega$ the former of all local operators on $\Omega$, that is, Lawvere–Tierney topologies of $\mathcal{E}$, it is ...

11
votes

1
answer

419
views

### Grothendieck toposes in (very) weak foundation

There is on the nLab page "Grothendieck topos" a part about the theory of Grothendieck toposes in weak foundation.
It claims that the equivalence for a category between the Giraud's axioms and being ...

23
votes

1
answer

4k
views

### What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...

8
votes

2
answers

1k
views

### Is there one binary operation foundational for set theory?

The membership relationship "$\in$" is foundational for set theory, in the sense that the axioms of any set theory are formulated in the language of "$\in$". Naturally, the ...