Your continued donations keep Wikipedia running!

Intuitionistic logic

From Wikipedia, the free encyclopedia

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 debated whether such a formal calculus really captures the philosophical aspects of intuitionism, it has properties which are quite useful from a practical point of view.

Both notions of the term will be considered below.

[edit]

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 intuitionistic logic a formula is only considered to be true if it can be proved. As an example of this difference consider the law of excluded middle. Accepted by classical logic, the law is not accepted by intuitionistic logic because, in a language that allows the formula, it is possible to draw the conclusion that P ∨ ¬P without knowing which of the disjuncts is true. In effect, in intuitionistic logic, P ∨ ¬P says that at least one of P or ¬P can be proved, which is stronger than saying that their disjunction is true.

The thought behind this is that the validity of a mental construct is dependent upon its coherence with its context (the mind). From this perspective, epistemological opacity is, in effect, cheating.

Intuitionistic logic substitutes justification for truth in its logical calculus. The logical calculus preserves justification, rather than truth, across transformations yielding derived propositions.

Intuitionistic logic has given philosophical support to several schools of philosophy, most notably the Anti-realism of Michael Dummett.

[edit]

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 logic 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 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 (by semantics) and an appropriate proof theory are needed. The syntax of formulæ 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 Peirce'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 it cannot be 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 P is refutable (i.e., that there is a proof that there is no proof of P). 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. However, the second implication fails: Just because there is no proof that there is no proof of P, we cannot conclude from this absence that there is a proof of P. A weaker version of double negation elimination is provable such that ¬¬¬P → ¬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, deterministic case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics.

[edit]

Heyting algebra semantics

In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Then we have the useful theorem that a formula is a valid sentence of classical logic if and only if its value is 1 for every valuation---that is, for any assignment of values to its variables.

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from a Heyting algebra, of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open sets of the real plane R². In this algebra, The ∧ and ∨ operations correspond to set intersection and union, and the value assigned to a formula A→B is (A^C ∪ B)°, the interior of the union of the value of B and the complement of the value of A. The bottom element ø is the empty set, and the top element is the entire plane R². Negation is as usual defined as ¬A = A→ø, so the value of ¬A reduces to A^C°, the interior of the complement of the value of A. With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire plane.

For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be the entire plane:

Value(¬(A ∧ ¬A)) =

(Value(A ∧ ¬A))^C° =

(Value(A) ∩ Value(¬A))^C° =

(X ∩ (Value(A))^C°)^C° =

(X ∩ X^C°)^C°

A theorem of topology tells us that X^C° is a subset of X^C, so the intersection is empty, leaving:

ø^C° = (R²)° = R²

So the valuation of this formula is true, and indeed the formula is valid.

But the law of the excluded middle, A∨¬A, can be shown to be invalid by letting the value of A be {y : y > 0 }. Then the value of ¬A is the interior of {y : y ≤ 0 }, which is {y : y < 0 }, and the value of the formula is the union of {y : y > 0 } and {y : y < 0 }, which is {y : y ≠ 0 }, not the entire plane.

The infinite Heyting algebra described above gives a true valuation to all intuitionistically valid formulas, regardless of what values are assigned to the variables in a formula. Conversely, for every invalid formula, there is an assignment of values from this algebra to the variables that yields a false valuation for the formula. It can be shown that no finite Heyting algebra has this property.

[edit]

Kripke semantics

Main article: Kripke semantics

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.

[edit]