Logic Fun: Intuitionistic Logic

It's time for a bit of a side-track from the series of articles about lambda calculus. Models of lambda calculus are based on something called intuitionistic logic, so I'm going to write a bit about that. It's also quite interesting in its own right.

Syntactically, intuitionistic logic looks the same as first order predicate logic. But the meanings of statements in it are often quite different. The basic idea behind intuitionistic logic is that some of the statements that you can make in propositional logic are too strong. In intuitionistic logic, a statement is only true if there is a proof that it is true; a statement that something is false means that that statement cannot be proved - so the negative statement "not P" can be read as an affirmative statement: "There is a proof that there is no proof for P".

This has the implication that many inferences that we're used to in propositional logic are not accepted in intuitionistic logic:

• In propositional logic, the statement "X or not X" is a tautology, that is a statement that is always true: the statement means that either X is true, or X is not true. In intuitionistic logic, it is not: the statement "X or not X" means that we can prove that X is true or we can prove that X is false. X is true in intuitionistic logic if and only if we have a proof that X is true; X is false if and only if we can prove that there is no proof for X. If we do not have a proof for either the truth or the falsehood of X, then "X or not X" is not a true statement: it's possible that X is true, but we don't have a proof for it.
  
• In propositional logic, we can often infer statements like "exists X : P(x)", even though we don't know what x is. In intuitionistic logic, to infer that statement, it must be possible to demonstrate at least one value for which it's true. Similarly, in order to prove that a universal statement is false, we need to be able to show a concrete counterexample that demonstrates its falsehood.
  
• In both propositional and intuitionistic logic, the statement that "P -> not not P" is true. But in intuitionistic logic, "not not P -> P" is not true. Since "not P" means "We can prove that there is no proof of P", the fact that P is true (i.e., that we have a proof that P is true) means that we can prove that "not P" is false - because the fact that there is a proof for P provides a concrete counterexample to the statement that there is no proof for P - so "not not P", which says "There is no proof that there is no proof for P" is proven true.
  
  But going the other direction: the fact that we can't prove that there is no proof for P does not imply that there is a proof for P. Being unable to prove that there is no proof for something is a much weaker statement that saying that that thing is true.
  

One way to think of intuitionistic logic is to think of it as if there were actually three values that can be assigned to a predicate: it can be in one of two definite states (proved true or proved false) or it can be in an indefinite state (unproven). If a predicate P is unproven, then we can assert neither that P is true nor that P is false. But if the predicate is in an indefinite state, and we can show a proof, then we can move it to a definite state: if we can find a way to provide a proof of P, then it becomes true; or if we can show that it's unprovable (generally through a counterexample), then it becomes false.

The formal semantics of intuitionistic logic are more complicated than the semantics of predicate logic. They tend to involve things like lattice theory. In another post, I'll talk about one way of describing the semantics of intuitionistic logic called Kripke Semantics. Kripke semantics is useful not just for intuitionistic logic, but for a lot of other things, like temporal logics, modal logics, and model checking. (Wikipedia describes another version of the semantics of intuitionistic model based on something called Heyting Algebra, but I'm not familiar with it.)