Home Philosophy Advances in Proof-Theoretic Semantics
Analysis of the Method
In order to make the method precise, we must define the notion of a canonical argument, for, to repeat, the idea is that an inference is justified if any canonical argument for its premises can be transformed into a canonical argument for its conclusion. The definition should make plausible the following: if a logically complex proposition is provable at all, then it could in principle be proved by a canonical argument. For only if that condition is met will Dummett's procedure have any plausible claim to justificatory force. In line with the underlying idea, it might be tempting to define a canonical argument as one composed only of introduction rules. This does not work, however, because of the nature of the introduction rule for the conditional, to wit: F → G may be inferred from a subsidiary argument from premise F to conclusion G, discharging the premise F . Since F itself may be logically complex, the argument from F to G cannot be restricted to those that use introduction rules only, or else many elementary logical truths will not be obtainable by canonical arguments, for example, A ∧ B → B. That is, a canonical argument will end in →-introduction:
[ A ∧ B]
A ∧ B → B
But if we are constrained to using only introduction rules, we will not be able to fill in the middle part. Hence the subsidiary arguments, the ones starting from premises that will eventually be discharged, cannot be constrained to contain only introduction rules. All that can be required of such subsidiary arguments is that they themselves be already recognized as justified. The result is a definition, by simultaneous induction on the complexity of the statements in the arguments, of the notion of “valid canonical argument” along with the notion of “valid argument”:
A valid canonical argument is a deduction whose premises are all atomic sentences and that uses only introduction rules except when auxiliary premises are introduced; at any point when such are introduced, the subargument from the point of the introduction of the first new premise to the last step before the discharge of the last new premise must be a valid argument.
A valid argument is an inference I such that any valid canonical argument (i.e., any valid canonical argument with any atomic premises) for the premises of I can be transformed into a valid canonical argument, with the same atomic premises, for the conclusion of I .
We have simplified matters slightly by omitting what Dummett calls “boundary rules”, which allow the inference of one atomic sentence from others.2 For example, these may be empirical laws, connecting the primitive notions of the vocabulary. Dummett allows the employment of such rules in valid canonical arguments. For the moment we take there to be no such rules, since the mathematics is clearer without them. In the next section, we shall allow boundary rules and investigate their impact.
The validity of an argument depends only on its premises and conclusion, and not on any intervening steps. Hence the second definition is framed as applying to inferences, rather than deductions. The simultaneous induction works because discharge of premises increases logical complexity. Thus, whether a deduction with conclusion F is a valid canonical argument depends on the validity of arguments whose premises and conclusion are of strictly lesser logical complexity than F .
These definitions are far from transparent. Applying them involves tracking through the tree structures of deductions in natural deduction systems. Most importantly, the definitions do not readily yield any general information about the range of inferences that are valid or not.
However, the definitions can be greatly clarified if we focus not on the prooftheoretic layout but rather on the relation that holds between a set α of atomic sentences and a formula F when there is a valid canonical argument with conclusion F and premises among the atomic sentences in α. Let us use “α fF ” for this relation. Using this notation we may frame the definition of “valid” thus: an inference from premises F1,..., Fn to conclusion G is valid iff, for all sets α, if α fFi for each i , then α fG. (It may seem that this reformulation ignores a constructivity requirement, implicit in the phrase “we can transform” of the original definition. However, since we are dealing with sentential logic only, all notions are decidable and all quantifiers in the metalanguage are constructively evaluable.)
We can now investigate the relation α fF , by looking at how its behaviour for logically complex F depends on its behaviour on the constituents of F . A valid canonical argument for F ∧ G is just a valid canonical argument for F and a valid canonical argument for G, put together by means of a final inference to F ∧ G, using
the rule of ∧-introduction. A valid canonical argument for F ∨ G is either a valid canonical argument for F followed by one application of ∨-introduction or else a
2These amount to the definitions given by Dummett in [3, p. 261], simplified by the absence of boundary rules and (more importantly) of the need to deal with free variables.
valid canonical argument for G followed by one application of ∨-introduction. These observations immediately yield:
α fF ∧ G iff α fF and α fG (1)
α fF ∨ G iff α fF or α fG (2)
A valid canonical argument for F → G with atomic premises in α is a valid inference I to G from premises F and members of α, followed by an application of →introduction, discharging the premise F and yielding F → G. The inference I will be valid provided that every valid canonical argument for F whose premises may include members of α and possibly some other atomic sentences can be transformed into a valid canonical argument for G whose premises are either in α or are among those others. This yields the condition:
α fF → G iff ∀β(if α ⊆ β and β fF, then β fG). (3) (1)–(3) show that the relation fis, in fact, a familiar one from the semantics of
intuitionistic logic, since they are nothing other than rules for the treatment of the connectives in the usual Kripke model semantics, when we take the sets α of atomic sentences as the nodes (worlds) of the model, and the relation α ⊆ β as the relation of extension. Thus the proof-theoretic trappings of Dummett's presentation conceal a notion whose structure is the same as the standard model-theoretic or semantic one.
One connective remains to be considered, namely, negation. As Dummett notes, the only way to treat negation that is consonant with his general procedure is to take
¬F as an abbreviation for (F →⊥), where ⊥ is a sentential constant governed by the
following introduction rule: from premises that are all the atomic sentences, it may be inferred. Dummett allows there to be infinitely many atomic sentences; in fact, this treatment of negation fares poorly if there are not. For if A1,..., An exhaust the atomic sentences, then the introduction rule just mentioned yields the validity of inferring ¬( A1 ∧ ... ∧ An ) with no premises. Thus on logical grounds alone we would be able to infer that not every atomic statement is true, and this is surely an unacceptable result.
If there are infinitely many atomic sentences, then this treatment of negation can most easily be incorporated into our forcing relation by requiring that the domain of sets of atomic sentences α that we consider is always finite. Then the stipulation above becomes:
α f⊥ for no α. (4)
The resulting rule for negation is then: α f¬F iff ∀β(if α ⊆ β then not β fF ). This is just the standard rule for the treatment of negation in the semantics of intuitionistic logic.
The characterization of the forcing relation will be complete once we give the clause governing atomic sentences themselves. Since we are at the moment allowing
no boundary rules, we have:
for any atomic sentence A,α fA iff A ∈ α. (5)
As we've just seen, Dummett's notion of valid canonical model yields a relation fthat obeys just the usual semantic rules for models of intuitionism, as given by (1)–(4). However, there is a key difference between fas used in Dummett's method and the ordinary model-theory of intuitionistic logic. In the latter, the validity of an inference would mean that at each node (world) in every Kripke model, if the premises are true then the conclusion is true. Dummett's method, in contrast, amounts to considering only one particular structure, the Kripke model in which every finite set of atomic sentences is a distinct node, and for every finite set of atomic sentences there is exactly one node at which all and only those sentences are true, namely, the node that is the set of those sentences. This restriction to one particular structure yields anomalous results.
Counterexample 1 If F does not contain ⊥, then the inference from no premise to
¬¬F is valid.
Proof It is easily shown by induction on the construction of F that if F does not contain ⊥ then for every α there exists β with α ⊆ β and β fF . But then for no γ do we have γ f¬F . Hence, for every α, α f¬¬F . D
By the way, since we have shown that, for F that do not contain ⊥, γ f¬F for no F , we also have the conclusion that, for such F and any G, the inference from no premises to ¬F → G is valid.
Counterexample 2 Let F be a sentence not containing ⊥ and G a sentence having no atomic sentences in common with F . Then the inference from premise F → G to conclusion G is valid.
Proof Suppose α fF → G; we must show α fG. By (3), for any β with α ⊆ β, if β fF then β fG. Moreover, as noted in the previous proof, there exists a β such that α ⊆ β and β fF .
The following is easily shown by induction on the construction of sentences: for any sentence H and any sets γ and δ, if A ∈ γ iff A ∈ δ for all atomic sentences A that occur in H , then γ fH iff δ fH .
Thus, if β1 is the subset of β containing just those atomic sentences either in α or occurring in F , we have A ∈ β iff A ∈ β1 for all A that occur in F . Since β fF , it follows that β1 fF . Hence β1 fG. Since F and G have no atomic sentence in common, no atomic sentence occurring in G is in β1 − α. Thus A ∈ β1 iff A ∈ α for all A that occur in G. Hence α fG. D
Thus there are many inferences that turn out valid under Dummett's definition, and yet are logically valid in no plausible sense. The counterexamples show that such inferences exist even in the fragment of the language that does not contain ⊥, and so does not contain negation. As a particularly vivid case, we have the validity of the inference from A → B to B whenever A and B are distinct atomic sentences! We must conclude that Dummett's method has no justificatory force whatsoever.
|< Prev||CONTENTS||Next >|