Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Extending the Mapping Arg to BHK-Proofs of A

7.2.1. Now I first consider the easiest case when A is a universal sentence ∀x B(x ). Let α be a BHK-proof of A. I define Arg (α) = (Arg 1(α), Arg 2(α)) as follows:

The line above the top sentence B(a) in the argument structure that Arg 1(α) assumes as value is meant to indicate that B(a) is not an assumption but is inferred from zero premisses; thus, the parameter a does not occur in any assumption that the sentence at the bottom depends on, and it becomes therefore bound by the ∀Iinference as usual.

For the argument structure Arg 1(α) to be valid with respect to a justification J , it is necessary and sufficient that J contains a reduction such that any instance of the argument structure B(a) reduces with respect to J to an argument structure A that is

valid with respect to J . The problem is that it is not sufficient to find, for each closed term t , appropriate reductions for B(t )[1]. Instead we must find a set J of reductions such that it can be shown that, for each term t , J contains appropriate reductions. I succeed in showing this only for the case of weak validity. The set Arg 2(α) defined above will be shown to be such a justification in that case. The same result could be obtained more easily by choosing the universal set of reductions for the language in question, but it may be of some interest to see that this smaller set will do.

For the understanding of the definition of Arg 2(α), recall that α∗ is the effective operation assumed in Sect. 2 to be possible to obtain effectively from α such that for each closed term t , α(t ) is a BHK-proof of B(t ). I also want to make clear that Arg 2(α) is the union of two sets (i) and (ii) where (i) is the union of all sets Arg 2(t )) for closed terms t and (ii) is the set of all pairs (B(t ), Arg 1(t ))) where t is a closed term. By the induction assumption, Arg 1(t )) and Arg 2(t )) are both defined.

In order to show that (Arg 1(α), Arg 2(α)) is a weakly valid argument for ∀x B(x ), we have to show in view of principles I and III and since Arg 1(α) is a closed argument structure for ∀x B(x ) in canonical form that the argument (B(t ), Arg 2(α)) is weakly valid for each closed term t . To this end we must show in view of principle II that B(t ) for each closed term t reduces with respect to Arg 2(α) to an argument structure

A such that (A, Arg 2(α)) is weakly valid.

We shall now verify that for each closed term t , Arg 1(t )) is such an argument structure A. Firstly note that it has been arranged so that B(t ) reduces to Arg 1(t )) with respect to Arg 2(α) for each closed term t by the defining Arg 2(α) as a union of two sets (i) and (ii) where (ii) is the set of all pairs (B(t ), Arg 1(t ))) for closed terms t . Secondly, note that by the induction assumption, for each closed term t , (Arg 1(t )), Arg 2(t ))) is a closed weakly valid argument for B(t ), since α(t ) is a BHK-proof of B(t ). Thirdly, we recognize that from the last fact follows the wanted result that (Arg 1(t )), Arg 2(α)) is weakly valid, because Arg 2(t )) is a subset of Arg 2(α) (in virtue of being a subset of the set (i) described above) and weak validity is monotone with respect to justifications, as remarked in Sect. 6.3.2. As seen the monotonicity of weak validity with respect to justifications is used in establishing this mapping, and therefore a similar demonstration does not go through for strong validity, not being monotone with respect to justifications.

7.2.2. Let now A be an implication BC and let α be a BHK-proof of BC. The construction of Arg (α) is similar to the preceding case. Clearly, Arg 1(α) is to be the canonical argument structure

It is weakly valid with respect to Arg 2(α), if and only if, for each weakly valid, closed argument (A, J ) for B, the argument structure

reduces with respect to JArg 2(α) to an argument structure A◦ such that (A, JArg 2(α)) is weakly valid (as is seen by applying clauses I, III, and II in this order). To guarantee that there is such an A◦ for each weakly valid closed argument (A, J ),

I define

Arg 2(α) = I{Arg 2(α(Proof(A, J ))) : (A, J ) is a weakly valid closed argument for B}

∪ {(A, A∗∗) : there is weakly valid closed argument (A, J ) for B

such that A∗ is of the form (c) and A∗∗ is Arg 1(α(Proof(A, J )))}

Assume now that (A, J ) is a closed argument for B that is weakly valid. We shall verify that Arg 1(α(Proof(A, J ))) is the wanted A◦. Firstly, note that the argument structure (c) reduces with respect to JArg 2(α) to Arg 1(α(Proof(A, J ))) in virtue of the fact that the pair ((c), Arg 1(α(Proof(A, J )))) is a member of the second set in the union that by definition constitutes Arg 2(α). Secondly, we note that by the induction assumption, Proof(A, J ) is a BHK-proof of B. Hence α(Proof(A, J )) is

a BHK-proof of C. Therefore, by the induction assumption in the other direction,

(Arg 1(α(Proof(A, J ))), Arg 2(α(Proof(A, J )))) (d) is a weakly valid argument for A. Thirdly, we recognize that from the weak validity

of the argument (d) follows the wanted result that the argument (Arg 1(α(Proof(A, J ))), JArg 2(α)) is weakly valid, because Arg 2(ϕ(Proof(A, J ))) is a subset of Arg 2(ϕ) (in virtue of being a subset of the first set of the union that constitutes Arg 2(ϕ) by definition) and weak validity is monotone with respect to justifications.

The demonstrations in 7.2.1 and 7.2.2 have been entirely constructive and thus

show that the result that Arg (α) is a closed weakly valid argument for A when α is a BHK-proof of A holds even when the notion of weak validity is understood constructively.

  • [1] This is all that is required by Dummett's notion of valid argument structure, which means that his notion is quite obviously extensionally equivalent to the notion of BHK-proof
 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics