Presupposition And Quantification.

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:

  1. \({{{\mathsf{Typ}(-)}}:{{\mathsf{tm}}\to\Omega}}\)
  2. \({{{\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.


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