Intuitionistic logic

Intuitionistic logic, or constructivist logic, is the symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism. The system preserves justification, rather than truth, across transformations yielding derived propositions. From a practical point of view, there is also a strong motivation for using intuitionistic logic, since it has the existence property, making it also suitable for other forms of mathematical constructivism.

Syntax

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, and even 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 observation that many classically valid tautologies are not theorems of intuitionistic logic leads to the idea of weakening the proof theory of classical logic.

Axiomatization

The inference rule is modus ponens, and axioms are:

THEN-1: φ → (χ → φ)
THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
AND-1: φ ∧ χ → φ
AND-2: φ ∧ χ → χ
AND-3: φ → (χ → (φ ∧ χ))
OR-1: φ → φ ∨ χ
OR-2: χ → φ ∨ χ
OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)
NOT-2: φ → (¬φ → χ)

To make this a system of first-order predicate logic, the rule of generalization is added, along with the axioms:

PRED-1: (∀x Z(x)) → Z(t)
PRED-2: Z(t) → (∃x Z(x))
PRED-3: (∀x (W → Z(x))) → (W → ∀x Z(x))
PRED-4: (∀x (Z(x) → W)) → (∃x Z(x) → W)

Interdefinability of operators

In classical propositional logic, it is possible to take one of conjunction, disjunction, or implication as primitive, and define the other two in terms of it together with negation, such as in Łukasiewicz's three axioms of propositional logic. It is even possible to define all four in terms of a sole sufficient operator such as the Peirce arrow or Sheffer stroke. Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.

These are fundamentally are consequences of the law of bivalence, which makes all such connectives merely boolean functions. The law of bivalence does not hold in intuitionistic logic, only the law of non-contradiction. As a result none of the connectives can be dispensed with, and the above axioms are all necessary. Most of the classical identities are only theorems of inuitionistic logic in one direction, although some are theorems in both directions. They are as follows:

Conjunction versus disjunction:

$(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)$
$(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)$
$(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)$
$(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)$

Conjunction versus implication:

$(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)$
$(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)$
$(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)$
$(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi)$

Disjunction versus implication:

$(\phi \vee \psi) \to (\neg \phi \to \psi)$
$(\neg \phi \vee \psi) \to (\phi \to \psi)$
$\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)$
$\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)$

Universal versus existential quantification:

$(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))$
$(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))$
$(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$
$(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))$

So, for example, "a or b" is a stronger statement than "if not a, then b", whereas these are classicaly interchangeable. On the other hand, "neither a nor b" is equivalent to "not a, and also not b".

Sequent calculus

Gentzen discovered that a relatively simple modification of his system LK results in a system which is sound and complete with respect to intuitionistic logic. He called this system LJ.

Semantics

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.

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.

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.

External links

Stanford Encyclopedia of Philosophy entry

Logic in computer science | Mathematical logic | Mathematical constructivism

Logique intuitionniste | Logica intuizionista | 直觉逻辑

Gourt Home::Gourt :: Intuitionistic logic