Home Philosophy Advances in Proof-Theoretic Semantics
The inferences of an argument structure that are not introductions should be justified by reductions as in natural deduction. I shall now be following Schroeder-Heister (2006)  partially by taking a justification to be simply a set of reductions  and a reduction to be a pair (A 1, A 2) of argument structures such that A 1 is not canonical and A 2 ends with the same sentence as A 1 and depends at most on what A 1 depends on.
An argument is a pair (A, J ), where A is an argument structure and J is a justification. An argument is said to be closed, open, or canonical (or in canonical form), if the respective attribute is applicable to the argument structure.
A 1 is said to reduce immediately to A 2 with respect to J , if (A 1, A 2) belongs to J . A reduction sequence with respect to the justification J is a sequence A 1, A 2,..., A n (n ≥ 1) such that for each i < n, either A i reduces immediately to A i +1 with respect to J or A i +1 is obtained from A i by replacing an initial part Ai of A i by an argument structure Aii such that Ai reduces immediately to Aii with respect to J . An argument structure A is said to reduce to the argument structure A∗ with respect to the justification J , if there is a reduction sequence with respect to J whose first element is A and last element is A∗.
Justifications of deductions as described above (Sect. 3) and of argument structures as I originally defined them were effective operations assigned to inference schemata and differ in this respect from the notion that I am now adopting. The main difference is that the relation 'to reduce immediately to' becomes now one-many instead of one-one. The present notion of justification is of particular interest when we come to comparing valid arguments with BHK-proofs , but as we shall see it has some unwanted consequences.
Schroeder-Heister remarks that to take justifications to be relations corresponds to the idea that there can be “alternative justifications” of the same argument structure. I think that this idea is somewhat doubtful; anyway, as we shall soon see, it can be taken in many ways.
Since a justification is just a set of reductions, it may not “really” justify the argument structure. We could say that what is called a justification is merely a proposed or possible justification, a justification candidate. What is required of a “real” justification gets expressed by the definition of what it is for an argument to be valid.
For instance, one can invent a justification of an argument structure using Prior's elimination rule for tonk by assigning some reductions to applications of the rule, but this will never give rise to valid arguments that make creative uses of Prior's rule.
An important example of justifications outside the standard ones for the elimination rules in natural deduction is one that can be associated with the argument structures exhibited in the preceding subsection as representing applications of mathematical induction. It consists of a pair (B 1, B 2) where thus B 1 is an argument structure of this form. What B 2 is depends on the form of the first premiss of the last inference, Nt , which may be called the major premiss of the inference. If the major premiss has the form N 0 and the conclusion accordingly has the form A(0), B 2 is to be A 2, the argument structure for A(0) that represents the induction base. If it has the form Ns(t ) and stands as conclusion of an inference whose premiss is Nt , the conclusion accordingly having the form A(s(t )), B 2 is to be argument structure
If the term t is a numeral n, the argument structure is finally transformed by successive reductions of this kind to an argument structure consisting of the induction base A 2 followed by n applications A 3(0), A 3( 1), . . . , A 3( n − 1 ) of the induction step on top of each other. These reductions represent indeed the natural and commonly given justification for inferences by mathematical induction.
|< Prev||CONTENTS||Next >|