When does (or should) Theoretical CS care about intuitionistic proofs?

Question

From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the approach requires us to take seriously the consequences of computation on logic and provability. A proof cannot exist unless there exists an algorithm constructing the consequences from the hypotheses. We might reject as an axiom the principle of the excluded middle, for instance, because it exhibits some object, which is either $X$ or $\lnot X$, nonconstructively.

The above philosophy might lead us to prefer intuitionistically valid proofs over ones that are not. However, I have not seen any concern about actually using intuitionistic logic in papers in other areas of theoretical CS. We seem happy to prove our results using classical logic. For example, one might imagine using the principle of the excluded middle to prove that an algorithm is correct. In other words, we care about and take seriously a computationally-limited universe in our results, but not necessarily in our proofs of these results.

1. Are researchers in theoretical CS ever concerned about writing intuitionistically valid proofs? I could easily imagine a subfield of theoretical computer science that seeks to understand when TCS results, especially algorithmic ones, hold in intuitionistic logic (or more interestingly, when they don't). But I have not yet come across any.

2. Is there any philosophical argument that they should? It seems like one could claim that computer science results ought to be proven intuitionistically when possible, and we ought to know which results require e.g. PEM. Has anyone tried to make such an argument? Or perhaps there is a consensus that this question is just not very important?

3. As a side question, I am curious to know examples of cases where this actually matters: Are there important TCS results known to hold in classical logic but not in intuitionistic logic? Or suspected not to hold in intuitionistic logic.

Apologies for the softness of the question! It may require rewording or reinterpretation after hearing from the experts.

Answer 1

As I said in the comments, intuitionist logic is not the main point. The more important point is having a constructive proof. I think Martin-Löf's type theory is much more relevant to programming language theory than intuitionistic logic and there are experts who have argued that Martin-Löf's work is the main reason for the revival of the general interest in constructive mathematics.

The computability interpretation of constructiveness is one possible perspective, but it is not the only one. We should be careful here when we want to compare constructive proofs to classical proofs. Although both might use the same symbols, what they mean by those symbols are different.

It is always good to remember that classical proofs can be translated to intuitionistic proofs. In other words, in a sense, classical logic is a subsystem of intuitionistic logic. Therefore you can realize (say using computable functions) classical proofs in a sense. On the other hand, we can think of constructive mathematics as some mathematical system in classical setting.

At the end, formalisms, whether classical or constructive, are tools for us to express statements. Taking a classical theorem and trying to prove it constructively without this perspective doesn't make much sense IMHO. When I say $A \lor B$ classically I mean something different from what I say $A \lor B$ constructively. You can argue what "should" be the real meaning of "$\lor$" but I think that is not interesting if we are not discussing what we want to express in the first place. Do we mean (at least) one of them holds and we know which one? Or do we simply mean one of them holds?

Now, with this perspective, if we want to prove a statement like $\forall x \ \exists y \ \varphi(x,y)$ and we want to relate this to a mapping from $x$ to some $y$ satisfying $\varphi(x,y)$ then the better way to express can be the constructive way. On the other hand, if we only care about the existence of $y$ and do not care about how to find them then the classical way would probably make more sense. When you prove the statement constructively, you are also implicitly building an algorithm for finding $y$ from $x$. You can do the same thing explicitly with a more complicate formula like "the algorithm $A$ has the property that for all $x$, $\varphi(x,A(x))$" where $A$ is some explicitly given algorithm. If it is not clear why one may prefer the constructive way to express this, think about programming languages as an analogy: you can write a program for the Kruskal's MST algorithm in x86 assembly language where you have to care about lots of side issues or you can write a program in Python.

Now why we don't use intuitionist logic in practice? There are several reasons. For example, most of us are not trained with that mind setting. Also finding a classical proof of a statement might be much easier than finding a constructive proof of it. Or we might care about low-level details which are hidden and not accessible in a constructive setting (see also linear logic). Or we might simply be uninterested in getting the extra stuff that comes with a constructive proof. And although there are tools to extract programs from proofs these tools generally need very detailed proofs and haven't been user-friendly enough for the general theorist. In short, too much pain for too little benefit.

Here is one possible reason why we don't see much constructive proofs in theory A: our theorems in theory A are often $\Pi^0_2$ statements and are proven using not very strong theories (say they are provable in $PA$) and by a meta-theorem all of them are also provable constructively (in the constructive counterpart of $PA$). In fact, many theory A results can be proven in theories much weaker than $PA$.

I remember that Douglas S. Bridges in the introduction to his computability theory book argued that we should prove our results constructively. He gives an example which IIRC is essentially as follows:

Assume that you work for a big software company and your manager asks you for a program to solve a problem. Would it be acceptable to return with two programs and tell your manager one of these two solves correctly but I don't know which one?

At end, we should keep in mind that although we use the same symbols for classical and intuitionistic logics these symbols have different meanings, and the one to use depends on what we want to express.

For your last question, I think Robertson–Seymour theorem would be an example of a theorem that we know it is true classically but we don't have any constructive proof of it. See also

• Are there non-constructive algorithm existence proofs?

Answer 2

It is is worth thinking about WHY intuistionistic logic is the natural logic for computation, since all too often people get lost in the technical details and fail to grasp the essence of the issue.

Very simply, classical logic is a logic of perfect information: all statements within the system are assumed to be known or knowable as unambiguously true or false.

Intuistionistic logic, on the other hand, has room for statements with unknown and unknowable truth values. This is essential for computation, since, thanks to the undecidability of termination in the general case, it will not always be certain what the truth value of some statements will be, or even whether or not a truth value can ever be assigned to certain statements.

Beyond this, it turns out that even in strongly normalizing environments, where termination is always guaranteed, classical logic is still problematic, since double negation elimination $\neg\neg P \implies P$ ultimately boils down to being able to pull a value "out of thin air" rather than directly computing it.

In my opinion, these "semantic" reasons are a much more important motivation for the use of intuistionistic logic for computation than any other technical reasons one could marshal.

Answer 3

Real-world cryptographic hash functions like MD5 & SHA are keyless. As such, it makes it quite difficult to apply techniques from theoretical cryptography to reason about their security. The simple reason why: for any keyless hash function, there exists a very small program/adversary which outputs a collision under that hash function; namely, a program that has such a collision -- which must exist! -- hard-coded.

Phil Rogaway's paper Formalizing Human Ignorance: Collision-Resistant Hashing without the Keys deals with this problem. In it he shows that some very standard theorems for keyed hash functions (like the Merkle-Damgård construction & hash-then-sign paradigm) can be adapted and re-proven with "intuitionist-friendly" theorem statements applying to unkeyed hash functions.

Answer 4

here is a nice chapter on Intuitionistic Logic from a comprehensive online book Logic for Computer Science, 300pp.[1] sec 9.5, p210, summary on p220:

Intuitionistic logic arose out of the constructivist movement in mathematics which rejected non-constructive existence proofs or those based on the law of the excluded middle. Recently a connection between intuitionistic mathematics and programming has come out of the observation that propositions and types (in the programming sense) are equivalent. Algorithm development in this formal system, which is based on natural deduction, consists of writing a specification in logical notation and then, considering this as a type, proving that it is non-empty. Because the underlying logic is constructive the proof, if it can be carried out, must embody the explicit construction of an object of the appropriate type.

another nearby perspective comes from TCSist Andrej Bauer writing on "Mathematics and computation; mathematics for computers"[2] who proposes basically that "intuitionistic mathematics is good for physics". the presentation is mainly in terms of physics, but for those who consider CS tightly coupled with physics the ideology will generally carry to TCS.

Computational interpretation. This is the interpretation of intuitionistic logic commonly presented in computer science. We view all sets as represented by suitable data structures—a reasonable point of view for a computer scientist. Then a statement is taken to be true if there exists a program (computational evidence) witnessing its truth.

[1] Logic for Computer Science, Reeves and Clark

[2] Intuitionistic mathematics for physics Bauer