What are proofs in constructivist logic?

208 Views Asked by At

The difference in syntax between classical and constructivist mathematics is, as far as I've understood, not because constructivists think a well-formed proposition may be untrue and unfalse at the same time. The difference lies in semantics; a constructivist says that mathematical theorems are not proofs, but rather proofs of provability. A constructivist agrees that if you assume a theorem is a proof, then it either proves the statement true, or false. I, a classical mathematician, agree with the constructivist view, IF we view theorems as proofs of provability. I find not accepting LEM as absurd if one views theorems as proofs.

Now, if one is working within a consistent framework, a classical and constructivist theorem that derives a non-negated proposition is, in effect, the same thing. The classical theorem proves the statement is true, and thus not false. The constructivist theorem proves the statement is provable (it can be proven true), and since the framework is consistent, it cannot thus cannot be proven false (LNC).

If one is working within an incomplete framework (which mathematics is, see Gödel), a classical and constructivist theorem deriving a negation does not amount to the same thing. A classical theorem deriving a negated statement proves it; it proves the negation, and thus proves the non-negated statement is false (LEM). A constructivist theorem deriving a negation merely proves that the non-negated statement is not provable. Just because one cannot prove a statement within an incomplete framework, does not mean that statement is false. There are true, yet unprovable statements.

So, assuming my account of this difference between classical and constructivist theorems is true, my following question arises:

If mathematical theorems are merely proofs of provability in constructivist mathematics, what then are proofs? I suspect it has something to do with computation and construction.

1

There are 1 best solutions below

4
On

The difference lies in semantics; a constructivist says that mathematical theorems are not proofs, but rather proofs of provability.

This is not accurate. As far as I know, no one believes that theorems literally are proofs - a theorem is a statement for which there exists a proof, but the theorem is not identical to the proof, and theorems can have many proofs.

Perhaps what you meant is that constructivists view a proof of a theorem merely as a demonstration that the theorem is provable and nothing more. This position is closer to the idea of formalism than constructivism, though the two can overlap. But I don’t want to speculate too much on what you meant since what you said doesn’t make much sense.

A classical theorem deriving a negated statement proves it; it proves the negation, and thus proves the non-negated statement is false (LEM).

LEM has nothing to do with it. In constructive mathematics, any statement which is not true is false. So a constructive proof of a negated statement disproves the non-negated statement. For more elaboration, see my answer here.

A constructivist theorem deriving a negation merely proves that the non-negated statement is not provable.

It is inaccurate, both in constructive and in classical mathematics, to say that a statement is false iff it is unprovable. Gödel’s incompleteness theorems and other related notions like Tarski’s undefinability of truth apply to both constructive and classical theories. Furthermore, any constructive proof of a proposition is also automatically a classical proof of the same proposition. So the idea that a constructive proof “tells us less” about a proposition than a classical proof is wrong; it’s the other way around.

Edit: some systems are classified as “constructive” which are not compatible with LEM. When I say “constructive”, I’m referring to something like constructive first-order logic or IZF, where if we add in LEM, we get the equivalent classical theory. Constructive logic is also compatible with statements that contradict LEM, like the claim that all functions $\mathbb{R} \to \mathbb{R}$ are continuous. A proof using this principle would obviously not be classically valid.