This morning I had a little epiphany; I finally realized exactly why the HoTT book's idea of induction feels so wrong to me. It has to do with the difference between classical and intuitionistic reasoning about infinities. In this post I'll try to explain what I think is going on.
The general form of "induction principles" in the HoTT book seems to be something like the following: "to prove something for all x, it suffices to prove it for y". Turned around: "if you've proven something for y, then you have proved it for all x". If x is Nat, y is the base case and inductive step; for enumerated types, y is the base cases; for equality and coproduct types too, y is the base case.
The problem is that, as the HoTT book emphasizes, in the case of equality types there may be many proofs of equality distinct from the base case (refl) and from each other. In fact infinitely many. Now we can prove an equality for the base case by construction - refl(a) is by definition proof of a = a. But HoTT says that proving this base case suffices to prove all the other cases, no inductive hypothesis needed. How can this be? As I understand it, HoTT says that this works because the base case "freely generates" all the other cases. But that's a non-sequitur. Mathematical induction is a proof technique that depends on a particular conception of a non-terminating generative process; free generation is a mathematical concept that has nothing to do with proof, as far as I can tell. In free generation the base case freely generates all the other cases; it does not follow that a proof of the base case counts as proof of all the other cases - at least, not for intuitionistic reasoning. "Free generation" is just a description of how some things are related to some other things, not a proof technique. Plus it's not constructive. What gets generated, unlike inductively constructed elements, is not compositional; it does not build on the base case. Free "generation" is actually a misnomer; it refers to various properties, not to generation. The operative term in "freely generated" is "freely", not "generated". But "free" is defined in terms of the result of the generation process - what is generated, rather than generation - the process - itself. What's going on here?
I think the problem is that HoTT uses classical logic for the semantic domain, but type theory is intuitionistic. And under the intuitionistic perspective, a phrase like "proof of P for all x", where there are infinite xs, is absurd. The phrase "all x" is incoherent unless there are only finitely many xs, since there is no "all" to infinity. You can't prove stuff for an infinite totality because there is no such thing; the best you can do is provide a method for finding a proof for any element in the totality. (See the Dummett quotes below).
What about mathematical induction over Nat? We can treat the base case and the inductive step intuitionistically, the latter being a method of "going on in the same way". But the conclusion - "therefore P(n) for all n" should be replaced with "therefore for any n we can show (find) P(n)". Proving the base case and the inductive step does not mean we have given a proof for "all n"; it means we've given a proof method that works for any n: starting at the base case, we can run through the initial segment that terminates at that n.
When it comes to HoTT's "principles of induction" for coproducts, equalities, and the like, HoTT seems to rely on the classical logic of homotopy theory. The formula goes something like this: "if we've proven P for the constant path at a (base case), then we have proved it for every path (element of) a=b". The problem is that there are elements other than the base case, but there is no "initial segment" that links the others to the base case; there is no sequence. So we are given no way to prove P for any element other than the base case. There is no way to "keep going in the same way" in order to reach an arbitrary element. There is no way that I can see to construe such "induction principles" intuitionistically. They are not genuinely inductive.
The homotopic strategy seems to be to present the non-canonical tokens of, say, an equality type, as (non-canonical?) paths "freely generated" by the base case (refl). Once we have them, their endpoints count as "equal", since there is a path between the two. And under the classical perspective of the semantic domain (homotopy theory), we always already have them. But if we want an intuitionistic version of this idea suitable for constructive type theory, we need a means of actually constructing them in a way that allows us to "reach" them. We need a way of thinking of "free generation" as a non-terminating process that constructs these paths, one at a time, giving an initial segment for each element, which allows us to reach each in a constructive proof. I don't really see a way of doing this at the moment, but then again people like Beth, Bishop and Dummett have developed lots of techniques for reconstructing bits of classical mathematics intuitionistically, so maybe there is already a technique out there for handling this.
But I think there is another possibility that will allow us to prove things for the sorts of infinities involved in equalities, co-products, and the like without relying on a concept of induction. The trick is to think of two kinds of infinitary process, the inductive and the involutional. An infinite inductive process always "moves forward", so to speak. Each step in the process spits out a unique token. For nat, we get 0,1...n. An infinite involutive process goes nowhere; it just spins in place, turning in on itself (hence "involution"). Each cycle in the process spits out a unique token-repeatable. So an involution that produces 'a' generates a sequence: a,a,...a. Each a is a distinct particular, so they are not identical; but they are all 'a' tokens (hence "token-repeatables"), so they are interchangeable. And because of that, proving P(a) for a particular such 'a' is as good as proving it for any such 'a'; there is no need to run through an initial segment.
In terms of paths, the involutional process generates distinct 'a' tokens, so we should treat witnesses of e.g. a=b as paths from the canonical 'a' token to other 'a' tokens - which we call 'b', since there is really no way that a writing system can present this idea unambiguously using only 'a' tokens. We could also always write a=a so long as we agree that these two 'a' tokens need not be "the same", so to speak - in other words, x:a=a is not necessarily a reflexivity proof - it could also represent a path to a different 'a' token.
The key concept here is "token-repeatable", rather than "free generation". The notion of an involutive process generating a sequence of (equal) token-repeatables gives us an intuitionistically respectable interpretation of the concept of free generation. The process is non-terminating (hence infinitary) and sequential, creating initial segments; but the elements of those initial segments are token-repeatables, which makes them interchangeable, so there is no need to "run through" an initial segment to reach a particular such token. You can stop after the first one.
To cut a long story short: what the HoTT book calls "path induction" is not induction at all; it would be better to call it "path involution".
More details to follow in a separate post.
Dummett, Elements of Intuitionism
p. 4:
"The fact that quantification over an infinite totality shares so much in common with quantification over a finite one tempts us to overlook the crucial difference from the case in which we are quantifying over a finite totality which we can survey, namely that we do not have, even in principle, a method of determining the truth-value of a quantified statement by carrying out a complete inspection of the elements of the domain, and checking, for each one, whether the predicate applies.
p. 40-1:
"[T]he thesis that there is no completed infinity means, simply, that to grasp an infinite structure is to grasp the process that generates it, that to refer to such a structure is to refer to that process, and that to recognize a structure as being infinite is to recognize that the process will not terminate. In the case of a process that does terminate, we may legitimately distinguish between the process itself and its completed output: we may be presented with the structure that is generated, without knowing anything about the process of generation. But, in the case of an infinite structure, no such distinction is permissible: all that we can, at any given time, know of the output of the process of generation is some finite initial segment of the structure being generated. There is no sense in which we can have any conception of this structure as a whole save by knowing the process of generation."
p. 41:
"It is, however, integral to classical mathematics to treat infinite structures as if they could be completed and then surveyed in their totality, in other words, as if we could be presented with the entire output of an infinite process. Given his assumption that the application of a well-defined predicate to each element of the totality has a determinate value, true or false, the classical mathematician concludes that its universal closure has an equally determinate value, formed by taking the product of the values of its instances, and that the existential closure likewise has a determinate value, formed by taking the sum of the values of its instances. On such a conception, the truth-value of a quantified statement is the final outcome of a process which involves running through the values of all its instances; the assumption that its truth-value is well-defined and determinate is precisely the assumption that we may regard an infinite process of this kind as capable of completion... On an intuitionisitic view, neither the truth-value of a statement nor any other mathematical entity can be given as the final result of an infinite process, since an infinite process is precisely one that does not have a final result: that is why, when the domain of quantification is infinite, an existentially quantified statement cannot be regarded in advance as determinately either true or false, and a universally quantified one cannot be thought of as being true accidentally, that is independently of there being a proof of it, a proof which must depend intrinsically upon our grasp of the process whereby the domain is generated."
No comments:
Post a Comment