# Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

67 questions
Filter by
Sorted by
Tagged with
1 vote
59 views

### "Axioms are the containments in $C$."

On the nlab page for internal logic it says The Internal Logic as a Functor As described above, a model of a given theory $T$ in a category $C$ consists of an assignment \begin{array}{|c|c|c|} \hline ...
1 vote
49 views

106 views

54 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 ...
155 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
103 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
885 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 ...
96 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 ...
205 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 ...
138 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 ...
168 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 ...
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 0 answers 27 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$) ... 2 votes 1 answer 235 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 1 answer 425 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 1 answer 181 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 ... 3 votes 2 answers 355 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 0 answers 36 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 1 answer 134 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}(...
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$ ...