13
$\begingroup$

I am a bit confused about the interpretation of "implication" in the standard treatment of categorical logic, for example in [Bart Jacobs 1999] "Categorical Logic and Type Theory".

(A). On the one hand, the book says that "terms give rise to morphisms between contexts, this is the canonical way to produce a category from types" (p.5) Under this interpretation, type contexts are the objects in the category, also called indices, such that fibers can be built over indices. Under the Curry-Howard isomorphism, this arrow would correspond to an implication $\Rightarrow$ in logic.

(B). On the other hand, "each fiber category $P(I)$ is a Boolean algebra... with propositional connectives such as $\wedge, \vee, \top, \bot, \neg$ in (Boolean) logic" (p.12, ibid). This seems to be the approach used by Lawvere when he formulated the notion of topos, with the sub-object classifier $\Omega$. Under this interpretation, one can also create the (Boolean) logic implication operator $A \Rightarrow B$ defined as $\neg A \vee B$ (in Boolean algebra, but one can also do similarly in Heyting algebra). Would this $\Rightarrow$ be in conflict with the $\Rightarrow$ in (A)?

Edit: More specifically, if there is an arrow $A \Rightarrow B$ in the fiber, as in (B), how does it correspond (via Curry-Howard) to some type or term in the base category?

$\endgroup$

4 Answers 4

23
$\begingroup$

There are two concepts here, which are tightly connected. Logically, this corresponds to the distinction between $\vdash$ and $\Rightarrow$.

(A) Morphisms $t : \Gamma \to A$ represent (well-formed, typed) terms $\Gamma \vdash t : A$ in a context. If there is a single type (such as in universal algebra), we may write this simply as $\Gamma \vdash t$. This represents entailment, or derivability, of $t$ in the context $\Gamma$.

(B) Objects $A \Rightarrow B$ (which is the exponential $B^A$) represent implication. This may be thought of as an internalisation of the notion of entailment: in fact, terms $\vdash f : A \Rightarrow B$ are in bijection with terms $x : A \vdash t : B$. By modus ponens (the counit of the adjunction $A \times (-) \vdash A \Rightarrow (-)$), if we have a term of type $A$ and a term of type $A \Rightarrow B$, we can form a term of type $B$. This corresponds to the process of substituting one term for a free variable in another (at the level of entailment).

You can think of (A) as a meta-logical construction, which is necessary to even talk about terms or derivations in the first place. Then (B) is a way to reason about entailment within the logic itself (it is not present in every logic, but can be constructed in Boolean logic as you point out).

$\endgroup$
2
  • 2
    $\begingroup$ I have often wondered about the exact difference between entailment and implication; upvoted and thank you. $\endgroup$
    – Alec Rhea
    Dec 5, 2020 at 5:31
  • $\begingroup$ Thanks, you taught me something new, but my question is more specifically about how the topos logic arrow can correspond to a type theory term via Curry-Howard (see edit). $\endgroup$
    – YKY
    Dec 5, 2020 at 17:19
9
$\begingroup$

The answers of varkor and Dmitri explain that in a given category, entailment corresponds to external homsets while implication corresponds to internal-homs. However, there's another thing going on here too that may be relevant to your question. When interpreting a logic over a type theory, the corresponding categorical structure is a fibration, in which there is both a base category (corresponding to types and terms) and a fiber category (corresponding to propositions and entailment). The Curry-Howard interpretation of "logic" happens only in the fiber category. Thus, the internal-hom in the base category corresponds to a function-type, while it is the internal-hom in the fiber category that corresponds to implication.

$\endgroup$
9
  • $\begingroup$ Thanks, my question is actually more related to your answer... specifically I don't know how the topos logic is related to the type theory via Curry-Howard. If there is an arrow $A \Rightarrow B$ in the fiber, how does one assure that there is a corresponding type or term in the base? $\endgroup$
    – YKY
    Dec 5, 2020 at 17:00
  • 2
    $\begingroup$ Essentially by definition, if I understand correctly. In the fibration constructed from a topos, the base category is the topos, while the fiber over an object $X$ is the poset of subobjects of $X$ (i.e. monomorphisms into $X$). So if there is an arrow $A\to B$ in the fiber, that means by definition that $A$ and $B$ are objects equipped with a monomorphism into $X$, and the former factors through the latter by a morphism $A\to B$. $\endgroup$ Dec 6, 2020 at 1:37
  • 2
    $\begingroup$ I can't really parse that sentence. Maybe this requires a longer discussion in a different forum. $\endgroup$ Dec 7, 2020 at 3:24
  • 1
    $\begingroup$ The (dependent) type corresponding to $\phi:A\to \Omega$ is the monomorphism $J \rightarrowtail A$ that it classifies, according to the universal property of $\Omega$. Substituting ${\rm John}:1\to A$ pulls this monomorphism back, yielding a subterminal object (a mere-proposition type). In the usual internal logic of a topos, not all types are regarded as propositions, only the monomorphisms (for dependent types) / subterminals (for non-dependent ones). $\endgroup$ Dec 23, 2020 at 21:30
  • 1
    $\begingroup$ Yes, they do coincide. $\endgroup$ Jan 9, 2021 at 18:16
7
$\begingroup$

Morphisms A→B form a set (typically denoted by C(A,B) or hom(A,B)), whereas the internal hom Hom(A,B) is an object in the same category C.

A morphism A→B corresponds to the entailment A⊢B, whereas the internal hom Hom(A,B) corresponds to the implication A⇒B.

Given a morphism A→B, by the product-hom adjunction we get a morphism 1→Hom(A,B). That is, A⊢B can be replaced by ⊢(A⇒B).

More generally, D,A⊢B can be replaced by D⊢(A⇒B), which correspons to replacing D⨯A→B with D→Hom(A,B). This is how you pass between these two notions.

if there is an arrow A⇒B in the fiber, as in (B), how does it correspond (via Curry-Howard) to some type or term in the base category?

Given some topos T and an object X of T, we can interpret the above in the category Sub(X) of subobjects of X, whose objects are monomorphisms A→X and morphisms are inclusions of subobjects.

Then if A and B are two subobjects of X, their internal implication A⇒B is another subobject of X, i.e., we have a monomorphism (A⇒B)→X in the topos T.

On the other hand, having an entailment A⊢B means that the subobject A of X (given by a monomorphism A→X) is contained in the subobject B of X (given by a monomorphism B→X), i.e., in the topos T there is a monomorphism A→B such that the composition A→B→X equals A→X.

The terminal object 1 of Sub(X) is the identity map X→X, and there is a morphism (i.e., entailment) from 1 to A⇒B in Sub(X) if and only if (by adjunction) A entails B in Sub(X), i.e., there is a morphism A→B in Sub(X).

That is, externally, (A⇒B)→X coincides with the identity map on X if and only if A is contained in B (as a subobject of X).

$\endgroup$
4
  • $\begingroup$ Thanks, but my question is more about how to ensure Curry-Howard correspondence between the topos-theoretic arrow and the type-theoretic term (see edit). $\endgroup$
    – YKY
    Dec 5, 2020 at 17:22
  • 1
    $\begingroup$ @YKY: I added an external interpretation for implication and entailment. $\endgroup$ Dec 5, 2020 at 22:53
  • $\begingroup$ Thanks, I am wondering about the type-theoretic interpretation of these, I guess I should look into the "internal language" of the topos. $\endgroup$
    – YKY
    Dec 7, 2020 at 3:10
  • $\begingroup$ @YKY: I am not sure what you're trying to say here. The relevant type theory does have function types, product types, etc., so what is written in the addendum make perfect sense type-theoretically. $\endgroup$ Dec 7, 2020 at 3:45
5
$\begingroup$

It's not always true that implication $A \Rightarrow B$ can be expressed as $\neg A \lor B$ [1]. This is in particular case in most systems in type theory at type level. Usually when the axiom of excluded middle is not assumed in the corresponding logic of types, implications cannot be expressed in terms of negation and disjunction.

[1] Crolard: Subtractive Logic

$\endgroup$
4
  • $\begingroup$ Thanks for pointing out, I'm aware of that. The Boolean algebra in my question could be replaced with Heyting algebra and the question seems still valid... $\endgroup$
    – YKY
    Dec 5, 2020 at 11:31
  • 1
    $\begingroup$ I'm confused as to whether the question is about the "kind level" or the "term level". In kind level there are things like "type", "type -> type" and "(type -> type) -> type -> type -> type", which classify parts of terms. In term level these correspond to things like "3 :: integer :: type", List :: type -> type, which induces [1,2,3] :: List(integer) :: type. $\endgroup$ Feb 12, 2021 at 18:30
  • $\begingroup$ Sorry to answer so late. I guess I have cleared up my understanding now. My question was about $A \Rightarrow B$ being defined using the "subobject" concept in a topos, but another definition of $A \Rightarrow B$ is via type theory as the internal language of a Cartesian Closed Category. And a topos is a CCC. So I was confused by two definitions of $A \Rightarrow B$. $\endgroup$
    – YKY
    Apr 29, 2022 at 23:34
  • $\begingroup$ I guess my question concerns only the most basic aspect of type theory, which probably does not involve "kinds". I'm not familiar with the latter concept. Does it arise because of dependent type theory? $\endgroup$
    – YKY
    Apr 29, 2022 at 23:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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