|
Intuitionistic logic, or constructivist logic, is the logic used in mathematical
intuitionism and other forms of mathematical
constructivism.
Roughly speaking, 'intuitionism' holds that logic and mathematics are 'constructive' mental activities. That is, they are not
analytic activities wherein deep properties of existence are revealed and applied. Instead, logic and mathematics 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.
Intuitionistic logic as a paradigm for logical reasoning
In intuitionistic logic, epistemologically unclear steps in proofs are forbidden. In classical logic, a formula (say,
A) asserts that A is true in an abstract sense. In intuitionistic logic, a formula is only considered
to be true if it can be proved.
As an example of this difference, law of the excluded
middle, while classically valid, is not intuitionistically 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. In intuitionistic logic, it is not permitted to assert a disjunction such as P ∨ ¬P
without also being able to say specifically which one is true. More generally, the formula P ∨ ¬P is not
a theorem of intuitionistic logic as it is of classical logic. In classical logic, P ∨ ¬P means that one
of P or ¬P is true; in intuitionistic logic, P ∨ ¬P means that one of
P or ¬P can be proved, which is a much stronger statement, and which might not always be the case.
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.
A more familiar example of a classical tautology which is invalid in intuitionistic logic concerns the so-called 'double
negation elimination'. In classical logic, both P → ¬¬P and also ¬¬P → P are
theorems. In intuitionistic logic, only the first is a theorem---double negation can be introduced, but not eliminated. The
interpretation of negation in intuitionistic logic is different from its counterpart in classical logic. In classical logic,
¬P asserts that P is false; in intuitionistic logic, ¬P asserts that a proof of P is
impossible. The asymmetry between the two implications above now becomes apparent. If P is provable, then it is
certainly impossible to prove that there is no proof of P; this is the first implication. But the second implication
fails: just because if there is no proof that a proof of P is impossible, we cannot conclude from this absence that
there is a proof of P.
The observation that many classically valid tautologies are not theorems of intuitionistic logic 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.
The semantics are rather more complicated than for the classical, two-valued case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics.
A valuation on propositional variables can be
given by assigning elements of a Heyting algebra. The valuation can then be extended to formulae by matching the propositional
connectives with their corresponding operations in the algebra. A valid sentence is then one which has valuation 1 in any
valuation on any Heyting algebra.
It can be shown that we need in fact consider only the Heyting algebra given by the open sets of the real plane with its usual
topology - intuitionistic validities correspond precisely to Heyting formulae which evaluate to the entire plane for any
assignment of open subsets to the variables.
For example, the law of the excluded middle can then easily be seen not to be valid - let A be the strict upper plane, {(x,y)
| y > 0}, then ¬A = Int(R^2 \ A) = {(x,y) | y < 0}, the strict lower plane, so A ∨ ¬A = {(x,y) | y!=0} !=
R^2. So we do not have |= P ∨ ¬P in intuistionistic logic.
Kripke semantics
TODO - seem Wikipedia lacks an article on Kripke semantics in general. Feel free to rectify.
See also
|