We now consider the system NI of natural deduction for intuitionistic propositional logic, for which one can show that it is not complete for validity.

Definition 16 Derivability of a formula A from a (possibly empty) set of assumptions Γ in NI is written Γ fA.

Definition 17 (i) Soundness of NI means: Γ fA =⇒ Γ Fi A.

(ii) Strong completeness of NI means: Γ Fi A =⇒ Γ fA.

(iii) Completeness (simpliciter) of NI means: Γ f-i A =⇒ Γ fA.

Soundness holds. Since derivability Γ fA in NI is closed under substitution, this implies Γ f-i A, that is, intuitionistic validity under substitution. The distinction between strong completeness and completeness (simpliciter) is useful, because one can show that validity is not closed under substitution; the given semantics validates a formula which is not derivable in NI. Thus strong completeness does not hold:

Theorem 5NI is not strongly complete. The set of valid formulas is not closed under substitution.

Three proofs of this result are discussed in [16]. Here we only mention the counterexample (cf. also Goldfarb [8] and Sect. 4)

a → (b ∨ c) F (a → b) ∨ (a → c)

which is already a counterexample for strong completeness of minimal logic, and hence of NI. This counterexample is independent of the level of atomic systems. There are other counterexamples, for which this is not the case. For example, ¬¬a Fi a holds for first-level atomic systems, but fails for atomic systems of levels higher than 1. Thus certain counterexamples in the realm of first-level atomic systems can be avoided by allowing for higher-level atomic systems. What the given counterexample therefore also shows is that strong completeness already fails for the (more standard) notion of validity based on first-level atomic systems.

Strong Completeness Results

Strong completeness holds for the fragment of disjunction-free formulas and for the fragment of arbitrary negative formulas ¬ A (see [16]):

Lemma 5Let Γ and A be disjunction-free. Then Γ Fi A ⇐⇒ Γ fA.

Lemma 6Let Γ and A be disjunction-free. Then Γ F A ⇐⇒ Γ m A,

where f-m denotes derivability in minimal logic. In other words, strong completeness holds for the {→, ∧}-fragment of minimal (and intuitionistic) logic (see SchroederHeister [33]).

Lemma 7For any formula of the form ¬ A it holds that Fi ¬ A ⇐⇒ f¬ A.

These results depend on higher-level atomic systems, for which Lemma 4 holds.

Found a mistake? Please highlight the word and press Shift + Enter