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$
22
$\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
    $\begingroup$ I have often wondered about the exact difference between entailment and implication; upvoted and thank you. $\endgroup$ – Alec Rhea Dec 5 '20 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 '20 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$
  • $\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 '20 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$ – Mike Shulman Dec 6 '20 at 1:37
  • 2
    $\begingroup$ I can't really parse that sentence. Maybe this requires a longer discussion in a different forum. $\endgroup$ – Mike Shulman Dec 7 '20 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$ – Mike Shulman Dec 23 '20 at 21:30
  • 1
    $\begingroup$ Yes, they do coincide. $\endgroup$ – Mike Shulman Jan 9 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$
  • $\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 '20 at 17:22
  • 1
    $\begingroup$ @YKY: I added an external interpretation for implication and entailment. $\endgroup$ – Dmitri Pavlov Dec 5 '20 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 '20 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$ – Dmitri Pavlov Dec 7 '20 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$
  • $\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 '20 at 11:31

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.