Returning to constructivity and (un)truncated logic

[mikeshulman]

The introduction to the book currently says

Using all types as propositions yields a "constructive" conception of logic... which gives type theory its good computational character.

Multiple people have complained about this sort of remark (at least Vladimir, Thierry, and Martin, I think), and I would now like to add my voice to them. At best, I think this remark is misleading because it is vague about what is meant by "computational character", and there are meanings of "computation" for which truncated logic is perfectly computational. For instance, computational models such as setoids and (now) cubical sets do implement (-1)-truncation. Moreover, plenty of people doing "constructive" mathematics have used (-1)-truncated logic.

In fact, I am no longer even sure what this remark is referring to. If I remember correctly, @RobertHarper was one of the main voices at IAS advocating the value of untruncated logic in computation, but I don't remember the exact arguments. Right now, the only possibility I can think of is that when using type theory as a programming language itself, rather than extracting programs from it metatheoretically, having an element of A+B (for instance) allows us to match on it and define functions into arbitrary types, whereas with only an element of A\/B our codomains would be restricted to propositions. However, it seems to me right now that this observation actually has little to do with computation specifically --- it is just as true in pure mathematics that an element of A+B is more useful than an element of A\/B, for the same reason.

Is there any sense in which untruncated logic is "more computational" than truncated logic? If not, we should modify this sentence.

[RobertHarper]

I don’t think so; NuPRL had truncation ages ago, and is computational. The discussion on this topic at the IAS was, as I remember, whether intuitionistic propositions are truncated or not. It seems to me that Brouwer’s conception of disjunction and existence was exactly that propositions are not truncated by nature; one has to get a witness from the proof.

Bob

On Feb 5, 2015, at 13:03, Mike Shulman notifications@github.com wrote:

The introduction to the book currently says

Using all types as propositions yields a "constructive" conception of logic... which gives type theory its good computational character.

Multiple people have complained about this sort of remark (at least Vladimir, Thierry, and Martin, I think), and I would now like to add my voice to them. At best, I think this remark is misleading because it is vague about what is meant by "computational character", and there are meanings of "computation" for which truncated logic is perfectly computational. For instance, computational models such as setoids and (now) cubical sets do implement (-1)-truncation. Moreover, plenty of people doing "constructive" mathematics have used (-1)-truncated logic.

In fact, I am no longer even sure what this remark is referring to. If I remember correctly, @RobertHarper https://github.com/RobertHarper was one of the main voices at IAS advocating the value of untruncated logic in computation, but I don't remember the exact arguments. Right now, the only possibility I can think of is that when using type theory as a programming language itself, rather than extracting programs from it metatheoretically, having an element of A+B (for instance) allows us to match on it and define functions into arbitrary types, whereas with only an element of A\/B our codomains would be restricted to propositions. However, it seems to me right now that this observation actually has little to do with computation specifically --- it is just as true in pure mathematics that an element of A+B is more useful than an element of A\/B, for the same reason.

Is there any sense in which untruncated logic is "more computational" than truncated logic? If not, we should modify this sentence.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/764.

[mikeshulman]

Hmm, well, maybe I am misremembering then. In that case, we should certainly change it!

[martinescardo]

I agree with everything except the claim that Brouwer worked with untruncated propositions. In his mathematics, all functions (N->N)->N are continuous (an internal mathematical statement). If you formulate continuity with untruncated propositions, then you conclude from the continuity of all functions (N->N)->N that 0=1. If you instead formulate continuity with truncated Sigma to express existence, you get a consistent statement in MLTT (validated in the topological topos) when you say that all functions (N->N)->N are continuous. That the untruncated continuity of all functions implies 0=1 holds in intensional MLTT. But the intensionality is a moot point, because only propositional equality on natural numbers is used to formulate continuity, and this propositional equality is definable by induction on N if we have a universe, and so identity types are not needed to formulate the untruncated notion of continuity and prove that if all functions are continuous then 0=1. So it is hard to accept that Brouwer had the proposition-as-types conception of logic.

[martinescardo]

Also: Mike, you say that A+B is more useful than AvB [when we can get it]. By extension, you would say that Sigma(x:X).A(x) is more useful than Exists(x:X).A(x) [again when we can get it]. This may be so in several examples of interest. But in other examples of interest, it is more useful to have Exists(x:X).A(x) rather than Sigma(x:X),A(x), such as in the definitions of image and of surjection. It is precisely because of such things that NuPrl introduced truncation (bracket types). Computation is about getting information. When we are consumers (read an input), we would rather have Sigma(x:X).A(x) than Exists(x:X).A(x), as it gives more information. But when we are producers (write an output), we may give the less precise information Exists(x:X).A(x), either because we are not able to get the more informative Sigma(x:X).A(x) or because, for whatever reason, we choose to give less information than we have available.

[mikeshulman]

@martinescardo I agree entirely. By the phrase "having an element" I meant to indicate reference only to the consumer situation.

[awodey]

I think it’s just referring (obliquely, to be sure) to the fact that a proof of (Pi x)(Sigma y) R(x,y) gives a function from the x’s to y’s, which of course is not the case of a proof of (forall x)(exists y) R(x,y). I’m not saying that is a reason to regard the former type as a “proposition”, but it is a difference that should be taken into account somehow.

Personally, I think that the pure PaT interpretaion is too coarse, and one should use Pa[T].

On Feb 5, 2015, at 1:03 PM, Mike Shulman notifications@github.com wrote:

The introduction to the book currently says

Using all types as propositions yields a "constructive" conception of logic... which gives type theory its good computational character.

Multiple people have complained about this sort of remark (at least Vladimir, Thierry, and Martin, I think), and I would now like to add my voice to them. At best, I think this remark is misleading because it is vague about what is meant by "computational character", and there are meanings of "computation" for which truncated logic is perfectly computational. For instance, computational models such as setoids and (now) cubical sets do implement (-1)-truncation. Moreover, plenty of people doing "constructive" mathematics have used (-1)-truncated logic.

In fact, I am no longer even sure what this remark is referring to. If I remember correctly, @RobertHarper https://github.com/RobertHarper was one of the main voices at IAS advocating the value of untruncated logic in computation, but I don't remember the exact arguments. Right now, the only possibility I can think of is that when using type theory as a programming language itself, rather than extracting programs from it metatheoretically, having an element of A+B (for instance) allows us to match on it and define functions into arbitrary types, whereas with only an element of A\/B our codomains would be restricted to propositions. However, it seems to me right now that this observation actually has little to do with computation specifically --- it is just as true in pure mathematics that an element of A+B is more useful than an element of A\/B, for the same reason.

Is there any sense in which untruncated logic is "more computational" than truncated logic? If not, we should modify this sentence.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/764.

[andrejbauer]

I agree that we should change this.

[mikeshulman]

I see that a couple years ago I wrote

When doing verified programming, frequently one does want to “prove a theorem” about a program one has written, and then extract computational content from that proof. This is not possible if when one is “proving a theorem” one must always be truncating types.

Is that correct?

[andrejbauer]

I am not sure I understand your question. If you've already written your program and you're just concerned with its correctness (and computational complexity) then it's very likely you're going to do everything truncatedly because you do not care about futher extraction, and it's easier to prove a truncated proposition than a non-truncated one.

A typical example is sorting of lists of natural numbers:

forall l : list nat, { k : list nat & ordered k /\ permutation_of k l }

The bit you care about is the map from lists to lists. The untruncated version also gives you an explicit permutation from l to k.

[mikeshulman]

But you do need the sigma { k : list nat & ... } to be untruncated in order to even have a map from lists to lists. That's not exactly what I originally said (we're writing a program rather than proving something about an already-written program) but we could view this program with its specification as a proof in untruncated logic that "every list can be permuted into an ordered one". Right?

[andrejbauer]

Sure, the truncations are inside, in "there merely exists a permutation".

[martinescardo]

Bob: I said above that I am not convinced that Brouwer really meant the so-called Brouwer-Heyting-Kolmogorov interpretation of mathematical statements, which, in type theory, corresponds to the Curry-Howard interpretation. I wrote, together with my student Chuangjie Xu, a paper about that. In the paper, we deliberately refrain from making speculative remarks regarding what Brouwer may have had in mind. We deliberately confine ourselves to the mathematical facts (also proved in Agda). It seems to me (and we didn't write this in the paper) that if Brouwer's mathematics was correct, then he could not have meant the BHK interpretation of his claims without getting into a contradiction. The mathematical facts regarding this are recorded here: http://www.cs.bham.ac.uk/~mhe/papers/escardo-xu-inconsistency-continuity.pdf