4
votes
2answers
103 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). ...
0
votes
0answers
72 views

Relation between existential and universal quantificator in category theory

Let $\mathscr C$ be a cartesian (i.e. with finite limits) category with subobject classifier $\Omega$ and generic subobject $\tau:I\to\Omega$ (here $I$ denote the terminal object). Let $f:X\to Y$ and ...
3
votes
1answer
77 views

Relations between Theories and Categories

I'm just toying around with some thoughts, trying to grock some concepts: It seems that every formal theory induces a locally small category via interpretations: its objects are structures that ...
5
votes
1answer
93 views

Is there a formal way to describe classical logic as a reflective subcategory of constructive logic?

Working informally, we can take any proof $P$ in constructive (or intuitionistic) logic and turn it into a classical proof $cP$ by 'copying' it, since all the rules of constructive logic reappear in ...
2
votes
1answer
36 views

Is there a phrase to describe those objects of $\mathbf{C}$ that can be expressed as quotients of the algebra freely generated by $X$?

Let $\mathbf{C}$ denote the category of models of an algebraic theory in $\mathbf{Set}.$ Now suppose $X$ is an object of $\mathbf{Set}$. Is there a traditional phrase used to describe those objects of ...
4
votes
3answers
199 views

Simplifying a categorical proof of constructive dilemma

In axiomatic propositional calculus the following axiom schema captures constructive dilemma: $\newcommand{\lif}{\supset} \renewcommand{\land}{\&}$ \begin{equation} (a \lif c) \lif ((b \lif c) ...
1
vote
1answer
87 views

Arrows-only implication & disjunction in $\mathbf{Set}.$

Just before the truth-arrows in a topos subsection of Goldblatt's "Topoi: A Categorial Analysis of logic," descriptions of the truth functions $\Rightarrow$ and $\smallsmile$ are given in ...
1
vote
1answer
104 views

Is there any relevance between Boolean Algebras and Fields?

In some sense Boolean Algebras and Fields have same operators and constants. In both structures there are operators addition ($+$ , $\vee$), multiplication ($\times$ , $\wedge$), inverse with respect ...
7
votes
2answers
122 views

The dense topology

The definition of the dense topology confuses me. If $C$ is a category and $X \in C$, a sieve $S$ on $X$ is a covering for the dense topology iff for every $f : Y \to X$ there is some morphism $g : Z ...
5
votes
0answers
96 views

Functorial first order theories interpretation

Question will be a bit naive, so please, be kind. Consider first order theories, $\Gamma, \Gamma'$ . Let $\mathcal{M}$ be the category of models for $\Gamma$ and $\mathcal{M}'$ be the category of ...
5
votes
2answers
94 views

Is there a logical interpretation for equalizer and co-equalizer?

I know the logical equivalent to several universal constructions. For example product $\times$ is $\land$ and co-product $+$ is $\lor$. The associated arrows are projection and inclusion. The ...
3
votes
0answers
52 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
1
vote
1answer
61 views

Do the circle groups have any interesting stand-alone descriptions?

By the circle groups, I mean firstly the circle group $\mathbb{T} \subseteq \mathbb{C}$ of all complex numbers having modulus $1$, and secondly the commutative group $\mathbb{S} = \mathbb{T} \cap ...
1
vote
1answer
90 views

Is there a first order theory for equivalences classes?

Question will be a bit naive, so please, be kind. Consider a first order theory, $\Gamma$ . Let $\mathcal{M}$ be the category of models for $\Gamma$. Consider $\sim$ an equivalence relation on ...
1
vote
1answer
34 views

Resources for Polyadic and/or Cylindric Algebra

I'm looking to learn a little bit about polyadic and cylindric algebras, as part of an investigation into algebraic approaches to logic. The only "text" that I can find for polyadic algebra is ...
0
votes
1answer
50 views

How to inverse this logic definition of separator of Set category?

Lawvere's Sets for Mathematics defines a separator object $S$ for morphisms $f_1, f_2: X \rightarrow Y$ of the Set category as a logic statement $s$ $s$: $\forall x \left[ S \xrightarrow{x} X ...
3
votes
3answers
135 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 ...
5
votes
2answers
512 views

Is maths = set theory + logic? [closed]

It seems to me that most branches of mathematics are just an application of set theory and the rules of logic. You just definite particular types of sets and study their properties. For example, in ...
4
votes
1answer
104 views

What do identities mean in $\mathrm{Set}^\mathrm{op}$?

Since $\mathrm{Set}$ has finite coproducts, thus we may consider models of equational theories in the opposite category $\mathrm{Set}^\mathrm{op}$. The result is basically that function symbols $f : ...
2
votes
1answer
59 views

Algebraic signatures as quivers; is there somewhere I can learn more about these definitions?

In my opinion, a cool definition of "algebraic signature" is as follows: An algebraic signature on the sort symbols $\mathcal{X} = \{X_0,...,X_{n-1}\}$ is precisely a quiver whose underlying set ...
7
votes
1answer
181 views

What is the dual of implication?

You may divide Intuitionistic Propositional Logic into the negative and positive fragments. The negative fragment includes truth, conjunction, and implication while the positive fragment includes ...
6
votes
1answer
192 views

Can we capture all domains of discouse in the predicate logic within categorical logic?

In the construction of the bounded quantifiers via adjoints in the fibered category of subsets over a set (see e.g. here on Wikipedia), is there any restriction on the sets - specifically regarding ...
4
votes
1answer
107 views

Advice regarding best-practice mathematics / categorial logic.

A good heuristic is: If it doesn't cost anything, generalize. In particular, if we have a theorem, and a proof thereof, then we ought to look for a maximal generalization of this theorem, ...
0
votes
2answers
95 views

The Adjunction $\_\times A\dashv (\_ )^A$ for Preorders: The Deduction Theorem.

The following is from Turi's Category Theory Lecture Notes. Definition 11.11 Let $A$ be an object of a category $\mathbb{C}$ with binary products. The right adjoint of $\_\times ...
2
votes
1answer
174 views

lambda calculus and category theory

I am not particularly knowledgeable in either lambda calculus or category theory, but I am starting to learn Haskell so I would like to ask: are there connections between category theory and lambda ...
5
votes
1answer
202 views

Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are: Set theory; Logic; Category theory; Type ...
7
votes
1answer
151 views

Is there any point in a logician studying $\infty$-categories?

My primary areas of interest lately have been set theory, logic, and category theory, so naturally topos theory has been a large part of what I'm learning (in between getting caught up on some other ...
3
votes
1answer
118 views

Is the empty function always a bijection?

Let $f_A:\emptyset\to A$ be the empty function with range $A$. The definition of a bijection as applied to this function is: $$\forall x,y \in \emptyset (x=y \implies f_A(x)=f_A(y))$$ negating you ...
2
votes
1answer
38 views

Question about Lemma D1.4.4(iii) in the Elephant - possible typo?

Given a morphism $[\theta] \colon \lbrace \bar{x}.\phi \rbrace \rightarrow \lbrace \bar{y}. \psi \rbrace$ in the syntactic category $\mathcal{C}_{\mathbb{T}}$ of a (cartesian) theory, we are told, in ...
8
votes
1answer
191 views

Can we found mathematics without evaluation or membership?

In some sense, composition generalizes evaluation. The trick is, instead of writing $f(x)$ for $x$ an element of the domain of $X,$ we write $f \circ x$ for $x$ a function $1 \rightarrow X$. ...
3
votes
2answers
95 views

How can I quantify over the class of all cardinalities?

I'd like to quantify over all cardinalities of sets. My end goal is to make a category-theoretic arguement: For all cardinalities of sets, in the category of sets with maps as morphisms: the ...
5
votes
1answer
151 views

Can logic be significantly geometrised?

I've already asked this question on philosophy.stackexchange, I'm hoping for a different answer here: Descarte has been lauded for putting together geometry and algebra, and his achievement allowed ...
6
votes
1answer
85 views

name of the unit of adjunction between $-\times C$ and $\cdot^C$

Answers to a earlier question about the categorical interpretation of first-order quantification led me to learn more about adjoints. Now, I understand that a category $\mathscr{C}$ with products has ...
6
votes
1answer
168 views

Is it possible to formalize a “universe” of categories as a one-sorted first-order theory with one binary relation and no functions?

This is a modification of a question I asked earlier. In that question, I hadn't placed any limits on the number of binary relations allowed, so my question had an affirmative answer, but a trivial ...
10
votes
3answers
283 views

Is there a category whose internal logic is paraconsistent?

The internal language of topoi is higher-order typed intuitionistic logic. Now according to wikipedia, the dual of intuitionistic logic, in some sense is paraconsistent. They say Intuitionistic ...
6
votes
1answer
220 views

Is it possible to formalize (higher) category theory as a one-sorted theory, just like we did with set theory?

Set theory is typically formalized as a one-sorted theory without urelements. Is it possible to do the same with category theory or higher category theory, formalizing the whole affair as a theory ...
8
votes
5answers
337 views

categorical interpretation of quantification

Many constructions in intuitionistic and classical logic have relatively simple counterparts in category theory. For instance, conjunctions, disjunctions, and conditionals have analogues in products, ...
4
votes
1answer
195 views

Are there dual logic gates?

In category theory the usefulness of dualising such devices as monoids to comonoids has been shown, where multiplication which takes two inputs to one output is dualised to comultiplication which ...
5
votes
1answer
224 views

Quantifiers as Adjoints in Generalized Logics

It is a well known fact that the classical universal and existential quantifiers can be seen as adjoints in certain categories. In the continuous model theory of metric structures (see ...
9
votes
4answers
327 views

What precisely is lost when considering proper classes rather than sets?

Motivated by concerns over the foundational issues vis-a-vis category theory. What is the essential useful characteristic of sets that is lost when instead considering proper classes? Referring to ...
2
votes
1answer
193 views

Modern reference on logic-set theory-foundation

I'm looking for a modern book on logic-set theory-foundation written as the Bourbaki's set theory. I'm particularly interested in a formal exposition of ZFC axiom with logic-set Grothendieck universe. ...
1
vote
0answers
63 views

Functors that have a natural Isomorphism

Find different functors $T, S: Rng \rightarrow Rng$ both identity on objects IE: for each ring $R, T(R)=S(R)=R$, such that there is a natural isomorphism between T and S. I know that a natural ...
4
votes
1answer
124 views

Is the internal language of a topos complete, sound and effective?

The internal language of a topos is higher order intuitionistic typed logic. Now according to this article in wikipedia higher order classical logic with full semantics is never complete, sound or ...
4
votes
2answers
149 views

Is higher order type theory the same as higher order logic?

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types. In mathematical logic we have higher-order ...
14
votes
4answers
389 views

What does a proof in an internal logic actually look like?

The nLab has a lot of nice things to say about how you can use the internal logic of various kinds of categories to prove interesting statements using more or less ordinary mathematical reasoning. ...
6
votes
2answers
130 views

Axiom of Choice-esque argument to show that a proof of a statement exists without actually giving a proof

What if the set of all well-formed statements in ZFC formed a kind of pseudo-category where a morphism f between objects A, B represented a formal proof that A implied B? What if that category could ...
6
votes
1answer
242 views

distribution of categorical product (conjunction) over coproduct (disjunction)

In the classical and intuitionistic propositional calculi, it is straightforward, using natural deduction, to derive $((A \land C) \lor (B \land C))$ from $(A \lor B) \land C$: Assume $(A \lor B) ...
2
votes
3answers
210 views

Beyond Goedel incompleteness and lack of soundness/completeness of higher-order logics

As I understand that there are at least two fundamental limits of the development of the mathematics: 1) Goedel incompeleteness theorems (or more clearly Church thesis) effectively says that there ...
4
votes
1answer
89 views

Recovering an object from its category

Consider the category of groups (but the question arises for any category of mathematical object, basically). It is easy to read off what the automorphism group of a group is or what its cardinality ...
3
votes
1answer
93 views

What is the (propositional) logic associated with an orthomodular lattice?

In Quantum Mechanics the space of projections on the associated Hilbert Space of States forms an Orthomodular Lattice. Von Neumann calls this a Quantum Logic. When projections commute they generate a ...