Bidirectionality

The transmission view of consequence is incorporated in natural deduction in that we have the operations of assumption introduction, assumption-closure by substitution and assumption-closure by discharge. There are various notations for it. The most common such notation in proof-theoretic semantics is Gentzen's [25] tree notation that was adopted and popularised by Prawitz [44]. Alternative notations are Jas´kowski's [34] box notation, which is the origin of Fitch's [18] later notation. A further notation is sequent-style natural deduction. In this notation proofs consist of

judgements of the form A1,..., An fB, where the A's represent the assumptions

and B the conclusion of what is claimed. This can be framed either in tree form,

in boxed form, or in a mixture of both. With sequent-style natural deduction the operation of assumption discharge is no longer non-local. In the case of implication introduction

A 1 ,..., A n , B fC

A1,..., An fB → C (1)

we pass from one sequent to another without changing the structure of the proof. In fact, in such a proof there are no sequents as assumptions, but every top sequent is

an axiom, normally of the form A fA or A1,..., An , A fA. However, this is not

a no-assumptions system in the sense of Sect. 2.2: It combines assumption-freeness

with a two-layer approach. The structural layer is the layer of sequents composed out of lists of formulas building up the left and right sides (antecedent and succedent) of a sequent, whereas the logical layer concerns the internal structure of formulas. By using introduction rules such as (1), the logical layer is characterised in terms of the structural layer. In this sense sequent-style natural deduction is a variant of 'standard' natural deduction.

However, a different picture emerges if we look at the sequent calculus LK or LJ that Gentzen devised. These are two-layer systems in which we can manipulate not only what is on the right hand side and what corresponds to assertions, but also what is on the left hand side and what corresponds to assumptions. In sequent-style natural deduction a sequent

A1,..., An fB (2)

just means that we have a proof of B with open assumptions A1,..., An :

A1,..., An

D (3)

(Footnote 1 continued)

in different ways. This distinction is analogous to that between assumptions and assertion, so that, when we prove an implication, we can at the same time regard this proof as a proof of the upper member of this implication from its lower members taken as assumptions. In the Grundgesetze Frege [21] even specifies rules of proofs in terms of this second-layer distinction. This means that he himself goes beyond his own idea of a single-layer system. See Schroeder-Heister [64].

In the symmetric sequent calculus, which is the original form of the sequent calculus, the A1,..., An can still be interpreted as assumptions in a derivation of B, but no longer as open assumptions in the sense of the transmission view. Or at least they can be given an alternative interpretation that leads to a different concept of reasoning. In the sequent calculus we have introduction rules not only on the right hand side, but also on the left hand side, for example, in the case of conjunction:

A , A 1 ,..., A n fC

∧ A ∧ B, A1,..., An fC

This can be interpreted as a novel model of reasoning, which is different from assertion-centred forward reasoning in natural deduction. When reading a sequent

(2) in the sense of (3), the step of (∧L) corresponds to:

A ∧ B A

This is a step that continues a given derivation D of C from A upwards to a derivation of C from A ∧ B. Therefore, from a philosophical point of view, the sequent

calculus presents a model of bidirectional reasoning, that is, of reasoning that, by means of right-introduction rules, extends a proof downwards, and, by means of left-introduction rules, extends a proof upwards.

This is, of course, a philosophical interpretation of the sequent calculus, reading it as describing a certain way of constructing a proof from hypotheses.2 Since under this schema both assumptions and assertions are liable to application of rules, assumptions are no longer understood simply as placeholders for closed proofs. Both assumptions and assertions are now entities in their own right. Read in that way we have a novel picture of the nature of hypotheses. We can give this reading a format in natural-

deduction style, namely by formulating the rule (∧L) as

[ A]

A ∧ B C

where the line above A ∧ B expresses that A ∧ B stands here as an assumption. We

may call this system a natural-deduction sequent calculus, that is, a sequent calculus

in natural-deduction style. It is a system in which major premisses of elimination rules occur only as assumptions ('stand proud' in Tennant's [70] terminology). The

2Gentzen [25] himself devised the sequent calculus as a technical device to prove his Hauptsatz after giving a philosophical motivation of the calculus of natural deduction. He wanted to give a calculus in 'logistic' style, by which he meant a calculus without assumptions that just moves from claim to claim and whose rules are local due to the assumption-freeness of the system. The term 'logistic' comes from the designation of modern symbolic as opposed to traditional logic in the 1920s (see Carnap, [3]).

intuitive idea of this step is that we can introduce an assumption in the course of a derivation. If a proof of C from A is given, we can, by introducing the assumption

A∧ B and discharging the given assumption A, pass over to C. That A∧ B occurs only

as an assumption and cannot be a conclusion of any other rule, demonstrates that we

have a different model of reasoning, in which assumptions are not just placeholders

for other proofs, but stand for themselves. The fact that, given a proof D of

A ∧ B and a proof of the form [ A]

A ∧ B C

C A ∧ B

we obtain a proof of C by combining these two proofs is no longer built into the system and its semantics, but something that must be proved in the form of a cut elimination theorem. According to this philosophical re-interpretation of the sequent calculus, assumptions and assertions now resemble handles at the top and at the bottom of a proof, respectively. It is no longer the case that one side is a placeholder whereas the other side represents proper propositions.

This interpretation also means that the sequent calculus is not just a meta-calculus for natural deduction, as Prawitz ([44], Appendix A) suggests. It is a meta-calculus in the sense that whenever there is a natural-deduction derivation of B from A1,..., An ,

there is a sequent-calculus derivation of the sequent A1,..., An fB, and vice versa.

However, this does not apply to proofs. There is no rule application in natural deduc-

tion that corresponds to an application of a left-introduction rule in the sequent calculus. This means that at the level of proof construction there is no one-one correspondence, but something genuinely original in the sequent calculus. This is evidenced by the fact that the translation between sequent calculus and natural deduction is non-trivial. Prawitz is certainly right that a sequent-calculus proof can be viewed as giving instructions about how to construct a corresponding natural-deduction derivation. However, we would like to emphasise that it can be interpreted to be more than such a metalinguistic tool, namely as representing a way of reasoning in its own right. We do not want to argue here in favour of either of these positions. However, we would like to emphasise that the philosophical significance of the bidirectional approach has not been properly explored (see also Schroeder-Heister, [59]).