Questions: Introduction to Intuitionistic Logic

Question 1

A mathematician announces: 'Either the Goldbach conjecture is true or it isn't — so we already know one of these is provable.' Why would an intuitionist reject this claim?

• A. Intuitionists reject all disjunctions about unresolved mathematical questions
• B. To assert φ ∨ ψ intuitionistically, you must produce a proof of one specific disjunct — knowing that both being false leads to contradiction is not enough
• C. The claim is valid intuitionistically; intuitionistic logic agrees with classical logic on all tautologies
• D. Intuitionists reject LEM only for empirical statements, not mathematical ones

Answer: (B)

Under the BHK interpretation, a proof of φ ∨ ψ requires either a proof of φ or a proof of ψ, together with a tag indicating which. Simply knowing that ¬(¬φ ∧ ¬ψ) — that both can't be false — does not supply a constructive proof of either disjunct. The classical 'law of excluded middle' φ ∨ ¬φ is not intuitionistically provable for arbitrary φ precisely because we cannot always commit to which side holds. Option B is the key insight of the BHK interpretation.

Question 2

Which statement correctly describes the intuitionistic status of double negation?

• A. Both p → ¬¬p and ¬¬p → p hold intuitionistically, as in classical logic
• B. Neither p → ¬¬p nor ¬¬p → p holds intuitionistically
• C. p → ¬¬p holds but ¬¬p → p fails intuitionistically
• D. ¬¬p → p holds but p → ¬¬p fails intuitionistically

Answer: (C)

p → ¬¬p holds intuitionistically: given a proof of p, construct a function that takes any proof of ¬p (i.e., p → ⊥) and applies it to the proof of p to get ⊥. This is a valid construction. But ¬¬p → p fails: knowing there is no refutation of p does not constructively supply a proof of p. The absence of a counterexample is weaker than the presence of a proof. This asymmetry is definitive of intuitionistic logic.

Question 3

Intuitionistic logic is incomplete — it lacks a completeness theorem analogous to the one for classical logic.

• T. True
• F. False

Answer: False

Intuitionistic logic has its own completeness theorem: it is sound and complete with respect to Kripke semantics (possible-worlds models where each world extends the knowledge at earlier worlds). Confusing 'cannot prove all classical tautologies' with 'is incomplete' is a common error. Intuitionistic logic is complete for its own semantics — it simply validates a different set of formulas than classical logic does.

Question 4

Under the Curry-Howard correspondence, a proof of the formula φ → ψ in intuitionistic natural deduction corresponds to a function of type φ → ψ in simply-typed lambda calculus.

• T. True
• F. False

Answer: True

The Curry-Howard correspondence ('proofs as programs') establishes an isomorphism between intuitionistic proofs and typed programs. A proof of φ → ψ is exactly a function that transforms any proof of φ into a proof of ψ — a term of type φ → ψ. A proof of φ ∧ ψ is a pair; a proof of φ ∨ ψ is a tagged sum type. This is why intuitionistic logic underlies programming language type theory: writing a well-typed terminating program is the same act as constructing an intuitionistic proof.

Question 5

Why does ¬¬p → p fail in intuitionistic logic, even though it is a classical tautology?

Model answer: In intuitionistic logic, ¬¬p means 'there is no proof that p is false' — it is evidence about the absence of a refutation, not a positive construction of p. Classically, because every proposition is either true or false, eliminating ¬p forces p. Intuitionistically, there is a third epistemic state: p may be neither proved nor refuted. To prove p constructively, you must exhibit a proof of p, and the mere impossibility of a refutation does not supply one.

This failure is the sharpest dividing line between classical and intuitionistic logic. Classical logic is bivalent, so ¬¬p collapses to p. Intuitionistic logic operates under the proof-theoretic interpretation that truth means 'there exists a construction,' and absence of refutation is strictly weaker than presence of proof. The Gödel-Gentzen translation embeds classical logic into intuitionistic logic by prepending ¬¬ to formulas, precisely acknowledging that classical truth is intuitionistic double-negation-truth.