Questions tagged [categorical-logic]
The categorical-logic tag has no usage guidance.
67
questions
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, ...
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 ...
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, ...
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 ...
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 ...
33
votes
1
answer
743
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 ...
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.
...
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, ...
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 ...
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 ...
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 ...
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 ...
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, ...
24
votes
1
answer
1k
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 ...
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 ...
20
votes
4
answers
4k
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 ...
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 ...
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 ...
14
votes
0
answers
339
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 ...
14
votes
0
answers
475
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 ...
13
votes
4
answers
6k
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 ...
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".
...
13
votes
2
answers
749
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}$.
...
13
votes
1
answer
543
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 ...
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 ...
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 ...
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$)...
12
votes
0
answers
406
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}]$ ...
11
votes
3
answers
879
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 ...
11
votes
2
answers
376
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 ...
11
votes
1
answer
418
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.
...
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, ...
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 ...
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}...
10
votes
2
answers
772
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 ...
10
votes
1
answer
383
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 ...
10
votes
0
answers
384
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 ...
10
votes
0
answers
372
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
431
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{\...
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 ...
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. ...
7
votes
1
answer
406
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 ...
6
votes
3
answers
287
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 ...
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^*...
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 ...
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 ...
6
votes
1
answer
282
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 ...
6
votes
0
answers
157
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
2
answers
491
views
Proof by contradiction in a topos
In a topos which is not Boolean topos, can we use proof by contradiction?
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 ...