6.1. As is easily seen, it comes to the same if we in clause II of the definition of validity require instead that A reduces relative to J to a canonical argument structure A∗ that is valid with respect to J .

An important question concerning valid arguments, especially crucial when comparing them with BHK-proofs, is whether this canonical argument A∗ required by clause II can be found effectively.

6.1.1. If the definition of validity is read constructively, or in other words, if the existential quantifier in clause II is understood intuitionistically, the answer is of course yes, the canonical argument A∗ can be found effectively. If so, there is also an effective operation denoted by ∗ that is defined for every valid closed argument (A, J ) and yields a canonical argument structure A∗ such that A reduces to A∗ with respect to J and (A∗, J ) is valid.

6.1.2. Otherwise, if the definition is not taken in a constructive sense, it is not guaranteed that A∗ can be found effectively. Even if we require of a justification that it should be possible to generate its reductions effectively, it is still not guaranteed that A∗ can be found effectively. It is true that when we are generating the reduction sequences with respect to a justification J that start from a closed non-canonical argument structure A that is valid with respect to J , we sooner or later hit upon a canonical argument structure A∗ such that (A∗, J ) is valid. But since validity is not a decidable property, we may not be able to tell which one(s) of the canonical structures A∗ that we reach in this way is (are) the right one(s).

6.2. The situation was quite different when we were dealing with valid deductions based on the standard reductions in natural deduction. Given a closed valid deduction A, a valid canonical deduction A∗ as required by principle II can always be found effectively because of two facts: firstly, as already noted, the justifications consist of effective operations, which means that a deduction reduces immediately to at most one other deduction; and secondly, it can be shown that, regardless of the order in which the operations are applied, they will transform a closed deduction to a valid canonical one. This second feature can be called strong validity^{[1]}, in analogy with how in proof theory one says that a natural deduction is strongly normalizable if all reduction sequences terminate in a normal deduction.

Similarly, we can speak of strong validity of arguments when the canonical argument A∗ is found regardless of the order in which the reductions are taken and regardless of which reductions in J are employed. More precisely, a definition of an argument structure (A, J ) being strongly valid (relative to a base B whose argument structures are now counted outright as strongly valid) is obtained by clauses I∗-III∗, where I∗ and III∗ are like I and III except that “valid” is replaced with “strongly

valid” and the second clause reads:

II∗ A closed non-canonical argument (A, J ) is strongly valid, if each reduction sequence relative to J starting from A can be prolonged to a reduction sequence that contains a canonical argument structure A∗ such that (A∗, J ) is strongly valid.

Henceforth, I shall refer to the notion of validity defined by I–III as weak validity.

6.3. Effectiveness is restored when going from weak validity to strong validity, in spite of the justification still being a relation instead of a set of operations, provided that we require that its reductions can be generated effectively. When we generate in some arbitrarily chosen order the reduction sequences with respect to J that start from a closed argument structure A that is a strongly valid with respect to J , the first canonical argument A∗ that we find is guaranteed to be strongly valid with respect to J ; to verify this fact, note that reductions obviously preserve strong validity: if A reduces to A∗ with respect to J and (A, J ) is strongly valid, then so is (A∗, J ).

6.3.1. That effectiveness is obtained can be seen as an aspect of the fact that strong validity requires all so-called “alternative justifications” to be “real” justifications, so to say—if a closed argument (A, J ) is strongly valid and the reductions (A 1, A 2) and (A 1, A 3) both belong to J , clause II∗ requires that regardless of which one is used in a reduction sequence, it takes A a step towards a valid canonical argument. Clause II, in contrast, only requires that one of the reductions does so, which means that the other reduction may lead astray and may have no significance for the validity of the argument in question.

6.3.2. An aspect of the last feature is that weak validity is obviously monotone with respect to justifications: if (A, J ) is weakly valid and J ⊆ J ∗, then (A∗, J ∗) is weakly valid too—whatever reductions we add to J , the argument remains weakly valid. In contrast, strong validity is not monotone with respect to justifications— added “alternative justifications” must be “real”, if validity is to be preserved.

6.3.3. Yet another aspect of essentially the same feature is that the property of an argument structure to be weakly valid with respect to some justification J is indeed a very weak property. In fact, there is a justification J for a given language such that any non-canonical argument structure A for a sentence A in that language is weakly valid with respect to J , provided only that there exists a weakly valid closed argument (A∗, J ∗) in that language for A. We can simply choose as J the universal set of reductions in that language, call it UR . Since J ∗ ⊆ UR , the argument (A∗, UR ) is weakly valid by the monotonicity of weak validity, and since A reduces to A∗ with respect to UR , (A, J ) is weakly valid too in virtue of clause II.

It must be said that this argument (A, UR ) may be quite far from an intuitively

valid argument for A—the inferences in A may lack any significance for the validity of the argument, and the only relevant property of UR for the validity is that the reduction (A, A∗) is an element and that J ∗ is included.

6.4. It should be noted that strong validity does not entail weak validity; a strongly valid argument for an implication A ⊃ B is also weakly valid if A does not contain implication, but as soon as implication becomes nested in the antecedent, this may cease to hold because of the third clause in the definitions of validity.

The features discussed here of the two variants of validity are essential when we are to compare the valid argument with the BHK-proofs, as will be seen in the next section ^{[2]}.

[1] I have previously used the expression strongly valid for deductions and arguments in another way where it would be better to say strongly computable—cf. second part of footnote 7

[2] As to the other variants of validity mentioned in footnote 8, Dummett defines validity directly for argument structures, thus leaving the justifications implicit. I have commented on this difference elsewhere [20], but then overlooked one important consequence of it, which is now taken up in footnote 14. Schroeder-Heister's notion of validity differs from weak validity as defined here by following my previous definition of valid deduction as regards extensions of the given base B (see footnote 7). We get this notion by requiring in clause III that also for every extension B∗ of B, it holds that all substitution instances (A∗, J ∗) are valid relative to B∗ where A∗ is obtained by substituting for A ◦ a closed argument structure A i such that (A i , Ji ) is valid relative to B∗. To consider extensions of the given base in this way is natural when a base is seen as representing a state of knowledge, but is in conflict with the view adopted here that a base is to be understood as giving the meanings of the atomic sentences. For instance, the argument representing reasoning by mathematical induction presented in Sect. 5.3 ceases to be valid relative to the arithmetical base B if we require in clause III that validity be monotone with respect to the base. Concerning my original notion of validity see remarks made in the text and in footnote 10

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