Home Philosophy Advances in ProofTheoretic Semantics


BidirectionalityThe transmission view of consequence is incorporated in natural deduction in that we have the operations of assumption introduction, assumptionclosure by substitution and assumptionclosure by discharge. There are various notations for it. The most common such notation in prooftheoretic 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 sequentstyle 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 sequentstyle natural deduction the operation of assumption discharge is no longer nonlocal. 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 noassumptions system in the sense of Sect. 2.2: It combines assumptionfreeness with a twolayer 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 sequentstyle 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 twolayer 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 sequentstyle 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) B (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 secondlayer distinction. This means that he himself goes beyond his own idea of a singlelayer system. See SchroederHeister [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 assertioncentred forward reasoning in natural deduction. When reading a sequent (2) in the sense of (3), the step of (∧L) corresponds to: A ∧ B A D C 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 rightintroduction rules, extends a proof downwards, and, by means of leftintroduction 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 C where the line above A ∧ B expresses that A ∧ B stands here as an assumption. We may call this system a naturaldeduction sequent calculus, that is, a sequent calculus in naturaldeduction 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 assumptionfreeness 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] D 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 reinterpretation 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 metacalculus for natural deduction, as Prawitz ([44], Appendix A) suggests. It is a metacalculus in the sense that whenever there is a naturaldeduction derivation of B from A1,..., An , there is a sequentcalculus 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 leftintroduction rule in the sequent calculus. This means that at the level of proof construction there is no oneone 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 nontrivial. Prawitz is certainly right that a sequentcalculus proof can be viewed as giving instructions about how to construct a corresponding naturaldeduction 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 SchroederHeister, [59]). 
CONTENTS 

Related topics 