Questions tagged [categorical-logic]

Categorical logic is a study of semantics constructed by categories.

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

Is there a decent notion of "double Lawvere theory?"

I've been playing with the idea of a "double Lawvere theory" for mechanizing first order logical theories. I've been able to find only a tiny amount of detail online though and want feedback ...
user avatar
6 votes
0 answers
121 views

Linear logic and linearly distributive categories

1. Context On page two of the introduction to their paper Weakly distributive categories on linearly distributive categories Cockett and Seely write: It turns out that these weak distributivity maps, ...
user avatar
  • 1,707
3 votes
1 answer
148 views

Mistake in B. Jacobs book Categorical Logic and Type Theory?

Lemma 1.8.9 in B. Jacobs book Categorical Logic and Type Theory describes how a collection of fibre-wise adjoints of a morphism of fibrations can be promoted to a global adjoint. Let $p: \mathbb E \...
user avatar
  • 1,368
2 votes
0 answers
75 views

Name of functor from "Propositions"/"Properties" to "Power set" implied (in part?) by axiom schema of specification?

$\newcommand{\Inj}{\operatorname{Inj}}$$\newcommand{\Prop}{\operatorname{Prop}}$Consider the "category of propositions" or "of properties" $\Prop$, where objects are logical ...
user avatar
2 votes
0 answers
53 views

Models of pretoposes vs. models of coherent categories

I'm confused about these lecture notes. Theorem 4 states, roughly, that for each coherent category $C$ there is a pretopos $C^\mathrm{eq}$ such that for any pretopos $D$, morphisms of coherent ...
user avatar
3 votes
0 answers
38 views

Does the forgetful functor from the category of models of a cartesian theory preserve and create limits?

It is well-known that a monadic functor preserves and creates limits, which in particular shows that any algebraic category, or equivalently, any category of models of an algebraic theory, has limits, ...
user avatar
4 votes
1 answer
61 views

Categories of presheaves with topologies stronger than $\neg\neg$-topology

In any topos, the Lawvere-Tierney topology given by $\neg\neg:\Omega\to\Omega$ is the strongest for which the morphism $0\to 1$ is closed. In most of the examples I am familiar with (admittedly, these ...
user avatar
1 vote
1 answer
114 views

Intuition for Exists and Forall functors

This question gives a concise definition of the exists and forall functors, in the form invented (I gather) by Lawvere. Quoting: Let $f:X\rightarrow Y$ be an arrow in $\mathsf{Set}$. $f$ induces ...
user avatar
  • 91
7 votes
0 answers
148 views

Precise statement of the syntactic category of a logic/type theory, in maximum generality?

I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article,...
user avatar
  • 11.9k
1 vote
0 answers
59 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 ...
user avatar
2 votes
0 answers
96 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,...
user avatar
  • 21
4 votes
1 answer
71 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 (...
user avatar
1 vote
0 answers
22 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 ...
user avatar
  • 519
5 votes
0 answers
114 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 ...
user avatar
  • 119
1 vote
2 answers
53 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 ...
user avatar
2 votes
0 answers
55 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 \ [\...
user avatar
  • 519
3 votes
1 answer
143 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://...
user avatar
  • 3,707
1 vote
0 answers
67 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 ...
user avatar
  • 3,707
1 vote
0 answers
93 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 ...
user avatar
  • 3,707
1 vote
1 answer
218 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: ...
user avatar
2 votes
0 answers
64 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(...
user avatar
  • 2,095
2 votes
0 answers
49 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 ...
user avatar
5 votes
2 answers
137 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$ ...
user avatar
1 vote
1 answer
79 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. ...
user avatar
-1 votes
2 answers
596 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 ...
user avatar
  • 38k
2 votes
0 answers
77 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 ...
user avatar
3 votes
1 answer
167 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 ...
user avatar
  • 1,864
2 votes
1 answer
125 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 ...
user avatar
2 votes
3 answers
124 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 ...
user avatar
  • 23
2 votes
1 answer
262 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 $\...
user avatar
1 vote
0 answers
25 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$) ...
user avatar
2 votes
1 answer
149 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 ...
user avatar
  • 2,950
2 votes
1 answer
281 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 ...
user avatar
  • 11.9k
0 votes
1 answer
122 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 ...
user avatar
  • 11.9k
2 votes
2 answers
247 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: $$ \...
user avatar
0 votes
0 answers
34 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 ...
user avatar
  • 1,063
2 votes
1 answer
94 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}(...
user avatar
3 votes
0 answers
119 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$ ...
user avatar
3 votes
1 answer
85 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}$ ...
user avatar
  • 1,479
2 votes
1 answer
91 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 ...
user avatar
  • 307
2 votes
1 answer
87 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(...
user avatar
  • 1,818
4 votes
1 answer
155 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, ...
user avatar
  • 2,406
3 votes
1 answer
118 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 ...
user avatar
2 votes
1 answer
348 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 ...
user avatar
5 votes
2 answers
229 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 ...
user avatar
0 votes
1 answer
113 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 ...
user avatar
  • 1,165
0 votes
1 answer
105 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}^...
user avatar
0 votes
0 answers
40 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 ...
user avatar
  • 1,450
2 votes
1 answer
57 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 ...
user avatar
1 vote
1 answer
205 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 ...
user avatar