Intuitionistic logic

Intuitionistic Logic is the logical branch of Mathematical intuitionism. Roughly speaking, 'intuitionism' holds that logic and math are 'constructive' mental activities. That is, they are not analytic activities wherein deep properties of existence are revealed and applied. Instead, logic and math are the application of internally consistent methods to realize more complex mental constructs (really, a kind of game). In a stricter sense, intuitionistic logic can be investigated as a very concrete and formal kind of mathematical logic. While it may be argued whether such a formal calculus really captures the philosophical aspects of intuitionism, it has properties which are also quite useful from a practical point of view. Both notions of the term will be considered below.

Inuitionistic Logic as a Paradigm for Logical Reasoning

In intuitionistic logic, epistemologically unclear steps in proofs are forbidden; in particular, the law of the excluded middle is not valid because, in a logical calculus that allows it, it's possible to argue P ∨ ¬P without knowing which one specifically is the case. This is fine if one assumes that the law of the excluded middle is some kind of subtle truth inherent in the nature of being; but if the validity of a mental construct is entirely dependent upon its coherence with its context (i.e., the mind), then epistemological opacity is, in effect, cheating.

Intuitionistic logic substitutes justification for truth in its logical calculus. Instead of a deterministic, bivalent truth assignment scheme, it allows for a third, indeterminate truth value. A proposition may be provably justified, or provably not justified, or undetermined. The logical calculus preserves justification, rather than truth, across transformations yielding derived propositions.

Intuitionistic logic gave philosophical support to several schools of philosophy, most notably the Anti-realism of Michael Dummett[?].

Intuitionistic Logic as a Formal Logical Calculus

From a practical point of view, there is also a strong motivation for using intuitionistic logic. Indeed, if one goes for automated reasoning like in logical programming, then one obviously is not interested in mere statements of existence. A computer program is assumed to compute an answer, not to state that there is one. Thus, in applications, one usually looks for a witness for a given existence assertion. In addition, one may have moral concerns about a proof system which has a proof for ∃x P(x), but which fails to prove P(b) for any concrete b it considers.

In order to formalize intuitionistic logic in a mathematically precise way, both a model theory (i.e., semantics) and an appropriate proof theory are needed. The syntax of formulae of intuitionistic logic is similar to propositional logic or first-order logic. The obvious difference is that many tautologies of these classical logics can no longer be proven within intuitionistic logic. Examples include not only the Law of Excluded Middle P∨¬P, but also Pierce's Law[?] ((P→Q)→P)→P.

This observation leads to the idea of weakening the proof theory of classical logic. This has for example been done by Gentzen with his sequent calculus LK, obtaining a weaker version, that he called LJ. This gives a suitable proof theory.

Feel free to add model theory.