Intuitionistic Logic
01 Oct 2015Intuitionistic logic rejects the law of excluded-middle(¬A ∨ A, LEM) or equivalently double-negation elimination(¬¬A → A, DNE) in classic logic (see appendix for proof of equivalence). The law of excluded middle is usually justified by the principle of bivalence, i.e. a proposition is either true or false.
- Background
- Syntax
- Proof System
- Semantics
- Relationship with Classic Logic
- Equivalence of DNE and LEM
- Reference
Background
Intuitionistic logic only admits constructive proofs. One justification for intuitionistic logic is that not all mathematical propositions have a proof provided that the system is consistent, as Gödel’s incompleteness theorem tells us. Later development of intuitionistic logic was mainly due to Andrei Kolmogorov and Martin Löf.
One consequence of intuitionistic logic is that the widely used proof technique Reductio ad absurdum becomes invalid, as ¬¬A → A is no longer a tautology, we can’t assert A from ¬¬A. Also, following classical tautologies are no longer valid in intuitionistic logic:
¬∀x ¬A(x) → ∃xA(x)
¬∀xA(x) → ∃x¬A(x)
In this article, I only talk about intuitionistic first-order predicate logic. All logical systems have three components: syntax, proof system and semantics. I’ll explain each part of intuitionistic logic in detail below.
For those interested, the lecture notes by Martin Löf On the Meanings of the Logical Constants and the Justification of the Logical Laws is a must read in intuitionistic logic.
Syntax
Syntactically, classic logic and intuitionistic logic have no difference. The well-formed formulas are defined inductively as follows:
- Each prime formula is a formula.
- If A and B are formulas, so are (A ∧ B), (A ∨ B), (A → B) and ¬A.
- If A is a formula and x is a variable, then ∀xA and ∃xA are formula.
The prime formulas are expressions such as P, Q(a), R(a, b, a) where P, Q(.), R(…) are 0-ary, 1-ary and 3-ary predicate letters respectively.
Proof System
There are a lot of proof systems: Hilbert-style system, natural deduction, sequent calculus, tableau method, etc. Two important properties of a proof system are soundness and completeness. Soundness means all provable propositions are theorems, completeness means all theorems are provable.
Here we only concern us with Hilbert-style system and natural deduction.
Hilbert-style System
Hilbert-style systems have very few inference rules(usually only Modus Ponens), but a lot of axiom schemes. For a given logical system, there exist many possible formulations of inference rules and axiom schemes. In the following one possible formulation is presented.
Inference rules in the system:
- Modus Ponens: From A and A → B, conclude B.
- ∀-Introduction: From Γ ⊢ A(y) we can conclude Γ ⊢ ∀xA(x) , where (1) y doesn’t occur free in Γ, (2) x doesn’t occur in A.
- ∃-Elimination: From Γ ⊢ ∃xA(x) we can conclude Γ ⊢ A(t), where t is a new variable which does not occur free in Γ.
Axiom schemes in the system:
- A → (B → A)
- (A → B) → ((A → (B → C)) → (A → C))
- A → (B → (A ∧ B))
- (A ∧ B) → A
- (A ∧ B) → B
- A → (A ∨ B)
- B → (A ∨ B)
- (A → C) → ((B → C) → ((A ∨ B) → C))
- (A → B) → ((A → ¬B) → ¬A)
- ¬A → (A → B)
- ∀xA(x) → A(t)
- A(t) → ∃xA(x)
Classic predicate logic can be seen as the augmentation of intuitionistic logic with LEM(¬A ∨ A) or LDN(¬¬A → A).
Natural Deduction
In natural deduction systems, there are only inference rules.
φ Θ φ ∧ Θ φ ∧ Θ
------------- (∧I) ------------- (∧E) ------------ (∧E)
φ ∧ Θ Θ φ
Θ ψ
. .
. .
. .
φ Θ Θ ∨ ψ φ φ
------------- (∨I) ------------ (∨I) ------------------------ (∨E)
φ ∨ Θ φ ∨ Θ φ
θ
.
.
.
ψ θ → ψ θ
------------ (→I) ----------------------- (→E)
θ → ψ ψ
θ
.
.
.
⊥ θ ¬θ
------------ (¬I) ------------------------ (¬E)
¬θ ⊥
x0 fresh, θ(x0/x) ∀xθ
------------------- (∀I) ------------------------ (∀E)
∀xθ θ(t/x)
x0 fresh, θ(x0/x)
.
.
.
θ(t/x) ∃xθ φ
------------------- (∃I) ------------------------ (∃E)
∃xθ φ
⊥
----------- (⊥E, ex falso quodlibet)
Θ
Classic predicate logic augments the inference rules with double negation elimination(DNE) or law of excluded middle(LEM):
Γ ⊢ ¬¬Θ
-------- (DNE) ----------- (LEM)
Γ ⊢ Θ Γ ⊢ ¬Θ ∨ Θ
Note that in classic predicate logic, there’s no need for an explicit rule of ex falso quodlibet – also called principle of explosion(from contradiction everything follows), as it can be proved as follows:
1 P ∧ ¬P Premise
2 P Conjunctive Elimination from 1
3 P ∨ A Weakening from 2
4 ¬P Conjunctive Elimination from 1
5 A Disjunctive Syllogism from 3 and 4
Para-consistent logic rejects the principle of explosion in order to achieve better expressiveness. Disjunctive Syllogism is usually sacrificed for the purpose.
First-order logic is augmentation of predicate logic with identity:
t1 = t2 φ(t1/x)
------------ (=i) ----------------------- (=E)
θ = θ φ(t2/x)
Semantics
There are many interpretations of intuitionistic logic, e.g. Kripke models, Heyting algebras, BHK-interpretation, etc. Here I only talk about BHK-interpretation, which is named after Brouwer, Heyting and Kolmogorov.
The BHK-interpretation of intuitionistic logic is based on the notion of proof or verification instead of truth. Note that proof here doesn’t mean logical proof, but some kind of evidence or verification. The BHK-interpretation was independently given by Kolmogorov and Heyting, with Kolmogorov’s formulation in terms of the solution of problems rather than in terms of executing proofs.
According to Martin Löf, intuitionistic logicians make the difference between propositions and judgments(or assertions). Propositions only state facts, but judgments assert them. For example, it is raining is a proposition, “it is raining” is a proposition or “it is raining” is true are judgments. What proofs concern are no longer propositions, but judgments. So the inference rules should be written as following:
A true A
---------- instead of -------
A ∨ B true A ∨ B
Regarding the nature of inference and hypothetical judgment, Martin Löf advocates that:
An inference is a proof of a logical consequence(i.e. hypothetical judgment). Thus an inference is the same as a hypothetical proof.
Note that hypothetical judgment is more general than implication. The concept of implication depends on hypothetical judgement and hypothetical proof. In classic logic, material implication A → B is often interpreted as ¬A ∨ B. In intuitionistic logic, the judgment A → B true can be verified by the hypothetical proof of B true assuming A true, and for verificationists the meaning of A → B is the verification of A → B true.
Following list is the semantic version of the inference rules, which Martin Löf gave a detailed justification in the lecture node I mentioned above:
- A proof of φ ∧ ψ consists of a proof of φ and a proof of ψ.
- A proof of φ ∨ ψ consists of a proof of φ or a proof of ψ,
- A proof of φ → ψ consists of a method of converting any proof of φ into a proof of ψ, e.g. the identity function is a proof of A → A,
- No proof of ⊥ exists,
- A proof of ∃xφ(x) consists of a name d of an object constructed in the intended domain of discourse plus a proof of φ(d),
- A proof of ∀x φ(x) consists of a method that for any object d constructed in the intended domain of discourse produces a proof of φ(d).
- The formula ¬P is defined as P → ⊥, so a proof of it is a function f that converts a proof of P into a proof of ⊥.
- There is no proof of ⊥ (the absurdity).
Relationship with Classic Logic
As it’s mentioned earlier, intuitionistic logic is a restriction of classic logic, all valid reasonings in intuitionistic logic are also valid in classic logic, but not vice versa. Does it mean intuitionistic logic is weaker?
Using a technique called double-negation translation, first proved by Glivenko, it’s possible to embed classic propositional logic inside intuitionistic propositional logic. The theorem says that
if Γ proves φ in classic propositional logic if and only if Γ proves ¬¬φ in intuitionistic propositional logic.
This result can be extended to predicate logic through following transformation:
- g(P) is ¬¬ P, if P is prime.
- g(A & B) is (g(A) & g(B)).
- g(A ∨ B) is ¬ (¬g(A) & ¬g(B)).
- g(A → B) is (g(A) → g(B)).
- g(¬A) is ¬ g(A).
- g(∀xA(x)) is ∀x g(A(x)).
- g(∃xA(x)) is ¬∀x¬g(A(x)).
The theorem states that:
For each formula A, g(A) is provable intuitionistically if and only if A is provable classically
From this perspective, intuitionistic logic is not weaker at all.
Equivalence of DNE and LEM
To get some taste in proof in natural deduction, let’s prove IL + DNE and IL + LEM are equivalent.
(1) Assume IL + LEM, prove DNE: ¬¬A → A.
------- v -------- t
¬A true ¬¬A true
-------------------- →E
⊥
------ u --------- s -------------------- ⊥E
A true ¬¬A true A
----------- LEM ------------------- →I(s) -------------------- →I(t)
A ∨ ¬A true ¬¬A → A true ¬¬A → A true
------------------------------------------------------------------ ∨E(u, v)
¬¬A → A true
(2) Assume IL + DNE, prove LEM: A ∨ ¬A
------ w
A true
--------------- u ------------ ∨I
¬(A ∨ ¬A) true A ∨ ¬A true
-------------------------------------- →E
⊥
--------------- →I(w)
¬A true
--------------- ∨I --------------- u
A ∨ ¬A true ¬(A ∨ ¬A) true
-------------------------------------- →E
⊥
--------------- →I(u)
¬¬(A ∨ ¬A) true
--------------- DNE
A ∨ ¬A true
Reference
- On the Meanings of the Logical Constants and the Justification of the Logical Laws by Martin Löf
- Intuitionistic Logic Development Standford Philosophy Encyclopedia
- Intuitionistic Logic Standford Philosophy Encyclopedia
- Lecture Notes Carnegie Mellon University