Home Philosophy Advances in Proof-Theoretic Semantics
In order to extend the notion of validity defined for deductions so that it can be applied to reasoning in general that proceeds by making arbitrary inferences, I consider treeformed arrangements of sentences of the kind employed in natural deduction, except that now the inference steps need not be instances of any fixed rules. They will be described by using common terminology from natural deduction, and are what will be called argument structures. A sentence standing at the top of the tree is to be seen either as an assumption or as asserted (inferred from no premisses). An occurrence of an assumption can be bound (discharged) by an inference further down in the tree. Indications of which sentences in the tree are assumptions and where they are bound (if they are bound) are to be ingredients of the argument structure.
An inference may also bind occurrences of a free variable (parameter) in sentences above the conclusion. Again it has to be marked how variables are bound by inferences. An argument structure is thus a tree of sentences with indications of these kinds, and can also be seen as a tree-formed arrangement of inferences chained to each other.
The notions of free assumption and free variable, of open and closed argument structure, and of a sentence or argument structure depending on a free assumption or parameter are carried over to the present context in the obvious way.
There are no restrictions on the argument structures except that an inference may not bind a variable that occurs in an assumption that remains free after the inference, that is, that the conclusion of the inference depends on (otherwise there would be a clash with the idea that an occurrence of a free assumption is free for substitution of closed argument structures, while bound variables are not free for substitution).
An argument structure may for instance look as follows
where the exhibited inference binds assumptions in the part A 3 of the form A(a) marked (1) as well as variables a that are free in A 3. The inference can be seen as representing an application of mathematical induction, where N stands for 'natural number' and s is the successor operation.
We keep open what forms of sentences are used in an argument structure in order to make the notion sufficiently general. However, when making comparisons with BHK-proofs of sentences in a first order language, we restrict ourselves to such languages. It is assumed that for each form of compound sentences there are associated inferences of a certain kind called introductions, for which we retain the condition from natural deduction that for some measure of complexity, the premisses of the inference and the assumptions bound by the inference are of lower complexity than that of the conclusion. For instance, we could allow the pathological operator tonk proposed by Prior and associate it with the introduction rule that he proposed.
We shall say that an argument structure is canonical or in canonical form if its last inference is an introduction.