All Questions
12 questions
5
votes
1
answer
415
views
Intuition for the "internal logic" of a cotopos
Let $\mathcal{E}$ be an elementary topos. By definition, $\mathcal{E}$ is a category that has finite limits, is Cartesian closed, and has a subobject classifier $\Omega$. This subobject classifier can ...
- 225
9
votes
1
answer
511
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{\...
- 21.3k
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. ...
- 1,720
26
votes
2
answers
2k
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, ...
user71137
2
votes
0
answers
392
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 ...
- 9,111
15
votes
0
answers
586
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 ...
- 171
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 ...
- 15.9k
36
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, ...
- 66.8k
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 ...
- 2,083
36
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 ...
- 8,659
29
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 ...
- 25.6k
14
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 ...
- 1,539