Intuitionistic Logic

Abstract

So far our logics have satisfied the principle of excluded middle (PEM): any statement φ is true or its negation is true, in formula: φ∨¬φ is true. To take an example: “Euler’s constant is rational or irrational”. This kind of statement is not useful at all, it gives no clue to the real question: “Oh yeah, which one is it then?”. What one needs is an effective logic, which will pick from the disjunction φ∨¬φ the correct one, and which will produce a number n with φ(n) as soon as ∃xφ(x) is established. It is most gratifying that such a logic exists; it goes back to Brouwer, and it is called intuitionistic logic. The proof technique for this logic is the same as for the old one, in that the reductio ad absurdum rule is dropped. Of course one has to change the semantics, but this is no problem; there are several options. In the present chapter Kripke semantics is chosen, a possible worlds semantics. A modification of Henkin’s completeness proof shows that “intuitionistic derivable = true in all Kripke models”. A number of meta-mathematical principles are proved, e.g. the disjunction property: if you can prove φ∨ψ, then you can prove ϕ or ψ; the existence property: if you can prove ∃xφ(x) in intuitionistic arithmetic, then you can find a natural number n and a proof of φ(n); there are derivability-preserving translations of classical propositional and predicate logic into intuitionistic logic (the Glivenko and Gödel translations).