What is the meaning of implication (for instance)? As with any logical construct, we must first lay down what counts as an *instance* of the implication-form, and only then may we begin to propound the conditions under which an individual instance shall be considered *true* or *evident*. This basic formula of definition in two stages is due to Per Martin-Löf, and is reflected not only in the distinction between propositionhood and truth of a proposition, but also in the concepts of “good” (comprehensible) judgment and *evident* judgment.

Returning to our original question about implication, we may begin by studying the idiosyncratic explanation given by Martin-Löf in the Siena lectures:

\[ {\frac{ {{\phi}\ \mathsf{prop}} \quad {{\phi}\ \mathsf{true}}\vdash{{\psi}\ \mathsf{prop}} }{ {{\phi\supset\psi}\ \mathsf{prop}} }} \]

This is of course different from the usual well-formedness conditions of formal implication:

\[ {\frac{ {{\phi}\ \mathsf{prop}} \quad {{\psi}\ \mathsf{prop}} }{ {{\phi\supset\psi}\ \mathsf{prop}} }} \]

It is possible to understand Martin-Löf’s implication as a hint toward the unification of implication and universal quantification which is characteristic of the type-theoretic tradition. (Is this *logic* or something else? I will write more on that in a later post.) The significance of this connection is that it is possible to verify seemingly strange judgments like \({{\bot\supset 25}\ \mathsf{prop}}\), and even \({{\bot\supset 25}\ \mathsf{true}}\). This may seem completely pathological, but in practice this has some convincing applications. To see this, let us consider an analogous treatment of conjunction:

\[ {\frac{ {{\phi}\ \mathsf{prop}} \quad {{\phi}\ \mathsf{true}}\vdash{{\psi}\ \mathsf{prop}} }{ {{{{\phi}\mathrel{\&}{\psi}}}\ \mathsf{prop}} }} \]

Suppose that we are formalizing the semantics of a programming language in such a logic. It is easy to imagine that we would have a sort \({\mathsf{tm}}\) of terms and predicates of the following form, specifying when a term denotes a type, and when a term denotes an element of a type:

\[ {\frac{ }{ {{A}:{{\mathsf{tm}}}} \vdash {{{\mathsf{Typ}(A)}}\ \mathsf{prop}} }} \qquad {\frac{ }{ {{{\mathsf{Typ}(A)}}\ \mathsf{true}}, {{e}:{{\mathsf{tm}}}} \vdash {{{\mathsf{Mem}(e,A)}}\ \mathsf{prop}} }} \]

We have declared a membership predicate which presupposes that the typehood predicate holds of \(A\); this makes sense, because it is hard to say what membership should mean in any other case. The verification conditions for instances of a predicate are always restricted to that predicate’s range of significance.

On the other hand, after such a predicate has been defined, it may be useful to *speculatively* consider the question of whether \({\mathsf{Mem}(e,A)}\) is “true”, without first knowing whether \(A\) is a type. Naïvely, one may try to use the standard conjunction to express this, but it would not even be the case that \({{({\mathsf{Typ}(A)}\land{\mathsf{Mem}(e,A)})}\ \mathsf{prop}}\) holds! However, our special “dependent conjunction” is precisely what is needed, since we *do* have \({{({{{\mathsf{Typ}(A)}}\mathrel{\&}{{\mathsf{Mem}(e,A)}}})}\ \mathsf{prop}}\).

## Relation to Lawvere Quantifiers

We can make sense of these “nonstandard” connectives in the context of categorical logic quite easily, thanks to F. W. Lawvere and his Invincible Thought. In a hyperdoctrine \({{\mathfrak{P}}:{{{\mathbb{C}}^{\mathsf{op}}}\to{\mathbf{Cat}}}}\), among other things we have both a left and right adjoint to reindexing along any \({{f}:{T\to S:\mathbb{C}}}\) \[ \exists_f\dashv\mathfrak{P}(f)\dashv\forall_f \]

These adjoints, sometimes called “Lawvere quantifiers”, generalize ordinary existential and universal quantification in the sense that the latter comprise the cases where \(f\) is a *projection* map in \(\mathbb{C}\) (i.e. a weakening). In the case of the *subobject hyperdoctrine* (which takes every object of \(\mathbb{C}\) to its poset of subobjects), when \(\mathbb{C}\) is a Heyting category, these adjoints have a direct description in the internal language: \[\begin{align*}
\exists_f A &\triangleq \{y : T\mid \exists x : S. f(x) = y \land x\in A\}
\\
\forall_f A &\triangleq \{y : T\mid \forall x : S. f(x) = y \supset x\in A\}
\end{align*}\]

Supposing that \(\mathbb{C}\) has a subobject classifier \(\Omega\), we can easily interpret our little development. Fixing an object \({{{\mathsf{tm}}}:{\mathbb{C}}}\) which shall serve as our principal domain of discourse, we will specify our predicates as maps into the subobject classifier as follows:

- \({{{\mathsf{Typ}(-)}}:{{\mathsf{tm}}\to\Omega}}\)
- \({{{\mathsf{Mem}(-,-)}}:{{\mathsf{tm}}\times\{x:{\mathsf{tm}}\mid{\mathsf{Typ}(x)}\}\to\Omega}}\)

Observe how the “presupposition” or range of significance of the membership predicate is expressed in the *type* of the predicate, using subobject comprehension (which is induced in a topos by the universal property of the subobject classifier).

Next, write \({{{{\iota_{\mathsf{Typ}}}}}:{\{x:{\mathsf{tm}}\mid{\mathsf{Typ}(x)}\}\rightarrowtail{\mathsf{tm}}}}\) for the canonical inclusion of types into terms. Using the Lawvere quantifiers, it is now easy for us to interpret our assertion:

\[ \llcorner{{{\mathsf{Typ}(A)}}\mathrel{\&}{{\mathsf{Mem}(e,A)}}}\lrcorner \equiv A\in \exists_{{\iota_{\mathsf{Typ}}}}\{x\mid {\mathsf{Mem}(e,x)}\} \]

In fact, every instance of the \({{\phi}\mathrel{\&}{\psi}}\) connective can be intepreted using the generalized existential quantifier in the appropriate way. Dually, the concept of Martin-Löf’s version of implication is completely captured by the generalized universal quantifier.

### Acknowledgement

*Thanks for Bob Harper for a helpful discussion about presupposition, and quantification, and non-standard versions of conjunction and implication.*