Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

2
votes
1answer
22 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
21 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$) ...
0
votes
0answers
40 views

Odds Ratios with independent linear trends

I have a question regarding odds ratios for a project I'm working on. For my analysis to determine if there was a significant change in access to a service at a certain type of facility from one year ...
1
vote
1answer
48 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
60 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
40 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 ...
1
vote
2answers
107 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
28 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
58 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
99 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
66 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
51 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
72 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(...
3
votes
0answers
80 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
31 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
92 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
171 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
212 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
65 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
88 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
34 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
161 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
140 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
62 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
164 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
189 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 ...
15
votes
2answers
5k 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). ...
5
votes
3answers
634 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 ...