https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.html

[utterances-bot]

Machine Logic

https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.html

[Landraitis]

The popularity of intuitionistic logic in the proof-assistant community has been a source of perplexity to me since I started learning about the subject. If I want to use e.g. Coq to verify that some program or math paper is correct, what do I care about the distinction between bool and Prop? I remember having to fuss about it when doing case analyses in the exercises of Software Foundations. It wasn't just an inconsequential question of taste; it added to the difficulty.

I would really like to see an intuitionistic-type-theory fan make their best affirmative case for the practice of building proof assistants and the standard libraries thereof without assuming excluded middle. Even if one really is skeptical about the consistency of nonconstructive mathematics, that is really a concern about consistency strength rather than LEM: One can choose to work in a classical theory which is constructively provable to be 𝛱⁰₂-conservative over a constructively acceptable theory, for example. Conversely, a given intuitionistic theory may have consistency strength well beyond what is known to be constructively justifiable. (IIUC, this is the case with Coq's type theory.) So I am skeptical that the preference for intuitionistic logic is about consistency. But if not that, what?

[andreasabel]

@Landraitis : The popularity of intuitionistic foundations, esp. Type Theory, is imo owned to the fact that functions are automatically computable there. The type bool is ordinary booleans and you can print any value of type bool and see either true or false in your output. However, Prop is a universe inhabited by types (i.e. propositions under the Curry-Howard correspondence). Elements of Prop are in general not decidable propositions so you cannot print them to see true or false. Forall-quantification thus can only construct a Prop in general, not a bool.

In classical systems like Isabelle/HOL, with functions not being computable, you have to jump through some hoops to extract programs from your developments. Or you keep programs and proofs completely separate, but then you will also end up with two bools: One is the boolean type in your programs, the other the type of propositions in your proof language.

[Landraitis]

@andreasabel So if I understand you correctly, the value proposition, pragmatically speaking, is that programming and proving things about your program can be done in the same language, with no sharp boundary between program and proof? It seems like there's a double trade-off here, where on the proof side you lose excluded middle, and on the programming side you have to use a pure total functional language. But I guess I can see why people would want to explore that approach.

[lawrencecpaulson]

When I first encountered Martin-Löf type theory around 1983, it seemed to offer a coherent, clean route to deductive program synthesis. (Manna and Waldinger had been promoting their own approach to deductive synthesis around that time.) But it soon became clear that you could not get efficient programs from proofs for free: you had to know the algorithm already and structure your proof around it, even if your theorem had a different and much simpler proof. Deductive synthesis seems as far away as ever.

What's really inexplicable is the avoidance of LEM when formalising mathematics. In most cases, this adds complications without realising any recognisable conception of constructive mathematics, for example developing real analysis without LEM but on top of the classical field axioms.

[andreasabel]

@Landraitis wrote:

programming and proving things about your program can be done in the same language, with no sharp boundary between program and proof?

Indeed, this is the main pay-off of Martin-Löf Type Theory (MLTT). The practical relevance of this can be seen when you imagine yourself proving e.g. a sorting algorithm correct. You need the comparison function both in the program (to make the necessary decisions) as well as in the specification (to even say what it means for a structure to be sorted). Thus, you want a common language for programming and proving, so that you do not have to implement comparison twice. This idea, to have a common language for programming and proving, in fact has some repercussions: E.g. you cannot have partial functions, because they lead to inconsistency when used in proofs.

What we in fact would want:

1. A common core vocabulary for programming and proving.
2. An extra vocabulary for just proving (like Prop).
3. An extra vocabulary for efficient programming, partiality etc.

MLTT only delivers 1. We are still trying to figure out canonical ways to deliver the other two. For 2., there is no a priori reason why it should not also allow classical reasoning. For 3., often monads are used (e.g. the Dijkstra monad for working with heap and pointers).

@lawrencecpaulson : Your comment is to the point! From the constructivist point of view, classical mathematics is about negative statements, about impossibilities. Fermat's theorem, which you quote, is about the impossibility of finding 4 numbers n, x, y, z with said properties. There is no constructive content in this statement, so proving it constructively gives no gain (at least on the end product). So from the constructivist point, when a classical mathematician says states that A is true, the constructivist hears them saying that the negation of A is false. So when it is said that A or B is true, it is understood that not both not A and not B can be true. Understanding classical reasoning as refutation reconciles it with the constructivist approach (this is what I learned from Frank Pfenning).

[Landraitis]

I notice that, as of this writing, this comment thread appears under every page of this blog. In case anyone was wondering, my initial comment was in reaction to this post.

[lawrencecpaulson]

Apologies for the chaos in the comments system. I am not sure what caused that but I think I managed to get comments working again. Let's see what happens if somebody comments another post!