I'm incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I'm going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some cleanups and rewrites, so this won't be identical to the original posts.
I've written about logic before, and mentioned intuitionistic logic at least in passing. Intuitionistic logic is an interesting subject. Intuitionistic logic is a variation of predicate logic which is built on the idea that there should be a stronger notion of "truth" in logic: that the strict categorization of all statements in classical logic as either true or false is too strong. In intuitionistic logic, a statement is only true if you can prove that it is true. It is not enough to prove that it's opposite is false: In propositional logic, it is not the case that ¬¬P→P.
In fact, truth is intuitionistic logic is defined by proof: A is true means that there exists a proof of A. A is false means that there is a proof that there is no proof of A. Most of the differences between intuitionistic and classical logic comes from that distinction between the classical meaning of true and false, and the intuitionistic meaning of true and false.
The intuitionistic meaning has the implication that many inferences that we're used to in propositional logic are no longer valid in intuitionistic logic:
- In classical propositional logic, the statement "X∨¬X" is a tautology, which says that either X is true, or X is not true. In intuitionistic logic, it is not: the statement "X∨¬X" means that we can prove that either X is true or 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∨¬X" is not a true statement: it's possible that X is true, but we don't have a proof for it.
- In classical predicate logic, we can often infer statements like "∃ 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. Intuitionistic logic is always constructive: proofs always generate concrete examples.
- In both propositional and intuitionistic logic, the statement that "P→¬¬P" is true. But in classical logic, "¬¬P -> P" is always true, but in intuitionistic logic, it is not. We can introduce double negation, but we can't eliminate it: 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 "¬¬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. In intuitionistic logic, 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, then it becomes false.
It's worth reiterating: one of the really wonderful properties of intuitionistic logic is that it's strongly constructionist. A proof that "¬A" in intuitionistic logic will always generate at least one concrete counterexample of A. There are entire programming languages built on this fundamental point. (Not to get too far off topic, but a prolog program basically works by negating a statement for which you want concrete examples, and then using intuitionistic inference to generate counterexamples for that negative - which are concrete examples of where the statement is true.)
The formal semantics of intuitionistic logic are more complicated than the semantics of predicate logic. They tend to involve things like lattice theory. In my next 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, model checking - and providing models for many of the calculi that fascinate me. Kripke semantics provide the definitive model for λ-calculus, and by extension, for other fascinating calculi like the π-calculus.