Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

Filter by
Sorted by
Tagged with
1
vote
0answers
43 views

categorical logic and computation

After encountering the field of Categorical Logic recently, and more specifically the nLab page on Computational Trilogy as well as this paper, I'm under the impression that we have a pretty complete ...
1
vote
0answers
47 views

Why realizability topos instead of category of assemblies?

A realizability topos is the exact completion of a category of assemblies. If I understood correctly, the major achievement of the completion is having (1) subobject classifier and (2) finite colimits,...
4
votes
1answer
49 views

Why is coherence important in the LCCC interpretation of substitution in dependent type theory?

Reading about the categorical models of dependent type theory (DTT) I have faced many articles pointing out the coherence problem for the interpretation of DTT in locally cartesian closed categories (...
0
votes
0answers
16 views

How does the universal property of the classifying category and generic algebra characterize them up to equivalence and isomorphism respectively?

I have been working through a multi-sorted, categorical presentation of equational logic. Given a collection of equations in context $ Th $, there is a syntactic construction of the "classifying ...
5
votes
0answers
102 views

Universal property of the codomain fibration

Let $\mathcal{C}$ a category with pullbacks. Does $\mathsf{cod}: \mathcal{C}^{\to}\to\mathcal{C}$ have any kind of universal property in the category of (co)fibrations over $\mathcal{C}$? I'd want it ...
1
vote
2answers
29 views

Decidability of bi-cartesian closed categories

This is actually in reference to the question posed here https://stackoverflow.com/posts/66285948/edit but is more appropriate as a question to be posed on a non-coding site. I provide a partial ...
2
votes
0answers
46 views

Which context weakening rules are derivable in this system of equational logic?

I am trying to work through Andrew Pitts' chapter on categorical logic: Categorical Logic. On page 7 he presents a system of equational logic. The rules are listed below: $$\dfrac{}{M = M : \sigma \ [\...
3
votes
1answer
112 views

Strong induction for natural number object

From Lawvere's paper about ETCS we know that we can do induction for natural number object. My aim is to prove the strong induction principle for an NNO in a topos by translating this argument https://...
1
vote
0answers
58 views

Proving the following is a equalizer by proving factorization for $1$ implies factorization for every object

I am reading the following document about Lawvere's ETCS: http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf My question is about Theorem 6 in this document. The aim is to prove an equivalence ...
1
vote
0answers
86 views

Existence of subobject classifier in Lawvere's ETCS

I am reading this document: http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf Compared with the ordinary definition of a topos, the axioms of ETCS do not assume the existence of a subobject ...
1
vote
1answer
130 views

Why is intuitionistic type theory without dependent types more powerful than Martin-Löf type theory?

In the preface of Introduction to higher order categorical logic, Lambek and Scott write (emphasis mine): [L]ogicians have made three attempts to formulate higher order logic, in increasing power: ...
1
vote
0answers
52 views

Counterexample to Frobenius reciprocity in a 1st-order classical hyperdoctrine?

Is there an intuitively-reasonable hyperdoctrine for classical first-order logic that doesn't satisfy the Frobenius condition, eg where $[\exists y. P^*(x) \land Q(x, y)] \ne [P(x) \land \exists y. Q(...
2
votes
0answers
43 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
132 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
70 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
votes
1answer
351 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
68 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
138 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
117 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
110 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
156 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
24 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
1answer
115 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
229 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
91 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
203 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
32 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
82 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
117 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
79 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
85 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
86 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
147 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
38 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 ...
3
votes
1answer
112 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
303 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
226 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
98 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
103 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
38 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
52 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 ...
1
vote
1answer
186 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
78 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
278 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
207 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 ...
19
votes
2answers
8k 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
1k 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 ...