Home Philosophy Advances in Proof-Theoretic Semantics
8.1. We have thus shown that the notion of a weak valid argument taken constructively is extensionally equivalent with the notion of a BHK-proof.
When weak validity is taken non-constructively, I have not been able to construct a BHK-proof of A from a weakly valid argument for A, but only in the other direction a weakly valid argument for A from a BHK-proof of A, given the induction assumption.
In contrast, from a strongly valid argument for A, I have constructed a BHK-proof of A, given the induction assumption and the assumption that the reductions can be generated effectively, but have not been able to construct in the other direction a strongly valid argument for A from a BHK-proof of A.
Since the mentioned constructions depend on the assumption that there are mappings in both directions for sub-sentences, nothing has been established about the relations between on the one hand BHK-proofs and on the other hand arguments that are weakly valid understood in a non-constructive sense or are strongly valid.
8.2. As has been seen above, when the notion of valid deduction is generalized to the notion of valid argument, the justifications come to play the major role and the inferences of the argument structures a correspondingly minor role. Some of the intuitions behind the notion of valid deduction are lost in this way. It would therefore be interesting to investigate a more restricted notion of reductions than the one used here in connection with arguments.
The standard reductions in natural deduction are all transformations of a given deduction by two kinds of very simple effective operations, possibly combined with each other. One kind consists of operations ϕ such that ϕ(D) is a sub-deduction of D. The other kind consists of operations ϕ such that ϕ(D) is the result of substituting in D an individual term occurring in a sentence of D for a free variable occurring in a sentence of D or substituting in a sub-deduction of D for a free assumption (in that sub-deduction) another sub-deduction of D. Also the reduction associated with mathematical induction (Sect. 5.2) is a transformation built up of these two kinds of operations.
By applying operations of these two kinds to a deduction or an argument structure one obtains an argument structure that is contained in the given deduction or argument structure; in case substitutions have been carried out, we should perhaps say that the result is implicitly contained. A reduction of this kind associated to an inference constitutes a justification of the inference in a much stronger sense than the reductions that have been considered in connection with argument structures: Given that the arguments for the premisses are acceptable, there is an acceptable argument for the conclusion, because an argument for the conclusion is already contained, at least implicitly, in the arguments for the premisses taken together. This is actually the kind of justification of Gentzen's elimination rules that I have labelled the inversion principle, using a term from Lorenzen, and have presented as the intuition behind the normalization theorem for natural deductions .
An argument structure that is valid with respect to a justification that assigns such operations to occurrences of inferences would in itself have an epistemic force. Perhaps one could say that the function of the justifications would then be to verify that they have such a force, whereas valid arguments as they have been defined here often get their entire epistemic force from the justifications.
A notion of valid argument based on justifications of this kind would be a quite different concept from the variants of valid argument that have been dealt with in this paper. It would also be different from the notion of BHK-proof, it seems.
|< Prev||CONTENTS||Next >|