The counterexamples I have presented are not schematic inferences, that is, inferences that rely only on the forms of the premises and conclusion. The inferences that I showed to be valid-by-Dummett's lights (although not valid in any ordinary sense) were further constrained, e.g., in Counterexample 2 the formulas could have no atomic constituent in common, and in Counterexample 3 the antecedent had to be atomic.
The question naturally arises as to how Dummett's definitions fare on schematic inferences. Let us call an inference schematically valid in Dummett's original sense iff the inference and all its instances are valid in Dummett's original sense. (An instance is simply any inference obtained from the original one by replacing atomic sentences with other sentences.)
Now any inference that is schematically valid is classically valid, since if F does not imply G in the classical sense, a truth-assignment T that makes F true and G false can be mimicked by the substitution instances of F and G in which sentence letters assigned truth by T are replaced with “ p → p” and those assigned falsity are
replaced with “⊥”. The resulting instances F ∗ and G∗ are such that ∅ fF ∗ but not
∅ fG∗ (since forcing will then just amount to two-valued truth-computation).
However, schematic validity outstrips intuitionistic logic.
Counterexample 45 The inference from no premise to ¬F ∨ ¬¬F is schematically valid (that is, for any F the inference from no premise to ¬F ∨ ¬¬F is valid in Dummett's original sense).
Proof If not α f¬F , then there exists β such that α ⊆ β and β fF . But then, for any γ such that α ⊆ γ , there exists δ such that γ ⊆ δ and δ fF , namely, δ = γ ∪ β. Thus, for any γ such that α ⊆ γ , not γ f¬F . That is, α f¬¬F . D
However, we can obtain a positive result if we combine the notion of schematic inference with that of validity-in-the-revised-sense, that is, validity given any collection of boundary rules. That is, it is possible to prove the following:
Theorem If every instance of the inference from F to G is valid in the revised sense, then the inference from F to G is intuitionistically valid.
For the proof, see the Appendix.
Dummett can't take too much comfort in this positive result. Dummett is careful to point out, in framing his method, that the inferences treated are actual inferences, involving particular meaningful sentences, the atomic components of which are actual atomic sentences, not schematic parts [3, p. 254]. That is, he treats the language as fully interpreted. On the view he is propounding, an inference is justified by its validity; the justification of a schematic inference (an inference rule) can lie only in the fact that each of its instances is justified. There is simply no room, on his view, for a position to the effect that validity does not justify an inference unless all inferences like it in being subsumable under a particular rule are also justified.
Let us return to Counterexample 3. Intuitionistically, the inference from A →
(G ∨ H ) to ( A → G) ∨ ( A → H ) is incorrect, because the former means “any
demonstration of A can be transformed either into one for G or into one for H ” whereas the latter means “any demonstration of A can be transformed into one for G or any demonstration of A can be transformed into one for H .” This inference turns out to be valid, in the revised sense, because—so to speak—the method treats an atomic formula as its own proof. That is, the criterion of the identity of a proof is just the atomic formulas it has as premises or are implied by its premises. Thus distinct ways of proving an atomic A will not register as distinct. Now this view of proofs arises because the whole set-up envisages all proofs as, ultimately from atomic formulas. And this is the upshot of the set-up's being part of, or the beginnings of, a verificationist meaning-theory.
I believe the basic views that lead to Dummett's difficulties are well exhibited in the following remark (he is speaking here only of mathematics, but presumably he would maintain the same for a language with empirical vocabulary as well):
If the intuitionistic explanations of the logical constants and, more generally, of the meanings of mathematical statements are to be considered as constituting a coherent theory of meaning for the language of mathematics, then the notion of proof which is appealed to must be such that we can fully grasp the concept of a proof of any constituent of a given sentence in advance of grasping that of a proof of that sentence. It cannot, therefore, be identified with the notion of the sort of proof that we may, at some future time, come to consider valid . . . [2, p. 402]
This remark expresses a fundamental view of Dummett's; and from it we can see three sources of the problems with his program for “proof-theoretic justification”. Of course, most generally, his underlying concern to meld intuitionistic logic with theory of meaning impels him to differ with the Brouwerian tradition of the openendedness of the notion of demonstration, and as we saw that was key to the anomalies exemplified by Counterexamples 1 and 2. But the remark also expresses Dummett's commitment to molecularity: that what it is to prove a sentence is explained in terms of what it is to prove each constituent of the sentence. That, of course, is a denial of the impredicative nature of intuitionistic conditionals; and it signals his commitment to just the view of the proofs of atomic sentences as, if you like, logically unanalyzable, that engenders Counterexample 3.
The difference between Dummett and the treatments of intuitionism standard in mathematical logic on these two points has not been sufficiently explored. In classical truth-functional semantics, atomic sentences are the basic building blocks, and it is clear why. Dummett takes atomic sentences to be the basic building blocks of a proof-theoretic semantics—and on both the “basic” aspect and the “building block” aspect he differs from classical intuitionism. It is not clear why one should believe this, except perhaps for the conflation of the notion of verification and a mathematical notion of proof.
The third factor expressed in Dummett's remark is that there will be no definite meaning ascribed to a sentence unless it is fixed what a demonstration is for that sentence. That will presuppose that not just the logical rules but also the boundary rules are fixed. This tells us that, from Dummett's viewpoint, the revised notion of validity is not acceptable. For, in considering all possible boundary rules, it should be clear, the revised notion of validity treats the atomic components of sentences in abstraction from their actual content. It takes them to be schematic, in that their connections to one another (and hence also to complex sentences) are varied at will, but this is precisely what Dummett's insistence that he seeks to justify actual inferences, not schematic ones, would rule out.6
Finally, I suppose the following line might be taken. The claim that Dummett's method provides justifications of logical laws might be abandoned or weakened, while still it be pressed that the method does show something. That, under the revised notion of validity, the inference rules that yield valid inferences under all substitutions are not the classical ones but precisely the intuitionistic ones, surely supports the ascription of some advantageous status to intuitionistic logic. But here we should note at once that the method—in taking the introductory rules as definitory of the connectives—identifies the sense of F → G as “G can be validly inferred from F ”, and then goes on to define the latter as “every valid canonical argument for F can be transformed into a valid canonical argument for G”. Thus, built into the method at the start is the intuitionistic construal of the conditional. As pointed out above, this is just what leads to condition (3) on the f--relation, and that in turn is the characteristic of the model theory of intuitionism. If (3) were to be replaced by α fF → G iff (if α fF then α fG), then what we obtain will be a classical notion of validity. In short, it should occasion no surprise, that the (revised) method yields intuitionistic validity, because the method is based on, or presupposes, an intuitionistic reading of the conditional. (Although attention is usually focused on negation as that which marks the difference between classical and intuitionistic, a case can be made that it's the conditional. A classical conditional combined with the definition of ¬F as F →⊥ would still yield the classical laws of negation.) And for this reason, that the method yields the intuitionistic inferences once it is applied schematically does not signal any greater virtue of intuitionistic logic, at least as framable from neutral ground. What is odd, and perhaps even undermining of the claims to virtue of intuitionistic logic, is that even when the intuitionistic reading of the conditional is built into the project at the start, it still takes lots of fussing here and jiggling there to get the method to yield just the intuitionistic laws.