Questions tagged [categorical-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
35 votes
3 answers
2k 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, ...
Mike Shulman's user avatar
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 ...
Peter LeFanu Lumsdaine's user avatar
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 ...
Michael Bächtold's user avatar
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 ...
Ioachim Drugus's user avatar
50 votes
5 answers
19k views

Categorical foundations without set theory

Can there be a foundations of mathematics using only category theory, i.e. no set theory? More precisely, the definition of a category is a class/set of objects and a class/set of arrows, satisfying ...
user avatar
34 votes
3 answers
3k 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 ...
David Corfield's user avatar
54 votes
2 answers
9k 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, ...
David Spivak's user avatar
  • 8,549
34 votes
2 answers
3k 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 ...
David Spivak's user avatar
  • 8,549
32 votes
3 answers
7k views

Category of categories as a foundation of mathematics

In Lawvere, F. W., 1966, “The Category of Categories as a Foundation for Mathematics”, Proceedings of the Conference on Categorical Algebra, La Jolla, New York: Springer-Verlag, 1–21. ...
Marc Nieper-Wißkirchen's user avatar
28 votes
2 answers
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 ...
Akhil Mathew's user avatar
  • 25.3k
14 votes
1 answer
1k 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 ...
Zhen Lin's user avatar
  • 14.9k
12 votes
0 answers
407 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}]$ ...
Ingo Blechschmidt's user avatar
12 votes
1 answer
930 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 ...
Ivan Di Liberti's user avatar
12 votes
0 answers
238 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$)...
Gro-Tsen's user avatar
  • 29.9k
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, ...
FWE's user avatar
  • 213
6 votes
2 answers
309 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^*...
Mendieta's user avatar
  • 249
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 ...
user478652's user avatar
3 votes
1 answer
149 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$...
Mendieta's user avatar
  • 249