Constructivity


One of the most striking differences between classical foundations and type theoryPlanetmathPlanetmath is the idea of proof relevance, according to which mathematical statements, and even their proofs, become first-class mathematical objects. In type theory, we represent mathematical statements by types, which can be regarded simultaneously as both mathematical constructions and mathematical assertions, a conception also known as propositions as types. Accordingly, we can regard a term a:A as both an element of the type A (or in homotopy type theory, a point of the space A), and at the same time, a proof of the propositionPlanetmathPlanetmath A. To take an example, suppose we have sets A and B (discrete spaces), and consider the statement “A is isomorphic to B.” In type theory, this can be rendered as:

𝖨𝗌𝗈(A,B):(f:AB)(g:BA)(((x:A)g(f(x))=x)×((y:B)f(g(y))=y)).

Reading the type constructors Σ,Π,× here as “there exists”, “for all”, and “and” respectively yields the usual formulation of “A and B are isomorphic”; on the other hand, reading them as sums and productsPlanetmathPlanetmathPlanetmathPlanetmath yields the type of all isomorphismsMathworldPlanetmathPlanetmathPlanetmath between A and B! To prove that A and B are isomorphic, one constructs a proof p:𝖨𝗌𝗈(A,B), which is therefore the same as constructing an isomorphism between A and B, i.e., exhibiting a pair of functions f,g together with proofs that their composites are the respective identity maps. The latter proofs, in turn, are nothing but homotopiesMathworldPlanetmath of the appropriate sorts. In this way, proving a proposition is the same as constructing an element of some particular type.

In particular, to prove a statement of the form “A and B” is just to prove A and to prove B, i.e., to give an element of the type A×B. And to prove that A implies B is just to find an element of AB, i.e. a function from A to B (determining a mapping of proofs of A to proofs of B). This “constructive” conception (for more on which, see [3],[10],[11]) is what gives type theory its good computational character. For instance, every proof that something exists carries with it enough information to actually find such an object; and from a proof that “A or B” holds, one can extract either a proof that A holds or one that B holds. Thus, from every proof we can automatically extract an algorithm; this can be very useful in applications to computer programming.

However, this conception of logic does behave in ways that are unfamiliar to most mathematicians. On one hand, a naive translation of the axiom of choiceMathworldPlanetmath yields a statement that we can simply prove. Essentially, this notion of “there exists” is strong enough to ensure that, by showing that for every x:A there exists a y:B such that R(x,y), we automatically construct a function f:AB such that, for all x:A, we have R(x,f(x)).

On the other hand, this notion of “or” is so strong that a naive translation of the law of excluded middleMathworldPlanetmathPlanetmath is inconsistent with the univalence axiom. For if we assume “for all A, either A or not A”, then since proving “A” means exhibiting an element of it, we would have a uniform way of selecting an element from every nonempty type — a sort of Hilbertian choice operator. However, univalence implies that the element of A selected by such a choice operator must be invariant under all self-equivalences of A, since these are identified with self-identities and every operationMathworldPlanetmath must respect identityPlanetmathPlanetmathPlanetmath. But clearly some types have automorphismsPlanetmathPlanetmathPlanetmathPlanetmath with no fixed pointsPlanetmathPlanetmath, e.g. we can swap the elements of a two-element type.

Thus, the logic of “proposition as types” suggested by traditional type theory is not the “classical” logic familiar to most mathematicians. But it is also different from the logic sometimes called “intuitionistic”, which may lack both the law of excluded middle and the axiom of choice. For present purposes, it may be called constructive logic (but one should be aware that the terms “intuitionistic” and “constructive” are often used differently).

The computational advantages of constructive logic imply that we should not discard it lightly; but for some purposes in classical mathematics, its non-classical character can be problematic. Many mathematicians are, of course, accustomed to rely on the law of excluded middle; while the “axiom of choice” that is available in constructive logic looks superficially similar to its classical namesake, but does not have all of its strong consequences. Fortunately, homotopy type theory gives a finer analysis of this situation, allowing various different kinds of logic to coexist and intermix.

The new insight that makes this possible is that the system of all types, just like spaces in classical homotopy theory, is “stratified” according to the dimensionsMathworldPlanetmathPlanetmath in which their higher homotopy structureMathworldPlanetmath exists or collapses. In particular, Voevodsky has found a purely type-theoretic definition of homotopy n-types, corresponding to spaces with no nontrivial homotopy information above dimension n. (The 0-types are the “sets” mentioned previously as satisfying Lawvere’s axioms.) Moreover, with higher inductive types, we can universally “truncate” a type into an n-type; in classical homotopy theory this would be its nth Postnikov section.

With these notions in hand, the homotopy (-1)-types, which we call (mere) propositions, supportMathworldPlanetmath a logic that is much more like traditional “intuitionistic” logic. (Classically, every (-1)-type is empty or contractibleMathworldPlanetmath; we interpret these possibilities as the truth values “false” and “true” respectively.) The “(-1)-truncated axiom of choice” is not automatically true, but is a strong assumptionPlanetmathPlanetmath with the same sorts of consequences as its counterpart in classical set theoryMathworldPlanetmath. Similarly, the “(-1)-truncated law of excluded middle” may be assumed, with many of the same consequences as in classical mathematics. Thus, the homotopical perspective reveals that classical and constructive logic can coexist, as endpoints of a spectrum of different systems, with an infiniteMathworldPlanetmathPlanetmath number of possibilities in between (the homotopy n-types for -1<n<). We may speak of “𝖫𝖤𝖬n” and “𝖠𝖢n”, with 𝖠𝖢 being provable and 𝖫𝖤𝖬 inconsistent with univalence, while 𝖠𝖢-1 and 𝖫𝖤𝖬-1 are the versions familiar to classical mathematicians (hence in most cases it is appropriate to assume the subscript (-1) when none is given). Indeed, one can even have useful systems in which only certain types satisfy such further “classical” principles, while types in general remain “constructive.”

It is worth emphasizing that univalent foundations does not require the use of constructive or intuitionistic logicMathworldPlanetmath. Most of classical mathematics which depends on the law of excluded middle and the axiom of choice can be performed in univalent foundations, simply by assuming that these two principles hold (in their proper, (-1)-truncated, form). However, type theory does encourage avoiding these principles when they are unnecessary, for several reasons.

First of all, every mathematician knows that a theorem is more powerful when proven using fewer assumptions, since it applies to more examples. The situation with 𝖠𝖢 and 𝖫𝖤𝖬 is no different: type theory admits many interesting “nonstandard” models, such as in sheaf toposes, where classicality principles such as 𝖠𝖢 and 𝖫𝖤𝖬 tend to fail. Homotopy type theory admits similar models in higher toposes, such as are studied in [9],[8],[7]. Thus, if we avoid using these principles, the theorems we prove will be valid internally to all such models.

Secondly, one of the additional virtues of type theory is its computable character. In addition to being a foundation for mathematics, type theory is a formal theory of computation, and can be treated as a powerful programming language. From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs. We do not yet fully understand the new principles introduced by homotopy type theory, such as univalence and higher inductive types, from this point of view, but the basic outlines are emerging; see, for example, [5]. It has been known for a long time, however, that principles such as 𝖠𝖢 and 𝖫𝖤𝖬 are fundamentally antithetical to computability, since they assert baldly that certain things exist without giving any way to compute them. Thus, avoiding them is necessary to maintain the character of type theory as a theory of computation.

Fortunately, constructive reasoning is not as hard as it may seem. In some cases, simply by rephrasing some definitions, a theorem can be made constructive and its proof more elegant. Moreover, in univalent foundations this seems to happen more often. For instance:

  1. 1.

    In set-theoretic foundations, at various points in homotopy theory and category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath one needs the axiom of choice to perform transfinite constructions. But with higher inductive types, we can encode these constructions directly and constructively. In particular, none of the “synthetic” homotopy theory in http://planetmath.org/node/87582Chapter 8 requires 𝖫𝖤𝖬 or 𝖠𝖢.

  2. 2.

    In set-theoretic foundations, the statement “every fully faithful and essentially surjective functor is an equivalence of categories” is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to the axiom of choice. But with the univalence axiom, it is just true; see http://planetmath.org/node/87583Chapter 9.

  3. 3.

    In set theory, various circumlocutions are required to obtain notions of “cardinal numberMathworldPlanetmath” and “ordinal numberMathworldPlanetmath” which canonically represent isomorphism classes of sets and well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of foundation. But with univalence and higher inductive types, we can obtain such representatives directly by truncating the universePlanetmathPlanetmath; see http://planetmath.org/node/87584Chapter 10.

  4. 4.

    In set-theoretic foundations, the definition of the real numbers as equivalence classesMathworldPlanetmath of Cauchy sequencesPlanetmathPlanetmath requires either the law of excluded middle or the axiom of (countableMathworldPlanetmath) choice to be well-behaved. But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles; see http://planetmath.org/node/87585Chapter 11.

Of course, these simplifications could as well be taken as evidence that the new methods will not, ultimately, prove to be really constructive. However, we emphasize again that the reader does not have to care, or worry, about constructivity in order to read this book. The point is that in all of the above examples, the version of the theory we give has independent advantages, whether or not 𝖫𝖤𝖬 and 𝖠𝖢 are assumed to be available. Constructivity, if attained, will be an added bonus.

Given this discussion of adding new principles such as univalence, higher inductive types, 𝖠𝖢, and 𝖫𝖤𝖬, one may wonder whether the resulting system remains consistent. (One of the original virtues of type theory, relative to set theory, was that it can be seen to be consistent by proof-theoretic means). As with any foundational system, consistency is a relative question: “consistent with respect to what?” The short answer is that all of the constructions and axioms considered in this book have a model in the category of Kan complexes, due to Voevodsky [2] (see [6] for higher inductive types). Thus, they are known to be consistent relative to ZFC (with as many inaccessible cardinalsMathworldPlanetmath as we need nested univalent universes). Giving a more traditionally type-theoretic account of this consistency is work in progress (see, e.g., [5],[1]).

We summarize the different points of view of the type-theoretic operations in Table 1.

Types Logic Sets Homotopy
A proposition set space
a:A proof element point
B(x) predicate family of sets fibrationMathworldPlanetmath
b(x):B(x) conditional proof family of elements sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath
𝟎,𝟏 , ,{} ,*
A+B AB disjoint unionMathworldPlanetmathPlanetmath coproductMathworldPlanetmath
A×B AB set of pairs product space
AB AB set of functions function space
(x:A)B(x) x:AB(x) disjoint sum total space
(x:A)B(x) x:AB(x) product space of sections
𝖨𝖽A equality = {(x,x)|xA} path space AI
Table 1: Comparing points of view on type-theoretic operations

References

  • 1 Bruno Barras and Thierry Coquand and Simon Huber. A GeneralizationPlanetmathPlanetmath of Takeuti-Gandy InterpretationMathworldPlanetmath. \urlhttp://uf-ias-2012.wikispaces.com/file/view/semi.pdf, 2013.
  • 2 Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2012. \hrefhttp://arxiv.org/abs/1211.2851/arXiv:1211.2851.
  • 3 Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35:58–65 1932
  • 4 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
  • 5 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
  • 6 Peter LeFanu Lumsdaine and Michael Shulman. Higher inductive types. In preparation, 2013.
  • 7 Jacob Lurie, Higher topos theory Princeton University Press,2009
  • 8 Charles Rezk. Toposes and homotopy toposes. \urlhttp://www.math.uiuc.edu/ rezk/homotopy-topos-sketch.pdf, 2005.
  • 9 Bertrand Toën and Gabriele Vezzosi. Homotopical Algebraic Geometry I: Topos theory, 2002. \hrefhttp://arxiv.org/abs/math/0207028/arXiv:math/0207028.
  • 10 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. I North-Holland Publishing Co.,1988
  • 11 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. II North-Holland Publishing Co.,1988
Title Constructivity
\metatable