Note on Diaconescu’s Theorem.

Briefly, Diaconescu’s theorem states that the axiom of choice & extensionality together suffice to imply the principle of the excluded middle (PEM). In 100 Years of Zermelo’s Axiom of Choice, Martin-Löf distinguishes an intensional version of AC from an extensional one, and argues that whilst the former is a theorem of intuitionistic type theory, the latter leads to taboo. In this note, I hope to clarify a few matters, and demonstrate that the matter at hand is not so much extensionality, but infelicitous interpretation of quantifiers. When viewed through this lens, it becomes evident that the problem all along was setoids, not extensionality.

Now, to begin with, Martin-Löf is operating in an intensional framework with setoids; a setoid is an “extensional set”, a set together with an equivalence relation. If \(I\) is a setoid, then \({|I|}\) is the set of its elements, and \({x\sim_{I} y}\) is the set of equivalences between \({{\color{MidnightBlue}{x,y}}}:{{\color{MidnightBlue}{{|I|}}}}\). The standard type constructors of type theory, such as \({(\Pi x\in A)\;B}\) and \({(\Sigma x\in A)\;B}\) operate on sets,1 not setoids.

Separate, derived quantifiers may be written which operate on setoids, enforcing the fact that functions between setoids should be extensional (that is, they should respect the equivalence relations of the domain and codomain). Note that for an operation to be extensional is the same as for it to be a function or functional; however, as you will see, it is crucial to ask, «functional with respect to what?».

In order to make his point, Martin-Löf needed only to define a predicate \({\mathsf{Ext}(f)}\) which expressed the extensionality of the operation \(f : {|I|}\to{|S|}\) where \(I,S\) are setoids:

\[ {{{\color{MidnightBlue}{ {\mathsf{Ext}(f)} }}}\equiv{{\color{Maroon}{ {(\Pi x\in {|I|})\; {(\Pi y\in {|I|})\; {x\sim_{I} y}\to {f(x)\sim_{S} f(y)} } } }}}} \]

As Martin-Löf presents it, the intensional axiom of choice (the “theorem of choice”), operates on sets, not necessarily setoids:

\[ {{{\color{MidnightBlue}{ {\mathsf{AC}}}}}\equiv{{\color{Maroon}{ ({(\Pi a\in A)\; {(\Sigma b\in B)\; Q(a,b) } })\to {(\Sigma f\in A\to B)\; {(\Pi a\in A)\; Q(a,f(a)) } } }}}} \]

This is evidently a theorem in ITT, witnessed by the following term:

\[\begin{align} {{\color{MidnightBlue}{{\mathsf{ac}}}}} &: {{\color{MidnightBlue}{{\mathsf{AC}}}}}\\ {{\color{MidnightBlue}{{\mathsf{ac}}}}} &\equiv {{\color{Maroon}{ {(\lambda q) {\langle {(\lambda a){q(a)_1}} , {(\lambda a){q(a)_2}} \rangle} } }}} \end{align}\]

On the other hand, Martin-Löf gives another variant of the axiom of choice, which he calls extensional, and proves equivalent to Zermelo’s axiom: \[ {{{\color{MidnightBlue}{ {\mathsf{AC}_\mathit{ext}}}}}\equiv{{\color{Maroon}{ ({(\Pi x\in {|I|})\; {(\Sigma y\in {|S|})\; Q(x,y) } })\to {(\Sigma f\in {|I|}\to{|S|})\; {\mathsf{Ext}(f)} \times {(\Pi x\in {|I|})\; Q(x,f(x)) } } }}}} \]

Note the crucial differences between \({\mathsf{AC}}\) and \({\mathsf{AC}_\mathit{ext}}\):

  1. \({\mathsf{AC}_\mathit{ext}}\) is defined over setoids, and says that any total relation between the elements of two setoids gives rise to a choice function.

  2. \({\mathsf{AC}}\) is defined over sets, and says that any total relation between elements of two sets gives rise to a choice function.

Now, not only is \({\mathsf{AC}_\mathit{ext}}\) not evident in ITT, Diaconescu’s result when transported to type theory shows that it in fact implies PEM.

Shifting Blame: Rehabilitating Extensionality

It may at first seem, then, that extensionality is at fault. This is what a naïve reading of Diaconescu’s result suggests, and this is also the conclusion that Martin-Löf came to in his paper, saying:

Within an extensional foundational framework, like topos theory or constructive set theory, it is not wholly impossible to formulate a counterpart of the constructive [intensional] axiom of choice, despite its intensional character, but it becomes complicated. In topos theory, there is the axiom that there are enough projectives, which is to say that every object is the surjective image of a projective object, and, in constructive set theory, Aczel has introduced the analogous axiom that every set has a base. Roughly speaking, this is to say that every set is the surjective image of a set for which the axiom of choice holds. The technical complication of these axioms speaks to my mind for an intensional foundational framework, like constructive type theory, in which the intuitive argument why the axiom of choice holds on the Brouwer-Heyting-Kolmogorov interpretation is readily formalized, and in which whatever extensional notions that are needed can be built up, in agreement with the title of Martin Hofmann’s thesis, Extensional Constructs in Intensional Type Theory. Extensionality does not come for free.

However, on closer examination, I do not think that this conclusion is tenable, given the following facts which I will make evident in the sequent paragraphs:

  1. From a type theoretic perspective, \({\mathsf{AC}_\mathit{ext}}\) is mere sleight of hand and depends on an infelicitous interpretation of the quantifiers.

  2. Extensional type theory2 itself is not susceptible to Diaconescu’s Theorem.

The Art of Disillusionment

Why is \({\mathsf{AC}_\mathit{ext}}\) not evident in intuitionistic type theory? For precisely the same reason that PEM is not valid in ITT, which is to say that it violates the principle that something cannot be got from nothing.3

What business does anyone have expecting an operation to be extensional when there is no evidence that this is the case? In fact, the proof of type-theoretic Diaconescu follows by encoding the decidability of an arbitrary proposition into the extensionality of an operation: if someone is offering you extensionality for free, you might as well get them to give you global choice as well. In this way, the confusion of ideas that leads one to believe in \({\mathsf{AC}_\mathit{ext}}\) is precisely (not just figuratively) the same confusion of ideas which leads one to believe in PEM (if it can be said that anyone really believes in that anyway).

If read closely, the argument for intensional foundations which follows from this taboo may make sense from a set-theoretic point of view, but this is only because in set theory, there is no over-arching natural law which states that every object is invariant under equivalence. The weakness inherent in the set-theoretic approach is evident, in that it greatly complicates the treatment of mathematical (i.e. extensional) objects in a constructive manner.

Intensional type theory with setoids has the exact same problem: because the entire framework is organized around intensional concepts (i.e. codes, expressions, algorithms, operations), it is easy to translate an informal mathematical statement into a type theoretic proposition inadequately:

\[ {{\color{MidnightBlue}{\textit{«$Q$ is a total relation between setoids $I,S$»}}}} \gg {{\color{Maroon}{ {(\Pi x\in {|I|})\; {(\Sigma y\in {|S|})\; Q(x,y) } } }}} \tag{*} \]

The above encoding, which is precisely the one in the premise of \({\mathsf{AC}_\mathit{ext}}\), is not adequate; it only encodes the statement «\(Q\) is a total relation between the carrier sets of setoids \(I, S\)». Like most illusions, the magic gives way as soon as it is examined carefully. It should be no surprise that this \({\mathsf{AC}_\mathit{ext}}\) is not a theorem of ITT, and this does not comprise an indictment of foundations which are overly extensional: it actually is a strong indication that ITT is not extensional enough!

Functionality and General Judgement

Why is extensional type theory not susceptible to Diaconescu’s result? For the simple reason that ETT begins directly with sets that correspond to ITT’s setoids, and does not have an intensional layer at which equivalent objects of a set could be distinguished. As such, all the constructs of ETT are designed from the start to enforce the natural law that all definable objects are invariant under equivalence.

When looking to place blame for a violation of this principle, the first place to check should be the treatment of hypothetico-general judgement, since this is the place where this principle will be won or lost. In ETT, hypothetico-general judgement is posterior to both the categorical judgements \({{{\color{MidnightBlue}{A}}}\ \textit{set}}\), \({{{\color{MidnightBlue}{A}}}={{\color{MidnightBlue}{B}}}\ \textit{set}}\), \({{{\color{MidnightBlue}{M}}}\in{{\color{MidnightBlue}{A}}}}\) and \({{{\color{MidnightBlue}{M}}}={{\color{MidnightBlue}{N}}}\in{{\color{MidnightBlue}{A}}}}\), and the higher-order judgements \({\mathcal{J}_2\ \ (\mathcal{J}_1)}\) and \({\vert_{{{\color{MidnightBlue}{x}}}}\, \mathcal{J}(x)}\).

The sequent judgements \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{A}}}\ \textit{set}}}\), \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{A}}}={{\color{MidnightBlue}{B}}}\ \textit{set}}}\), \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{M}}}\in{{\color{MidnightBlue}{A}}}}}\) and \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{M}}}={{\color{MidnightBlue}{N}}}\in{{\color{MidnightBlue}{A}}}}}\) are defined by mutual induction on the evidence of their presupposition \({{{\color{MidnightBlue}{\Gamma}}}\ \textit{ctx}}\) (the meaning of which is purely formal):

\[\begin{gather} {\dfrac{\matrix{ }}{ {{{\color{MidnightBlue}{\cdot}}}\ \textit{ctx}} }}\qquad {\dfrac{\matrix{ {{{\color{MidnightBlue}{\Gamma}}}\ \textit{ctx}} & {{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{A}}}\ \textit{set}}} & {{{\color{MidnightBlue}{x}}}\,\#\,{{\color{MidnightBlue}{\Gamma}}}} }}{ {{{\color{MidnightBlue}{(\Gamma,x:A)}}}\ \textit{ctx}} }} \end{gather}\]

Then, we may give meaning explanations for the forms of sequent judgement; intuitively, we define a sequent \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{A}}}\ \textit{set}}}\) based on the notion of an environment for \({{\color{MidnightBlue}{\Gamma}}}\equiv{{\color{Maroon}{x_0:A_0,\dots,x_n:A_n}}}\), which is a vector of terms \({{\color{MidnightBlue}{\rho}}}\equiv{{\color{Maroon}{M_0,\dots,M_n}}}\) which inhabit \(A_0,[M_0/x_0]A_1,\dots,[M_0,\dots,M_{n-1}/x_0,\dots,x_{n-1}]A_n\) respectively. Equality of environments is pointwise.

Then, a sequent \({{{\color{MidnightBlue}{\Gamma}}}\gg {{{\color{MidnightBlue}{A}}}\ \textit{set}}}\) is defined in the following way: for any equal environments \(\rho_0,\rho_1\) of \(\Gamma\), \({{{\color{MidnightBlue}{[\rho_0/\Gamma]A}}}={{\color{MidnightBlue}{[\rho_1/\Gamma]A}}}\ \textit{set}}\); the remainder of the sequent judgments are defined in the same way. The quantification over environments used here is formally an instance of the primitive general judgment \({\vert_{{{\color{MidnightBlue}{x}}}}\, \mathcal{J}(x)}\) and hypothetical judgment \({\mathcal{J}_2\ \ (\mathcal{J}_1)}\); after this point, these primitives are eschewed and the above sequents, which induce functionality in addition to generality, are used in their place; this enforces that equivalence is respected at every turn.

For instance, we will say that the sethood of the cartesian product of a family of sets \(B\) fibred over \(A\) is a evident when we know \({{{\color{MidnightBlue}{A}}}\ \textit{set}}\) and \({{{\color{MidnightBlue}{x:A}}}\gg {{{\color{MidnightBlue}{B}}}\ \textit{set}}}\); then, unfolding the meaning explanation, it suffices to say what is a canonical verification of \({(\Pi x\in A)\;B}\) under the circumstances that the evidence of the hypotheses is known to us, and when two such canonical verifications are equal:

A canonical verification of \({(\Pi x\in A)\;B}\) (assuming \({{{\color{MidnightBlue}{A}}}\ \textit{set}}\) and \({{{\color{MidnightBlue}{x:A}}}\gg {{{\color{MidnightBlue}{B}}}\ \textit{set}}}\)) is a term \({(\lambda x)E}\) such that \({{{\color{MidnightBlue}{x:A}}}\gg {{{\color{MidnightBlue}{E}}}\in{{\color{MidnightBlue}{B}}}}}\); two verifications \({(\lambda x)E}\) and \({(\lambda x)E'}\) are equal when \({{{\color{MidnightBlue}{x:A}}}\gg {{{\color{MidnightBlue}{E}}}={{\color{MidnightBlue}{E'}}}\in{{\color{MidnightBlue}{B}}}}}\).

The standard introduction and elimination rules at contexts \(\Gamma\) are then admissible according to the meanings of the judgements of type theory.

So, what was the purpose of this excursion? It was to demonstrate that the standard interpretation of the quantifiers in ETT requires functionality with respect to a set(oid)’s equivalence relation from the start, and this is the reason that the “theorem of choice” really is a theorem in ETT. The problem was never, then, with extensionality; rather, the taboo arises from a failure of extensionality to be sufficiently pervasive in both set theoretic and intensional type theoretic foundations. Intensionality does not come for free.

Postscript & Acknowledgements

The problem which I identify is not so much one of intensional type theory, but rather with the practice of using setoids inside an intensional foundational framework. The failure of extensionality disappears whenever the setoids (or \(\omega\)-groupoids, or whatever is the taste of the day) are internalized into the type theory; whether it is done at the judgemental level as in ETT, or at the propositional level as in Observational Type Theory or Homotopy Type Theory, is immaterial.

Thanks to Darin Morrison for getting me worried about Diaconescu’s Theorem in extensional type theory; thanks to Bob Harper for providing clarity, as always. Thanks to Carlo Angiuli for alerting me to an error in the definition of the functional sequent judgment.

  1. I’m using Martin-Löf’s current terminology, in which a set is a small type.

  2. Note that I will use the term «extensional type theory» and its abbreviation ETT in this post to refer to Martin-Löf’s type theory between 1979 and 1986, which is characterized by the verificationist meaning explanations and the modular definitions of types. I do not refer to what many (mostly non-type theorists) define as intensional type theory + equality reflection, which has never existed in any meaningful sense except in the imaginations of formalists.

    When Martin-Löf wrote down the equality reflection rule in Constructive Mathematics and Computer Programming, he was giving it as an example of an evident (valid, admissible) rule under his meaning explanation; in the same way as the elimination rules do not have any part in defining the other types, equality reflection has nothing to do with the definition of the identity type. Moreover, the things which made ETT different from modern intensional type theory would continue to set it apart even in the absense of an identity type.

  3. Credit for the expression of this dictum belongs to Bob Harper.