Two interpretations of implication in categorical logic?

Question

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?

Answer 1

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).

Answer 2

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.

Answer 3

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).

Answer 4

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