Mappings of Valid Arguments on BHK-Proofs and Vice Versa
After having now made Gentzen's approach free from ties to a specific formal system, we return to the question whether the two approaches come to the same thing extensionally. Let us assume that P is a set of BHK-proofs of atomic sentences, that B is a base of valid arguments for atomic sentences, and that they have been mapped on each other. We shall try to extend these mappings to compound sentences.
In other words, we shall try to define one mapping called Proof which applied to a valid closed argument relative to B for a sentence A gives as value a BHK-proof of A over P , and a mapping in the other direction called Arg which applied to a BHK-proof over P of a sentence A gives as value a valid closed argument relative to B for A, assuming as an induction assumption that we have been able to define such effective mappings for all sentences of complexity less than that of A.
If α is a BHK-proof of a sentence A, Arg (α) has to be a pair, which will be written (Arg 1(α), Arg 2(α)); thus, Arg 1(α) is an argument structure for A and Arg 2(α) is a justification.
I restrict myself to the cases when A is an implication or a universal quantification, and shall consider in parallel the problems that arise for different variants of validity of arguments.
Extending the Mapping Proof to Arguments for A
7.1.1. Consider first the case when A is an implication B ⊃ C. Proof is then to be defined for any valid closed argument (A, J ) for A, which is done by saying that Proof(A, J ) is to be the operation α defined for BHK-proofs β of B such that
I have to explain what operation A◦ is and show—under the assumptions that (A, J ) is a valid closed argument for A and that β is a BHK-proof of B and the induction assumption—that:
(i) the operation A◦ is an effective procedure for finding an argument structure for
(ii) the pair to which Proof is applied above in (a) is effectively obtained from (A, J )
and β, and is a valid closed argument for C.
It then follows by the induction assumption that Proof is defined for this argument and that α(β) as defined in (a) is a BHK-proof of C, which means that the operation α is a BHK-proof of A.
If A is in canonical form, that is, has the form
we let A◦ be the immediate sub-structure Ai of A, which is an argument structure for C.
If A is not in canonical form, we want A◦ to be the immediate sub-structure of
a closed canonical argument structure A∗ to which A reduces with respect to J and that is valid with respect to J . Now it becomes important what kind of validity we are dealing with. If the argument (A, J ) is strongly valid, then as noted in Sect. 6.3, there is an effective procedure for finding such an argument structure A∗ that is strongly valid with respect to J : Generating the reduction sequences with respect to J that The left one stands for the same argument structure as A and is used to indicate that the last sentence of A is A. The right one stands for an argument structure formed by putting A under the structure A (and it is left open what the last sentence of A is).
start from A in some arbitrarily chosen order, we take the first canonical argument structure A∗ that we find. We then let A◦ be its immediate sub-structure; that is, A◦ is again Ai if A∗ has the form shown above.
Note that if (A, J ) is weakly valid, the procedure described above may result in an argument structure such that A∗ is not weakly valid with respect to J , and that if (A, J ) is neither strongly nor weakly valid, the procedure may not give any result at all. But when (A, J ) is strongly valid and closed, the operation A∗ is defined and is an effective procedure. Hence, A◦ is an effective procedure for finding an argument
structure for C.
If (A, J ) is weakly valid and this is taken in a constructive sense, then as already noted (Sect. 6.1.1), there is an effective procedure ∗ defined for all weakly valid closed arguments (A, J ) which yields an argument structure A∗ such that A reduces to A∗ with respect to J and A∗ is weakly valid with respect to J . Letting A◦ be the immediate substructure of A∗, we have again explained the operation A◦ as an effective procedure for finding an argument structure for C.
Task (i) has thus been carried out for strong validity and for weak validity read constructively, but not for weak validity read non-constructively. In the two successful cases, task (ii) is now easy. That the pair to which Proof is applied in (a) is effectively obtained follows from the induction assumption and the effectiveness of
the operation A◦. The demonstration of the fact that the pair is a strongly or weakly valid closed argument for C follows the same pattern for the two cases of validity, so we may let valid mean either weakly or strongly valid: That (A◦, J ) is a valid argument for C follows from the validity of (A, J ) or of (A∗, J ), as the case may
be. By the induction assumption (Arg 1(β), Arg 2(β)) is a valid argument for B, and from these two facts it follows by clause III∗ or III that the argument to which Proof
is applied in (a) is a closed valid argument for C, as was to be shown.
7.1.2. Let now A be the sentence ∀x B(x ), and let (A, J ) be a closed argument for
∀x B(x ) that is strongly valid or is weakly valid taken in a constructive sense.
As in Sect. 2, it is assumed that the elements in the individual domain D have canonical names. I apply the conventions explained there, and define Proof(A, J ) to be the operation α defined for the elements e in the individual domain D such that
α(e) = Proof(A◦(e), J ) (b) The operation A◦ is explained analogously to how it was explained in the preceding
case. Thus, if A is in canonical form, A has the form
∀x B(x )
and we let A◦ be Ai(a), the immediate sub-structure of A. A◦(e) is then the result of substituting for a in A◦(a) the canonical name for e.
If A is not in canonical form, we find effectively as in the preceding case a closed canonical argument structure A∗ to which A reduces with respect to J such that (A∗, J ) has the same kind of validity as (A, J ). We let then A◦(a) be the immediate substructure of A∗ and A◦(e) the result of substituting for a in A◦(a) the canonical name for e.
Since by clauses I∗ and III∗ or by clauses I and III (A∗(e), J ) is a closed valid argument for B(e), validity taken in one of the two forms here considered, it follows
by the induction assumption in question, that Proof is defined for this argument and that α(e) as defined in (b) is a BHK-proof of B(e). Thus, α is a BHK-proof of A.
-  Note the difference between the two notations below, commonly used in natural deduction: