2
$\begingroup$

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 frame propositional logic in category theory: Every proposition is an object, and a proof of a proposition is a morphism from $T$ to that object, and we assume the category is cartesian closed. $A$ implies $B$ is assumed as an axiom by positing a morphism from $T$ to the exponential object $B^A$. A conjunction between $A$ and $B$ is true if there is a morphism from $T$ to $A\times B$, and to the coproduct for a disjunction. A negation of a proposition $A$ is represented by a morphism from $A$ to type “bottom” which is uninhabited.

But I’m not sure how to represent universal quantifiers and existential quantifiers, and I couldn’t really understand the texts I found online.

$\endgroup$
3
$\begingroup$

Assuming you are interested only in the Curry-Howard-Lambek type of interpretations of logic in categories then in order to interpret first-order logic in a category cartesian closed categories are not sufficient.

The problem lies in the fact that you need a category whose objects represents not only propositions, i.e. closed formulas, but predicates as well (i.e. formulas with vatiables).

In order to do this one needs some sort of fibered categories (or indexed ones if you prefer).

We assume we have a logic signature made of an algebraic signature $\Sigma$, containing the operation symbols, and predicate signature $\Pi$, containing the predicate symbols.

For start one consider the category $T(\Sigma)$ whose objects sets of free variables and for every pair of such sets $X$ and $Y$ we have $$T(\Sigma)[X,Y]=\mathbf{Set}[X,T_\Sigma(Y)]$$ where $T_\Sigma(Y)$ is the set of terms with variables in $Y$. So morphisms of this category are substitutions for the logic signature considered.

To each $X \in T(\Sigma)$ we can associate the poset $P(X)$ of formulas with free variables in $X$, with order relations given by $\varphi \leq \psi$ iff $\varphi \vdash \psi$.

Also for every morphism/substitution $\sigma \in T(\Sigma)[X,Y]$ we have a monotone map $$P(\sigma)\colon P(X) \to P(Y)$$ defined as $P(\sigma)(\varphi)=\sigma(\varphi)$, that is the formula obtained by applying the substitution $\sigma$ to the formula $\varphi$.

These assignment define a functor $P\colon T(\Sigma) \to \mathbf{Cat}$, where we regard posets as categories and monotone functions as functors.

In this set up we can characterize quatifiers as adjoint functors, let see how.

For every $X$ set of variables and a new variable $x$ we have a morphisms $\pi_x^X \in T(\Sigma)[X,X\cup\{x\}]$ given by the substitution $$\pi_x^X \colon X \longrightarrow X\cup\{x\}$$ $$\pi_x^X(x)=x$$ for every $x \in X$.

The induced functor/monotone map $P(\pi_x^X)$ sends every proposition of $P(X)$ into itself seen as a member of $P(X\cup\{x\})$.

A left adjoint to $P(\pi_x^X)$ would be a functor $L_x^X \colon P(X \cup\{x\}) \to P(X)$, that takes formulas with free variables in $X\cup\{x\}$ and sends them in formulas with free variables in $X$ (pretty much as the quantifiers that eliminate free variables).

For $L_x^X$ to be an adjoint we need to have a natural isomorphism $$P(X)[L_x^X(\varphi),\psi]\cong P(X\cup\{x\})[\varphi,P(\pi_x^X)(\psi)]$$ and since we are dealing with posets this amounts to require that $$L_x^X(\varphi) \leq \psi \iff \varphi \leq P(\pi_x^X)(\psi)=\psi$$

This is equivalent to require that $L_x^X(\varphi)$ is a proposition whose logical consequences $\psi$ with free variables in $X$ are exactly those formulas that are implied by $\varphi$ in the extended context of $P(X\cup\{x\})$.

With a little effort one can show that such $L_x^X(\varphi)$ must be $\exists x \varphi$.

Similarily a right adjoing $R_x^X \colon P(X\cup\{x\}) \to P(X)$ would be a functor such that there is a natural isomorphism $$P(X\cup\{x\})[P(\pi_x^X)(\varphi),\psi]\cong P(X)[\varphi,R_x^X(\psi)]$$ Again, since we are dealing with posets, this amounts to require that $R_x^X(\psi)$ is the formula such that $\varphi \leq R_x^X(\psi)$ iff and only if $\varphi \leq \psi$, that is $R_x^X(\psi)$ is a logical consequence of $\varphi$ if and only if $\psi$ is a logical consequence of $\varphi$.

By playing a little bit with logic one can show that the only possibility is for $R_x^X(\psi)$ to be $\forall x \psi$.

If you are interested to some pointers I suggest to read Bart Jacobs' "Categorical Type Theory" that deals in details with these subject.

Note: usually authors use a different notation form the one I used here, for instance they usually deal with the category $T(\Sigma)$, nevertheless if you got the general idea I think you can easily fix the difference in notations.

I hope I was able to give you the raw idea, in case you needed any additional clarification please ask.

$\endgroup$
  • $\begingroup$ What is the “substitution functor”, and between which categories is it ? (I don’t know how to parse “between the categories indexed by $X$ and $Y$”, or what the functor would be). 2. A substitution is a function from variables to formulas. But in your example where you add a variable to $X$, it is a function from variables to another set of variables. This confuses me. 3. Could you give an intuition why the existential and universal quantifiers are adjoints of this functor, and what we can do with this fact? (Though as I said before, I don’t understand how the functor is constructed.) $\endgroup$ – user56834 Jun 30 at 21:17
  • $\begingroup$ @user56834 I've edited the answer adding as much details as I could. Let me know if these changes address all your doubts. $\endgroup$ – Giorgio Mossa Jul 2 at 11:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.