3
votes
2answers
78 views

What's the difference between a logic, an internal logic (language) of a category, an internal logic of a topos and a type theory?

maybe this question doesn't make sense at all. I don't know exactly the meaning of all these concepts, except the internal language of a topos (and searching on the literature is not helping at all). ...
1
vote
1answer
86 views

Arrows-only implication & disjunction in $\mathbf{Set}.$

Just before the truth-arrows in a topos subsection of Goldblatt's "Topoi: A Categorial Analysis of logic," descriptions of the truth functions $\Rightarrow$ and $\smallsmile$ are given in ...
7
votes
2answers
119 views

The dense topology

The definition of the dense topology confuses me. If $C$ is a category and $X \in C$, a sieve $S$ on $X$ is a covering for the dense topology iff for every $f : Y \to X$ there is some morphism $g : Z ...
5
votes
2answers
184 views

What is the relation between axiomatic set theory and logical quantifiers?

On the one hand, the logical predicates $\forall$ and $\exists$ are defined using the concept of a Domain of Discourse, which itself is defined as a set (at least according to wikipedia). On the ...
9
votes
1answer
115 views

Properties of the internal language of the category of sheaves.

Consider a simple case of sheaves on some topological space $X$, $\operatorname{Sh}(X)$ (recall that a sieve on $U$ is covering iff its $\operatorname{sup}$ is $U$). All of these are Grothendieck ...
7
votes
1answer
148 views

Is there any point in a logician studying $\infty$-categories?

My primary areas of interest lately have been set theory, logic, and category theory, so naturally topos theory has been a large part of what I'm learning (in between getting caught up on some other ...
2
votes
1answer
37 views

Question about Lemma D1.4.4(iii) in the Elephant - possible typo?

Given a morphism $[\theta] \colon \lbrace \bar{x}.\phi \rbrace \rightarrow \lbrace \bar{y}. \psi \rbrace$ in the syntactic category $\mathcal{C}_{\mathbb{T}}$ of a (cartesian) theory, we are told, in ...
10
votes
3answers
267 views

Is there a category whose internal logic is paraconsistent?

The internal language of topoi is higher-order typed intuitionistic logic. Now according to wikipedia, the dual of intuitionistic logic, in some sense is paraconsistent. They say Intuitionistic ...
1
vote
2answers
85 views

Do 'nice' first order logics have universal models?

A first-order logic is interpreted in a model where sentences of the logic can be said to be true or false. There may be more than one model, and we can identify morphisms between models. Do we have ...
4
votes
1answer
122 views

Is the internal language of a topos complete, sound and effective?

The internal language of a topos is higher order intuitionistic typed logic. Now according to this article in wikipedia higher order classical logic with full semantics is never complete, sound or ...
14
votes
4answers
354 views

What does a proof in an internal logic actually look like?

The nLab has a lot of nice things to say about how you can use the internal logic of various kinds of categories to prove interesting statements using more or less ordinary mathematical reasoning. ...
0
votes
1answer
56 views

Is this thing K-finite?

This is related to this question: Freyd's Geometric Finiteness : An Example Computation I've essentially reduced the problem to the following question: Equip $\mathbb{N}$ with the discrete ...
4
votes
1answer
412 views

Logic and geometry

By delving into topos theory and sheaves one will eventually discover a "deep connection" between logic and geometry, two fields, which are superficially rather unrelated. But what if I have not the ...
7
votes
3answers
217 views

Does the category framework permit new logics?

It appears to me that a topos permits a broader concept of subsets than the yes/no decission of a characteristic function in a set theory setting. Probably because the subobject classifier doesn't ...
3
votes
1answer
99 views

Locating a copy of a thesis

Does anyone have a transmittable copy of the thesis "Logical and cohomological aspects of the space of points of a topos" by Carsten Butz? The link provided in ...
6
votes
1answer
320 views

What do coherent topoi have to do with completeness?

There is a theorem of Deligne 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 geometric ...
5
votes
2answers
231 views

Where is the well-pointedness assumption of ETCS used in everyday math?

Where is the well-pointedeness assumption of the Elementary theory of the category of sets (Lawvere's category-theoretic axiomatization of set theory) used in everyday math? Specifically, if you have ...