Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

Filter by
Sorted by
Tagged with
2
votes
0answers
33 views

Defining truth in a topos model

My colleague and I are working through Goldblatt's Topoi, and we're stuck on exercise 2 in chapter 11, section 4. The exercise is to show that $\|\phi\|^m \circ f = \|\phi\|^m \circ h$, for any ...
5
votes
2answers
115 views

What is a logical formula in the language of categories? How can we express basic model theoretic concepts categorically?

At the beginning of a course in Model Theory, one is introduced to the definition of signature, structure and homomorphism. It is then clear that the class of all structures over a fixed signature $L$ ...
1
vote
1answer
57 views

Syntactic category of a geometric theory has finite limits.

Let $T$ be a geometric theory. Consider the syntactic category $C_T$. I want to show that $C_T$ has all finite limits. To show this, it is enough to show that it has finite products and equalizers. ...
1
vote
1answer
171 views

The legitimacy of topos theory and intuitionism.

This is an exercise in critical thinking. I am not looking, therefore, for opinions on the matter; rather: I would like to know the evidence (whatever that might mean). Background: I have a ...
2
votes
0answers
54 views

Which limit sketches produce Grothendieck toposes?

A limit sketch $\mathcal S=(\mathcal A,L)$ consists of a small category $\mathcal{A}$, together with a set $L$ of cones in $\mathcal A$. A model (in the category of sets) of a limit sketch is a ...
3
votes
1answer
122 views

Logic and adjunctions with ideals in ring theory

Studying ring theory, I remarked two things in the context of ideals that look like some interpretation of a logic in the ideals of a ring (I never studied this subject so my formulation is quite ...
2
votes
1answer
107 views

Sorting out what's true in the generic model in the classifying topos of a theory

I'm interested in trying to understand the generic model in the classifying topos of a particular coherent theory$^1$, and more specifically trying to sort out what non-coherent formulae hold in said ...
2
votes
3answers
88 views

Hyperdoctrines and Contravariance

I've been reading through the extremely useful discussion of First-Order Categorial Logic that recently popped up over at The Diagonal Argument. But when I compare Baez and Weiss's construction to ...
2
votes
1answer
87 views

An $\omega$-categorical theory $T$ with no finite models is complete.

I'm trying to understand the following proof of this result, but I don't understand: where the assumption that $T$ has no finite models is used; why the final step is valid. Take two models $\...
1
vote
0answers
22 views

Basic Constructive Modal Logic and Monoidal Endofunctors

I'm reading this paper by Kakutani : http://nicosia.is.s.u-tokyo.ac.jp/~kakutani/files/aplas07.pdf but I can't see how to use naturality of $m$ (given by the monoidal endofunctor modelling $\Box$) ...
1
vote
1answer
58 views

If a Grothendieck topos has a geometric morphism to $Sets$, then it is unique

In Caramello, Theories, Sites, Toposes, I read that Every Grothendieck topos $\mathcal E$ admits a unique (up to isomorphism) geoemtric morphism $\gamma_{\mathcal E}:\mathcal E\to \bf Set$. The ...
2
votes
1answer
138 views

Universal quantifiers in category theory

I’ve recently learned about the curry howard isomorphism for dependent type theory, and I’m now interested in learning about how to capture this in category theory. I believe that I understand how to ...
0
votes
1answer
63 views

Introduction to categorical logic and CHL-correspondence?

My motivation for this question is that I’m interested in using categorical logic/category theory to intuitively visualize and think about proofs in advanced type-theory based proof-assistants like ...
2
votes
2answers
156 views

Universal properties of universal and existential quantification

In the paper What You Needa Know about Yoneda, Boisseau and Gibbons appeal to the universal properties of universal and existential quantification in order to derive the "co-Yoneda" data type: $$ \...
0
votes
0answers
29 views

How to categorically characterize the structure of all grounded first-order logic formulas?

If the notion of topos corresponds to set theory or first-order logic, then what if one is only interested in grounded logic formulas, ie, formulas that don't contain variables? In a topos one has ...
2
votes
1answer
74 views

What is a presentation of a Lawvere theory formally, and how do you generate the associated Lawvere theory?

A Lawvere theory for a specific algebraic theory is usually given by some sort of presentation. You have generating functions and constants $f_i:A^n \to A$, and relations $(r_1,r_2) \in ``\mathrm{Hom}(...
3
votes
0answers
116 views

Internal equality for Eq-fibrations

In Jacob's Categorical logic and Type Theory in relation to fibrations with equality the author gives the following definition: ...call two morphisms of Eq-fibrations $(K,H),(H',K') \colon p \to q$ ...
3
votes
1answer
77 views

Equivalent algebraic theory with at most binary operations

Given an arbitrary (one-sorted) algebraic/equational theory $\mathbb{T}$, is it possible to devise an equivalent (one-sorted) algebraic theory $\mathbb{S}$ such that the signature of $\mathbb{S}$ ...
2
votes
1answer
64 views

Categoricity of categorical arithmetic

Consider the elementary theory of the category of sets (ETCS). Inside this framework, we have that $(\mathbb N, 0, s)$ is a natural number objet and that : it is a model of the Peano axioms, it is ...
2
votes
1answer
82 views

Graphs in a regular category

Let $\mathcal{C}$ be a regular category, and let $X,Y,Z\in Ob(\mathcal{C})$. Let $g:Z\to Y$ be a regular epi, and let $R\in Sub(X\times Y)$ (subobjects of $X\times Y$). Define $S:=(id_X\times g)^\ast(...
4
votes
1answer
138 views

A simple example in regular categorical logic

I am starting to learn about regular categorical logic as an application of what we learned in class about regular categories. After reading through the definitions of the representation of terms, ...
1
vote
0answers
34 views

In categorical logic, how to correctly formalize sequents whose premise is itself a sequent/implication?

In the literature written in the language of categorical logic, does there exist an example (or even didactic discussion) of the following? Suppose $\Gamma$ is a context, and $P_1(x),P_2(x)$ are ...
2
votes
1answer
101 views

Why are local rings a coherent theory?

It is well known that one way to describe the theory of local rings in first order logic is to add to the algebraic theory of rings two more sequents yielding non triviality and locality: one common ...
2
votes
1answer
260 views

What do you think of this visual category theory tool? See any issues? Would you use it?

The idea behind it is that every category theoretical definition is made with visual diagrams. One reason this is good is that we don't have to do as much language processing which is hard IMO. Here ...
5
votes
2answers
222 views

Can we give a categorical definition of product without using any sub/superscripts or cheating?

For instance changing notation from $C_i$ to $C(i)$ would be considered cheating unless $C$ is a functor from a category $I$. I'm trying to figure out a way to simplify handling category constructs ...
0
votes
1answer
91 views

If logic/type theory/model theory don't depend on set theory

I am at the beginning of trying to understand how to read foundations, but one thing that keeps tripping me up is that, when authors introduce theories that seem like they should proceed or replace ...
0
votes
1answer
98 views

When sheafification functor is open

Let $\mathcal{G}$ be a Grothendiek topos and let $(\mathcal{C},J)$ be a site for $\mathcal{G}$. Is it true that if the sheafification functor $$ \mathcal{G} \leftrightarrows \text{Set}^{\mathcal{C}^...
0
votes
0answers
37 views

Is “points lift along surjections” equivalent to choice in the internal logic?

I'm wondering about the following proposition in the internal logic of a topos: Given an epimorphism $e : E \to B$, then for every points $p : 1 \to B$, there is a point $\tilde{p} : 1 \to E$ for ...
2
votes
1answer
48 views

Models in categorical logic

This is a very basic question: given a theory $\mathbb{T}$, I have seen definitions of models of $\mathbb{T}$ as functions from signature $\Sigma$ to a fixed background category such that it satisfies ...
0
votes
1answer
207 views

ω-categorical theory of an equivalence relation with two infinite equivalence classes

I read on the Wikipedia page that "an equivalence relation with exactly two infinite equivalence classes is an easy example of a theory which is ω-categorical, but not categorical for any larger ...
1
vote
1answer
176 views

Introduction and elimination rules for type-theoretic equalizers/coequalizers/pushforwards/pullbacks

Most presentations of (dependent) constructive type theory present introduction and elimination rules for $0,1,+,\times$, which via Curry-Howard-Lambek corresponds to the initial object, terminal ...
3
votes
1answer
71 views

How to construct a regular functor from a categorical interpretation?

I have read a lecture note by Jaap van Oosten and I am stuck on the exercise 84 in the article. A functor between two regular categories is regular if it preserves finite limits and regular ...
2
votes
1answer
231 views

How to express predicate logic in the categorical (monoidal) logics?

Rosetta stone in the book "New Structures in Physics" (http://www.springer.com/la/book/9783642128202) is the correspondence between the propositional (linear) logic from the one side and the monoidal ...
6
votes
1answer
200 views

Path to categorical realizability theory

I'm trying to understand the sorts of things found on this page: http://ncatlab.org/nlab/show/realizability In particular, I want to read Oosten's Realizability: An Introduction to the Categorical ...
16
votes
2answers
7k 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). ...
6
votes
3answers
827 views

Some reference for categorical logic?

By "categorical logic" I mean category-theoretical models of logic. In particular, I am more interested in models of intuitionistic predicate logic with conjunction, disjunction, implication and ...