We can now define what it is for an argument to be valid by adopting three principles analogous to the ones stated for valid deductions:

I. A closed canonical argument (A, J ) is valid, if for each immediate sub-argument structure A∗ of A, it holds that (A∗, J ) is valid.

II. A closed non-canonical argument (A, J ) is valid, if A reduces relative to J to an argument structure A∗ such that (A∗, J ) is valid.

III. An open argument (A, J ) depending on the assumptions A1, A2,..., An is valid, if all its substitution instances (A∗, J ∗) are valid, where A∗ is obtained by first substituting any closed terms for free variables in sentences of A, resulting in an argument structure A◦ depending on the assumptions A◦, A◦,..., A◦ , and then

1 2 n

for any valid closed argument structures (A i , Ji ) for A◦, i ≤ n, substituting A ifor A◦ in A◦, and where J ∗ = J Ji ∪ J .

Because of the assumed condition on the relative complexity of the ingredients of an introduction inference, the principles I-III can again be taken as clauses of a generalized inductive definition of the notion of valid argument relative to a base B, which is to consist of a set of closed argument structures containing only atomic sentences. If A is an argument structure of B, the argument (A, ∅), where ∅ is the empty justification, is counted as canonical and outright as valid relative to B. A base is seen as determining the meanings of the atomic sentences. An argument that is valid relative to any base can be said to be logically valid.

If A is an argument structure representing mathematical induction as exhibited in Sect. 5.1, J is the justification associated with A as described in Sect. 5.2, and B is a

base for arithmetic, say corresponding to Peano's first four axioms and the recursion schemata for addition and multiplication, then the argument (A, J ) is valid relative to B (as was in effect first noted in a different conceptual framework by Martin-Löf (1971) [14]. This is an example of a valid argument that is not logically valid but whose validity depends on the chosen base. However, I shall often leave implicit the relativization of validity to a base.

Instead of saying that the argument (A, J ) is valid it is sometimes convenient to say that the argument structure A is valid with respect to the justification J . But it is argument structures paired with justifications that correspond to proofs and that will be compared to BHK-proofs.

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