All Questions
Tagged with categorical-logic topos-theory
35 questions
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
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
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
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 ...
- 2,303
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
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
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
14
votes
2
answers
802
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
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
13
votes
4
answers
2k
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".
...
- 558
13
votes
1
answer
1k
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 ...
- 9,111
12
votes
1
answer
439
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 ...
- 42.4k
12
votes
0
answers
432
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}]$ ...
- 3,312
11
votes
3
answers
940
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 ...
- 1,720
11
votes
2
answers
405
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 ...
- 714
11
votes
1
answer
461
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.
...
- 113
11
votes
0
answers
411
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 ...
- 407
10
votes
1
answer
526
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}...
- 8,659
10
votes
1
answer
234
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 ...
- 101
10
votes
0
answers
391
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 ...
- 613
9
votes
1
answer
2k
views
What does the topos of (light) condensed sets classify?
Recall that $\mathrm{Pro}(\mathbf{FinSet}) = *_{\text{proét}}$, the category of profinite sets, forms a site with finite jointly surjective families as covers, and that the category of sheaves on this ...
- 1,094
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
6
votes
3
answers
291
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 ...
- 619
6
votes
2
answers
314
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^*...
- 401
6
votes
2
answers
171
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 ...
- 66.8k
6
votes
1
answer
307
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 ...
- 913
5
votes
2
answers
503
views
Proof by contradiction in a topos
In a topos which is not Boolean topos, can we use proof by contradiction?
- 105
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
4
votes
0
answers
269
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 ...
- 9,111
3
votes
1
answer
165
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$...
- 401
3
votes
0
answers
454
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 ...
- 159
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
2
votes
0
answers
129
views
Sheaves, colimits and closure
I am considering the sheaf topos $\mathbf{Sh}(\mathfrak{X})$ on a topological space $\mathfrak{X}$.
Limits in this category are constructed pointwise, as in presheaves. Colimits, however, are not ...
- 408