Dummett [3, Chaps. 11–13] made an approach to proof-theoretic validity for inference rules (or arguments) which is similar to Prawitz's (cf. Sect. 2). It is supposed to yield a justification of intuitionistic first-order logic. Goldfarb [8] (this volume) has given an analysis of the propositional part of Dummett's approach, resulting in a notion of validity for formulas (instead of inference rules).

Goldfarb first gives a formulation for atomic systems of axioms only, that is, for sets of atoms. It is presumed that there are infinitely many atoms available and that only finite sets of atoms α, β are ever considered. We follow his notation in writing α, β for such sets but adjust it to ours otherwise:

Definition 7

(G1) α F a :⇐⇒ a ∈ α,

(G2) α F A → B :⇐⇒ ∀β ⊇ α : (β F A =⇒ β F B),

(G3) α F A ∨ B :⇐⇒ α F A or α F B,

(G4) α F A ∧ B :⇐⇒ α F A and α F B,

(G5) There is no α such that α F ⊥.

This notion of validity (F) can be discarded right away, since it validates formulas which are not even derivable in classical logic (see Goldfarb [8]):

Lemma 1(i) Suppose A does not contain ⊥. Then α F ( A → ⊥) → ⊥.

(ii) Let a and b be two distinct atoms. Then α F (a → b) → b.

Goldfarb then modifies this notion of validity by relativizing the relation F to proper first-level atomic systems S (i.e., in Dummett's terminology, to sets of boundary rules) as in Dummett's approach. He points out that in order to avoid cases like Lemma 1 (i), atomic rules with conclusion ⊥ have to be allowed as well. The modified notion can be given by rewriting clauses (G1)–(G5) with FS instead of F, together with the condition that sets α, β have now to be closed under the rules in S and do not contain ⊥:

Definition 8 Let S be a proper first-level atomic system. Let the sets α, β be closed under the rules in S, and ⊥ ∈/ α, β.

(G1t) α FS a :⇐⇒ a ∈ α,

(G2t) α FS A → B :⇐⇒ ∀β ⊇ α : (β FS A =⇒ β FS B),

(G3t) α FS A ∨ B :⇐⇒ α FS A or α FS B,

(G4t) α FS A ∧ B :⇐⇒ α FS A and α FS B,

(G5t) There is no α such that α FS ⊥.

According to Goldfarb, this notion of validity is a revision of Dummett's approach in that it considers in principle all atomic systems S instead of only a fixed one.

For this revised notion of validity all valid formulas are classically valid. Completeness for intuitionistic logic does not hold (see Goldfarb [8]):

Lemma 2(i) Every valid formula is derivable in classical logic.

(ii) The formula (a → (B ∨ C)) → ((a → B) ∨ (a → C)) is valid for any atom a and any formulas B and C, but it is not intuitionistically derivable for all B, C.

The counterexamples to completeness given in Lemmas 1 and 2 are not schematic in the sense that all substitution instances of the valid formulas presented there are valid too. Goldfarb introduces the relation of schematic validity, which holds for a formula A if and only if all instances of A resulting from uniform substitutions of formulas for atoms in A are valid (cp. substitution-Kreisel-validity). He shows that the intuitionistically non-derivable formula ¬ A ∨ ¬¬ A is schematically valid for atomic systems which do only contain atoms (i.e., for atomic systems of level 0). In other words:

Theorem 3 (Goldfarb [8]) Intuitionistic logic is not complete for schematic validity for sets of atoms α (i.e., for the notion of schematic validity based on validity (F) according to Definition 7).

However, for the schematically understood revised notion of validity the following completeness result holds:

Theorem 4 (Goldfarb [8]) Intuitionistic propositional logic is complete for schematic validity based on the revised notion of validity (i.e., for the notion of schematic validity based on validity (FS ) according to Definition 8).

We note that this completeness result depends on the restriction to consistent sets of atoms α, β in the sense that ⊥ ∈/ α, β. A restriction to consistent extensions is also made in Definition 6 of (substitution-) Kreisel validity, namely in clause (K5) for negation. If negation is understood as ¬ A := A → ⊥, and ⊥ is explained by α FS ⊥ :⇐⇒ ∀a : α FS a, then

α FS ¬ A ⇐⇒ ∀β ⊇ α : β 'FS A.

Since α, β are consistent, this is equivalent to clause (K5), where ⊥ is a word w such that J.St w. However, in the case of (substitution-) Kreisel validity this is the only clause where a restriction to consistent atomic systems (resp. Post systems) S, St is made, whereas such a restriction applies in general in the case of (schematic) validity according to Definition 8. Assuming consistent extensions in general also in the case of Kreisel validity implies completeness for substitution-Kreisel-validity. That is, Conjecture 2 is decided positively in this case.

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