Questions tagged [categorical-logic]
Categorical logic is a study of semantics constructed by categories.
84
questions
1
vote
1
answer
42
views
Equivalence between equality as a left adjoint and as a right adjoint
Given a hyperdoctrine $P : C^{op} → HA$ it is common to define equality as a left adjoint to contraction
$$ \dfrac{weak(φ) ∧ =_σ ⊢ ψ : P\ (σ × σ)}{φ ⊢ contr(ψ) : P\ σ} $$
Here $$weak := P\ π : P\ \...
- 1,459
1
vote
1
answer
55
views
Explicit definition of cartesian multicategories
In the definition of cartesian multicategories of the nlab it says "symmetric multicategory [equiped with contraction and deletion operations ...] which satisfy certain evident axioms".
In ...
- 1,459
1
vote
0
answers
23
views
Symmetry of cartesian multicategories in first order logic syntax
Cartesian multicategories are symmetric multicategories with a weakening and contraction operations.
When thinking of multicategories as some kind of "algebra" (?) of terms of first order ...
- 1,459
2
votes
0
answers
114
views
About F.Lawvere article "AN ELEMENTARY THEORY OF THE CATEGORY OF SETS"
reference articles:
[L] AN ELEMENTARY THEORY OF THE CATEGORY OF SETS (LONG VERSION) WITH COMMENTARY, F. WILLIAM LAWVERE (http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf)
[T] Topos theory, P....
- 466
0
votes
0
answers
45
views
Categoriсal perspective on the Disjuntion property of the intuitionistic propositional calculus
I came about four different proofs of the disjunction property:
formulated in the language of Heyting algebras;
done using Kripke models;
using the fact that every topological space is an open ...
- 88
1
vote
1
answer
58
views
Morphism between product types as a product of diagonal maps
I am trying to follow this post
https://ncatlab.org/toddtrimble/show/Notes+on+predicate+logic
and I got confused on this paragraph:
From this point of view, a morphism between product types is a ...
- 4,267
1
vote
1
answer
65
views
Models of a slice of coherent category
I am trying to get some sense of the proof of Theorem 10 in this link.
https://www.math.ias.edu/%7Elurie/278xnotes/Lecture6-Completeness.pdf
Immediately after it, Exercise 11 says a model of coherent ...
- 4,267
0
votes
1
answer
51
views
Prove two versions of Godel’s completeness are equivalent
In this notes:
https://www.math.ias.edu/~lurie/278xnotes/Lecture6-Completeness.pdf
Lurie says Theorem 5 implies Theorem 9 by adding constants and an axiom demands that the newly added constants ...
- 4,267
1
vote
0
answers
40
views
Understanding the proof of Giraud's Theorem
I am trying to understand the proof of a lemma of Giraud's Theorem in Lurie's notes on categorical logic:
https://www.math.ias.edu/~lurie/278xnotes/Lecture10-Giraud.pdf
I am confused by the proof of ...
- 4,267
2
votes
1
answer
76
views
Monomorphism to $\{\emptyset.\top\}$ implies equivalence to a sentence
I remember from a discussion the statement:
In the context category (I think of some geometric theory, but I do not think the property of theory matters.)
If $\{\vec{x}. \varphi\}\overset{[\theta]}\to ...
- 4,267
1
vote
2
answers
95
views
Explicit geometric machinery to check the truth of FOL formula
It is standard to use the semantics of topological spaces for checking the truth value of propositional formula in the absence of excluded middle. An explicit description is written down here, for ...
- 4,267
0
votes
1
answer
65
views
How are existential quantifiers present in the internal logic of regular categories?
Intuitively speaking, how do existential quantifiers appear?
I'm just starting to get familiar with these definitions.
Top and conjunctions appear because of finite products. (Plus, I assume, ...
- 1,459
0
votes
1
answer
83
views
Deducing the definition of subobject classifier from Sub functor being representable
As the title says.
Let's consider some category $C$ and the contravariant functor $Sub : C^{op} \rightarrow Set$ that for each object gives its set of subobjects.
The introductory book by Leinster ...
- 1,459
1
vote
0
answers
67
views
Are the "intramural" and "extramural" definitions of "set" from category theory equivalent?
Note: This question takes a pluralistic / "multiverse" view of sets (including "classes" and "collections") and set theories.
My understanding (from reading many nLab ...
- 1,468
1
vote
1
answer
63
views
$Lang$ of a Hyperdoctrine
$$Form \dashv Lang : Hyp \rightarrow FOL$$
We consider an object of $FOL$ to be a signature made of sorts, function symbols and relation symbols, together with a set of axioms of first order logic.
...
- 1,459
2
votes
1
answer
85
views
Definition of structure over first order hyperdoctrine
I'm having trouble understanding this definition.
I use Hyperdoctrine in the sense of Pitts. I know the word hyperdoctrine is very loaded so let me give some definitions before the actual question ...
- 1,459
1
vote
0
answers
50
views
How to define terms categorically before constructing the classifying category (Equational Logic)
I'm reading Pitts' Categorical logic and I'm having a hard time with some basic things.
My goal is to construct the classifying category and give its universal property, but I wanted to understand a ...
- 1,459
2
votes
2
answers
140
views
"Classical" bicartesian closed category?
Every Heyting algebra can be thought of as a bicartesian closed category through which is also a poset.
We may interpret classical logic in a Heyting algebra if we ask of their pseudocomplements to be ...
- 1,459
1
vote
1
answer
72
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,459
1
vote
0
answers
62
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 ...
- 1,459
0
votes
1
answer
80
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 ...
- 1,459
1
vote
0
answers
97
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 ...
- 1,459
5
votes
0
answers
109
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
245
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$. ...
- 4,360
0
votes
1
answer
71
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
33
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"?
3
votes
0
answers
111
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.
...
0
votes
1
answer
118
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 ...
- 4,360
2
votes
2
answers
154
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 ...
- 4,360
2
votes
1
answer
83
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,344
6
votes
1
answer
302
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, ...
- 3,108
4
votes
1
answer
214
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 \...
- 4,360
2
votes
0
answers
108
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,468
2
votes
0
answers
103
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
62
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
78
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,733
2
votes
1
answer
263
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
...
- 257
8
votes
0
answers
243
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,...
- 13.1k
2
votes
0
answers
128
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
262
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
191
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
139
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
2
votes
2
answers
154
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
67
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
189
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://...
- 4,267
1
vote
0
answers
74
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 ...
- 4,267
1
vote
0
answers
114
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 ...
- 4,267
1
vote
1
answer
463
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
91
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,225