Questions tagged [categorical-logic]
Categorical logic is a study of semantics constructed by categories.
67
questions
1
vote
1
answer
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
...
- 791
1
vote
0
answers
49
views
Free monoidal category out of multicategory
There's a known adjoint pair $Cat \rightarrow MonCat \dashv MonCat \rightarrow Cat$.
See here.
The question is: is there a similar construction $Multicat \rightarrow MonCat \dashv MonCat \rightarrow ...
- 791
0
votes
1
answer
61
views
A subobject is regarded as a proposition - internal logic
a subobject $\ \phi\hookrightarrow A\ $ is regarded as a proposition: by thinking of it as the subcollection of all those things of type $A$ for which the statement $\phi$ is true
First of all I ...
- 791
1
vote
0
answers
68
views
A doctrine is a categorification of a theory
So it says in the nlab page of doctrine.
Let's focus on first order theories for simplicity.
I have two questions, one regarding vertical categorification and another regarding horizontal ...
- 791
5
votes
0
answers
73
views
Images are stable under pullback if and only if covers are
Let's say that an arrow $ f\colon X\to Y $ in a category $ \mathcal C $ have an image if there exists a mono $ \iota\colon \operatorname{Im} f\rightarrowtail Y $ through which $ f $ factors, such that ...
2
votes
1
answer
214
views
What *is* a geometric formula?
In logic (and categorical logic) one learns that infinitary logic is like finitary logic, only that the formulas may contain set-indexed disjunctions and conjuctions such as $\bigvee_{i\in I}\phi_i$. ...
- 3,998
0
votes
1
answer
67
views
Conditions on when a functor $F: Syn_0 \to Set$ arises from a model
In Lecture 4 of Lurie's notes on categorical logic, it is proved when a functor $F: Syn_0(T) \to Set$ arises from a model of the weak syntactic category. I think I can follow most of the argument, up ...
0
votes
0
answers
28
views
What does "full first-order logic" mean?
I see this phrase in the categorical logic literature, but always undefined. What does the "full" mean in "full first-order logic"?
- 303
0
votes
0
answers
49
views
What is a Boolean functor?
According to nlab, a coherent functor is a morphism of coherent categories.
And a Boolean category is a coherent category where subobject posets are always Boolean algebras. Is a Boolean functor a ...
- 303
3
votes
0
answers
92
views
Classifying Topos of a Classical First-order Theory
This nlab page shows a chart describing the structure of the classifying topos of a theory in various logics, but it doesn't have an entry for the classifying topos of a classical first-order theory.
...
- 303
0
votes
1
answer
95
views
is the NNO in a sheaf topos a model of classical PA?
In their book Models for Smooth Infinitesimal Analysis Moerdijk and Reyes claim that the natural number object in any Grothendieck topos is a model of all classical provable statements of first order ...
- 3,998
2
votes
2
answers
128
views
Why is $V(xy)$ the (geometrically correct) union of the two axis (as a scheme)?
Consider $\newcommand{\Spec}{\operatorname{Spec}}V(xy) \subset \Spec \mathbb C[x,y]$ as a closed subscheme. We think of $V(xy)$ as the union of the two axis in $\mathbb A_\mathbb C^2$. But why?
The ...
- 3,998
2
votes
1
answer
79
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 ...
- 1,276
6
votes
1
answer
275
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, ...
- 2,958
4
votes
1
answer
204
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 \...
- 3,998
2
votes
0
answers
106
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 ...
- 1,300
2
votes
0
answers
91
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 ...
- 21
3
votes
0
answers
54
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, ...
- 31
4
votes
1
answer
73
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 ...
- 9,603
2
votes
1
answer
216
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
...
- 135
8
votes
0
answers
215
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,...
- 12.7k
2
votes
0
answers
111
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 ...
- 323
6
votes
0
answers
217
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,...
- 61
6
votes
1
answer
163
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 (...
1
vote
0
answers
31
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 ...
- 549
6
votes
0
answers
134
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 ...
- 129
1
vote
2
answers
123
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
0
answers
64
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 \ [\...
- 549
3
votes
1
answer
175
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://...
- 3,813
1
vote
0
answers
73
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 ...
- 3,813
1
vote
0
answers
110
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 ...
- 3,813
1
vote
1
answer
396
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: ...
- 13
2
votes
0
answers
81
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,205
2
votes
0
answers
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 ...
- 43
5
votes
2
answers
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$ ...
- 2,482
1
vote
1
answer
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,450
1
vote
2
answers
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 ...
- 43.6k
2
votes
0
answers
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 ...
- 173
3
votes
1
answer
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 ...
- 2,061
2
votes
1
answer
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 ...
- 9,603
2
votes
3
answers
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 ...
- 23
2
votes
1
answer
410
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 $\...
- 616
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$) ...
- 11
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 ...
- 3,080
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 ...
- 12.7k
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 ...
- 12.7k
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:
$$
\...
- 452
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 ...
- 1,183
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}(...
- 135
3
votes
0
answers
122
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$ ...
- 17.9k