To apply proof theory to the investigation of dialogues, we introduce a sequent calculus representation of Lorenzen dialogue. Then, as a rst step in extending our study of Lorenzen dialogue to the study of argumentation more generally, we extend Lorenzen dialogue by introducing why-because moves. We show that a sequence of why-because moves corresponds to a successive applications of cut-rule in a sequent calculus proof. Then, by combining the correspondence between Lorenzen dialogue and sequent calculus GK, we show that our dialogue corresponds to sequent calculus GK+cut.
In the 1950s, Lorenzen [
Apart from those studies on Lorenzen dialogue as another semantics of logics than the usual
set-theoretical semantics, Lorenzen dialogue has also received attention from the viewpoint of
argumentation theory. See, for example, [
In Lorenzen dialogue, as well as related dialogues investigated in argumentation theory, a
dialogue is de ned as a sequence of moves or locutions, such as attack and defense, and such
moves are associated with each other, for example, by reference numbers. However, such a
description of a dialogue as a sequence of moves is not suitable for structural analysis of dialogue.
From the viewpoint of logic, this is similar to the description of proofs in Hilbert-style, which is
not suited for structural analysis of proofs. Cf. [
In this article, we introduce a sequent calculus representation of Lorenzen dialogue. Sequent
calculus, along with natural deduction, is the most popular formalization in logic, and it led to a
signi cant development in proof theory. Furthermore, sequent calculus provides a basis for both
automated theorem proving and logic programming. Our sequent calculus representation of
dialogues enables the application of the proof theoretical results and techniques to the study of
dialogues; investigation of typical or normal forms of dialogues and the normalization theorem,
structural analysis of dialogues, characterization of the structure of dialogues, automated
dialogue construction, and so on. Cf. [
In Section 2, we review a variant of sequent calculus called Kleene’s sequent calculus GK
[
The original Lorenzen dialogue is a dialogue for the interpretation of basic logical connectives,
and as such is inadequate for exploring general arguments that do not t within the framework of
those logical connectives. Kacprzak and Yaskorska [
Formulas are de ned inductively as usual. Formulas are denoted by A, B, C, . . . , and atoms are denoted by Q, R, . . . . For simplicity, we consider only propositional connectives ¬ (negation) and ^ (conjunction).
We introduce a variant of Gentzen’s sequent calculus [
De nition 2.1. The inference rules of GK are the following ¬l and ¬r (inferences on ¬A), and ^ li (i = 1, 2) and ^ r (inferences on A1 ^ A2).
Ai, , A1 ^ A2 ` , A1 ^ A2 ` , ¬A ` A,
, ¬A ` ^ li(i = 1, 2) ¬l , A ` , ¬A ` ¬A,
¬r ` A1, , A1 ^ A2 ` A2, , A1 ^ A2 ` A1 ^ A2, ^ r Any sequent of the form , Q ` Q, , where Q is an atom, is called an axiom.
In each rule, and are collectively called the context. A proof, which is denoted by
⇡, ⇡ 1, ⇡ 2, . . . , is a nite tree constructed using inference rules, whose leaves are axioms. See
[
In section 4, we investigate GK + cut by adding the following rule of cut to GK, which is
known as an admissible rule in GK [
` , A , ⇧ `
A, ⇧ ` ⇤ , ⇤ (A) In the above form of cut, the two occurrences of A is called the cut-formula.
cut-rule can be regarded as a generalization of modus ponens; ` A and A ` C implies ` C. Furthermore, this rule can be interpreted as logical reasoning that uses an appropriate “lemma” (` A), intermediate steps that may be easier to prove, to prove conclusion (` C).
In Section 3.1, we review Lorenzen dialogue following Felscher [
Lorenzen dialogue is introduced as a two players’ dialogue between Proponent and Opponent. We use X, Y (X 6= Y ) to denote P (Proponent) or O (Opponent). The rule of a dialogue is de ned based on the following argumentation form, which describes how a composite formula may be attacked and, how, if possible, this attack may be defended.
The argumentation forms of Lorenzen dialogue for the connectives ^ and ¬ are de ned as follows (read from bottom up). Y ’s assertion is a formula C obtained previously by Y ’s defense on C or Y ’s attack on ¬C.
^ -argumentation form Y ’s defense by asserting Ai X’s attack by choosing i = 1 or 2 Y ’s assertion of A1 ^ A2 ¬-argumentation form No defense is possible X’s attack by asserting A Y ’s assertion of ¬A
We express an X’s attack upon A1 ^ A2 by choosing Ai (for i = 1, 2) as (Xa; ^ i), an X’s attack upon ¬A by asserting A as (Xa; A), an X’s defense by asserting A as (Xd; A).
An X’s move is (Xa; ^ i; j), (Xa; A; j), or (Xd; A; j), where j is a natural number called the reference number, which denotes for what number of the move is attack/defense in a sequence of moves. We denote moves as m, m1, m2, . . . .
The attack of j-th move is said to be open at k-th move with j < k, if there is no l-th move with j < l k which carries a defense to the attack of j-th move according to the appropriate argumentation form.
De nition 3.1. A sequence of moves m1, m2, m3, . . . , where we refer k-th move by mk, is a dialogue for a formula A if it satis es the following conditions. (D00) The rst move m1 is (P d; A; 0), and thereafter, P ’s and O’s moves appear alternately. (D01) If mk (k > 1) is (Xa; ^ i; j), or (Xa; A; j) for j < k, then mk is an X’s attack upon the assertion in mj according to the appropriate argumentation form. (D02) If mk (k > 1) is (Xd; A; j) for j < k, then mk is an X’s defense to the attack in mj according to the appropriate argumentation form. (D10) P may assert an atom only after it has been previously asserted by O. (D11) If, at mk 1, there are several open attacks suitable to be defended at mk of O, then only the latest of them may be defended at mk of O. (D12) A P ’s attack may be defended by O at most once. (D13) A P ’s assertion may be attacked by O at most once.
A dialogue for A is won by P if it is nite, ends with P ’s move and if the rules do not permit O to continue with another move.
De nition 3.2. A strategy for A is a tree with moves as nodes, which satis es the following conditions.
1. Each branch is a dialogue for A; 2. Every O’s move has at most one successor node; 3. Every P ’s move has all successor nodes for each possible next O’s move. A winning strategy for A is a strategy for A, where every dialogue in it is won by P .
The above dialogue is that for classical logic. Felscher [
We review the sequent calculus representation GKD of Lorenzen dialogue introduced in [
` ⇤ , [] for any multiset of formulas
[⇧] is formulas to be defended by O; is formulas to be attacked by P ; ⇤ is formulas to be attacked by O; and [] is formulas to be defended by P .
Although we can de ne our GKD in the same way as Lorenzen dialogue of the previous section, we here introduce our dialogue GKD in the style of sequent calculus. From the proof theoretical viewpoint, a winning strategy corresponds to a proof, and a dialogue in such a winning strategy corresponds to a branch in the proof. Based on the correspondence, we de ne the notion of a strategy prior to a dialogue. Thus, in the following de nition of moves, O’s attack on A1 ^ A2 (denoted as Oa^ 12) is de ned including branching as it is in ^ r-rule in GK. De nition 3.4. Moves of X’s attack on A1^ A2 (Xa^ i), X’s attack on ¬A (Xa¬), X’s defense on A (Xd) are de ned as follows.
[⇧] , ` ⇤ , [A1, , A1 ^ A2] [⇧] , [⇧] , ` A1 ^ A2, ⇤ , []
` ⇤ , [A2, , A1 ^ A2] [⇧ , Ai], , A1 ^ A2 ` ⇤ , []
[⇧] , , A1 ^ A2 ` ⇤ , [] [⇧] , , A ` ⇤ , [ , ¬A] [⇧] , ` ¬A, ⇤ , [] [⇧] , A, [⇧ , A], ` ⇤ , [] ` ⇤ , []
Oa¬
Od
P a^ i(i = 1, 2) [⇧] , , ¬A ` A, ⇤ , []
[⇧] , , ¬A ` ⇤ , []
The above moves are read from the bottom up. For Oa^ 12, when we focus one of the two upper sequents, we refer the move by Oa^ 1 or Oa^ 2. In the given de nition of moves, if we ignore contexts ⇧ , , , ⇤ , we nd that they correspond to the argumentation forms of Lorenzen dialogue: X’s ¬-argumentation form corresponds to Xa¬; X’s ^ -argumentation form corresponds to the pair of moves Xa^ i followed by Y d.
De nition 3.5. A strategy for a sequent the following conditions.
`
is a tree constructed using moves satisfying
2. In each branch, the rst (i.e., the bottom of the tree) is P ’s move, and thereafter, the moves of O and P alternately appear. 3. P d on Q or P a¬ on ¬Q for an atom Q is possible only when the given d-sequent is of the form [⇧] , ⌃ , Q ` ⇤ , [] , where Q 2 or ¬Q 2 ⌃ .
Every branch in a strategy is called a dialogue. A strategy for ` and every leaf thereof is of the form ⌃ , Q ` Q, [] for an atom Q. is winning if it is nite, Example 3.6. The following left is a winning strategy for ¬(¬Q ^ Q) (which is equivalent to Q _ ¬ Q) in Lorenzen dialogue, and the following right is that in GKD. Both read from bottom to top.
P a¬ Od P a^ 1
Although the original Lorenzen dialogue is de ned for a formula A, it can be regarded as our dialogue for the sequent ` A. Condition (3) of De nition 3.5 is the same as (D10) of the original Lorenzen dialogue.
By a P ’s attack (P a^ i or P a¬), the attacked O’s assertion remains in the same position in the upper sequent; hence, P may attack more than once for the same assertion of O, in the same way as Lorenzen dialogue. In contrast, by an O’s attack (Oa^ i or Oa¬), the attacked P ’s assertion (eg., A1 ^ A2 in the lower sequent [⇧] , ` A1 ^ A2, ⇤ , [] of Oa^ 12) is moved inside [ ] which are formulas to be defended by P (eg., [⇧] , ` ⇤ , [Ai, , A1 ^ A2]). Thus, O can attack a P ’s assertion at most once, and the condition (D13) of Lorenzen dialogue is included in our description of moves of Oa.
By an O’s defense Od, the defended formula A in the lower sequent [⇧ , A], ` ⇤ , [] is moved to the position of O’s assertion [⇧] , A, ` ⇤ , [] . Thus, O can defend a P ’s attack at most once, and the condition (D12) of Lorenzen dialogue is included in our Od. Although, at rst glance, P d appears to be the same as Od, but it is not. By Oa (eg., A1 ^ A2 in the upper sequent [⇧] , ` ⇤ , [Ai, , A1 ^ A2] of Oa^ 12), the attacked formula itself (A1 ^ A2) is duplicated inside [ ] to be defended by P . Thus, when P d on A is applied to an O’s attack [⇧] , ` ⇤ , A, [] , the formula A is contained in . That is, P may defend an O’s attack several times.
We nd that the restriction (D11) on O’s moves also holds in GKD as follows. Lemma 3.7. In any strategy, the O’s move is uniquely determined.
Proof. Beginning with a d-sequent of the form ` [] , P ’s possible move is P d, P a¬, or P a^ i. (1) By P d or P a¬, we obtain a d-sequent of the form 0 ` A, [ 0]. Then, the next possible O’s move is only an attack on A; as such, we return to a d-sequent of the form 00 ` [ 00]. (2) By P a^ i, we obtain [A], 0 ` [ 0]. The next possible O’s move is only Od, and we return to a d-sequent of the form 00 ` [ 00]. Thus, in a strategy, no choice of moves exists for O.
In particular, Od is possible for only the latest P a; hence, (D11) holds in our GKD. Based on the above discussion and Lemma 3.7, we show that GKD is Lorenzen dialogue. Proposition 3.8. Every dialogue of GKD is a Lorenzen dialogue.
Proof. We show that a given dialogue of GKD for ` A, i.e., a branch in a strategy for ` [A], is a Lorenzen dialogue. The rst P ’s move P d is common; hence, (D00) holds in GKD.
As for (D01), Oa^ i in GKD corresponds to the move (Oa; ^ i; k) in Lorenzen dialogue. Note that when Oa^ i is possible in GKD, there exists P ’s assertion A1 ^ A2, that is, A1 ^ A2 is already asserted by P before the Oa^ i. The same applies to the other attack moves of O and P ; hence, (D01) also holds in GKD.
As for (D02), Od on A in GKD corresponds to the move (Od; A; k) in Lorenzen dialogue. Note that when Od on A is possible in GKD, A is already inside [ ] formulas to be defended by O, and hence, A should be moved inside [ ] before the Od. The same applies to P d, and hence, (D02) also holds in GKD.
(D10)⇠ (D13) hold in GKD as discussed previously and by Lemma 3.7.
Thus, we obtain the equivalence between our GKD and Lorenzen dialogue via the
completeness theorem of Felscher [
Ai, A1 ^ A2,
A1 ^ A2, ` ` ^ li
() ` , A1 ^ A2, A1 ` , A1 ^ A2, A2 ` , A1 ^ A2 ^ r ()
Ai, A1 ^ A2, [Ai], A1 ^ A2,
A1 ^ A2,
In Section 4.1, we introduce our why- and because-moves, and discuss their counterparts in sequent calculus. Then, in Section 4.2, we de ne our WB-dialogue, and Lorenzen dialogue extended with WB-dialogue GKDwb. We show the correspondence between our dialogue GKDwb and sequent calculus GK + cut.
We introduce O’s why-move and P ’s because-move. On the one hand, by a why-move, O
requires grounds for a formula provided by P . On the other hand, by a because-move, P
provides grounds for a formula asked by O. Essentially the same dialogue is introduced in [
Firstly, P chooses a formula A1 and claims it. 2. O’s why: ` [A1]
By the why-move, O requires grounds for A1, which is expressed by the d-sequent ` [A1].
By the O’s why-move, A1 becomes a formula to be defended by P . 3. P ’s because: A2, A3 ` [A1]
P provides grounds A2 and A3 for A1. By the because-move, P puts A2 and A3 on the left-hand side of the given d-sequent ` [A1] of (2). If O agrees that A2 and A3 hold, then the dialogue ends. Otherwise, O further requires grounds for A2 or A3 by a why-move. 4. O’s why: (` [A2]) (A2, A3 ` [A1])
O requires grounds for A2. By the why-move, O extends the given d-sequent A2, A3 ` [A1] of (3) by connecting another d-sequent ` [A2]. 5. P ’s because: (A4 ` [A2]) (A2, A3 ` [A1])
P provides ground A4 for A2. 6. O’s why: (` [A3]) (A4 ` [A2]) (A2, A3 ` [A1])
O requires grounds for A3. 7. P ’s because: (A5 ` [A3]) (A4 ` [A2]) (A2, A3 ` [A1])
P provides ground A5 for A3.
In this way, a WB-dialogue is expressed by a sequence of d-sequents extended to the left. Except for the rst P ’s claim, a pair of an O’s why-move and a P ’s because-move constitutes a d-sequent of the form ` [A]. We call the above sequence of d-sequents connected with a multi-d-sequent (md-sequent for short).
From the viewpoint of sequent calculus, corresponds to cut-rule; the md-sequent (A4 ` [A2]) (A2, A3 ` [A1]) corresponds to the following application of cut.
A4 ` A2 A2, A3 ` A1 (A2)
A4, A3 ` A1 Thus, if O agrees that A4 and A5 hold, then the above WB-dialogue is nished, and it is interpreted as the following successive applications of cut called a cut-string. ` A5 ` A4 ` A1
A5 ` A3
A4 ` A2 A2, A3 ` A1 (A2)
A4, A3 ` A1 (A3)
A5, A4 ` A1 (A4)
A5 ` A1 (A5)
There is agreement between O and P on A4 and A5, but not on the sequents A5 ` A3, and A4 ` A2, and A2, A3 ` A1. Whether or not O accepts them is examined by Lorenzen dialogues for them further. O rst chooses such a d-sequent which constitutes the given WB-dialogue, and then P starts a Lorenzen dialogue for the d-sequent designated by O. Note that the d-sequent ` [A] designated by O is that whose validity is challenged by O. That is, O considers that A is false even if is true. Thus, as it is in GKD, is a set of formulas (tentatively) asserted by O, and [A] is a formula to be defended by P .
why-because dialogue We de ne our WB-dialogue, and then, by combining with our GKD, we de ne Lorenzen dialogue with why-because dialogue GKDwb. Although the general form of a d-sequent is of the form [⇧] , ` ⇤ , [] , it is su cient for WB-dialogue to consider a particular form ` [A], where [⇧] and ⇤ are empty, and [] is restricted to a single formula.
De nition 4.2. An md-sequent M is a sequence of d-sequents of the form are connected by , de ned inductively as follows. ` [A], which
S2 S1.
We call every d-sequent that constitutes an md-sequent M a component sequent of M.
For appropriate d-sequents S1, . . . , Sn, an md-sequent is of the form (Sn (· · · (S3 (S2 S1)) · · · )); hence, we usually omit the parentheses of an md-sequent, and write as Sn · · · De nition 4.3. O’s why-move and P ’s because-move are de ned as follows. O’s why-move: For any md-sequent M, where a component sequent A, ` [C] appears, O extends M to the md-sequent ((` [A]) M ) by connecting the d-sequent ` [A]. In particular, when M is empty (at the beginning of a dialogue), O puts the d-sequent ` [A] for a formula A (chosen by P ).
P ’s because-move: For any md-sequent M, where a component sequent ` [A] with the empty context appears, P replaces it by ` [A] by adding any non-empty formulas to the component sequent.
To set up the end of a dialogue, we introduce a set of formulas B called the basis of a WBdialogue, that O and P agree are true. By its nature, O cannot ask why to every formula B 2 B . When all antecedents not asked by O of all component sequents of a WB-dialogue are belongs to B, the dialogue ends. However, neither P nor O wins at that point, and who wins the dialogue is determined by Lorenzen dialogues for all component d-sequents of the WB-dialogue that follow.
De nition 4.4. Let B be a given set of formulas called the basis. A WB-dialogue is a sequence of moves satisfying the following conditions.
1. P rst chooses a formula A and claims it, and thereafter, moves of O and P alternately appear. 2. Every occurrence of a formula is asked by an O’s why-move at most once. 3. O cannot apply a why-move to any formula B 2 B .
4. A dialogue ends when O cannot continue the dialogue with another why-move. A WB-dialogue is that for A, when P ’s rst claim is A.
We identify a WB-dialogue and the resulting md-sequent M.
Note that the above condition (2) is de ned for occurrences of a formula. The same formula may be provided as ground by P several times, and in such a case, O should ask why for all occurrences of that formula, not once collectively.
P may end a WB-dialogue at any time by choosing formulas of B as required grounds. We consider the purpose of a WB-dialogue is the investigation of appropriate grounds or lemmas, by P and O working cooperatively, to establish a given proposition.
We de ne GKDwb by combining GKD and WB-dialogue.
De nition 4.5. A dialogue of GKDwb for A consists of the following two stages.
2. The second stage consists of dialogues of GKD for all component sequents of M chosen by O.
A dialogue of GKDwb is won by P if all dialogues of GKD at the second stage are won by P . De nition 4.6. A strategy of GKDwb for A is a sequence of strategies of GKD for all component sequents of a WB-dialogue M for A constructed at the rst stage of the dialogue.
A strategy of GKDwb is winning if every strategy of GKD thereof is winning.
Note that since we consider a set of strategies of GKD as a strategy of GKDwb, the validity of formulas in GKDwb is reduced to that in GKD. Thus, the valid formulas are common in GKD and GKDwb, while GKDwb has a higher expressive power than GKD.
We investigate a correspondence between our dialogue GKDwb and our sequent calculus GK + cut. We extend GK + cut by introducing non-logical axioms of the form ` B for all B 2 B for a given basis B. We rst show that there is a one-to-one correspondence between a WB-dialogue and a successive applications of cut called a cut-string in GK + cut.
De nition 4.7. In GK + cut, a path of a proof-tree that consists only of successive applications of cut is called a cut-string.
In the following, for any multisets 1, . . . , n of formulas, by S n, we denote 1 [ · · · [ n, where [ is the multiset union. 1 \ {A1, . . . , An} is the multiset di erence. For example, {A, A, B} [ { A, C} = {A, A, A, B, C} and {A, A, B} \ {A} = {A, B}.
De nition 4.8. In the construction of a WB-dialogue, except for the rst P ’s claim, every successive pair of an O’s why and a P ’s because moves is called an OP -pair. Furthermore, a sequence of OP -pairs, in the order in which they appear in the given WB-dialogue, is called an OP -sequence.
Lemma 4.9. Let any d-sequent ` [A] in GKDwb be identi ed with a sequent ` A in GK. Then, for any OP -sequence M, there exists a cut-string consisting of all component sequents of M.
Proof. Let M be an OP -sequence ( n ` [An]) · · · ( 2 ` [A2]) ( 1 ` [A1]). We show that M corresponds to the following cut-string by induction on the length l the number of OP -pairs of the given OP -sequence.
2 ` A2 1 ` A1 (A2) S 2 \ { A.2} ` A1 . .
. n ` An S n 1 \ {A2, . . . , An 1} ` A1 (An)
S n \ {A2, . . . , An} ` A1 (Base step) When l = 2, the given OP -sequence is of the form ( 2 ` [A2]) ( 1 ` [A1]), and it corresponds to the following cut.
2 ` A2 1 ` A1 ( 1 [ 2) \ {A2} ` A1 (A2) (Induction step) When l > 2, the given OP -sequence is of the form ( l ` [Al]) ( l 1 ` [Al 1]) · · · ( 1 ` [A1]), and it corresponds to the following cut-string, by applying the induction hypothesis IH. .
... IH l ` Al
S l 1 \ {A2, . . . , Al 1} ` A1 (Al)
S l \ {A2, . . . , Al} ` A1 Note that by the de nition of the OP -sequence, we have Al 2 S l 1 \ {A2, . . . , Al 1}; hence, the above cut (Al) is applicable.
When the given OP -sequence is a WB-dialogue, the above S n \ {A2, . . . , An} is the formulas {B1, . . . , Bm} of the basis B. Hence, by applying cut with non-logical axioms, we obtain the following cut-string.
` Bm
` A1 ` B1 S n \ {A2, . . . , An} ` A1 (B1) S n \ {A2, . . . , A.n} \ {B1} ` A1 . .
.
Bm ` A1 (Bm)
The converse of the lemma is shown in the same way, by induction on the length of a given cut-string.
Note that a strategy of GKDwb is de ned as a sequence of strategies of GKD. As discussed in the end of Section 3.2, there is a correspondence between winning strategies of GKD and sequent calculus proofs in GK. Thus, by combining the above Lemma 4.9, we obtain the following theorem.
Theorem 4.10. If there exists a winning strategy of GKDwb for A, then there exists a proof of ` A in GK + cut.
Example 4.11. Let us illustrate the following dialogue of GKDwb, which is a modi cation of
the example given in [
1. P : My car is safe. 2. O: Why is your car safe? 3. P : Because my car has an airbag, and if my car does not have an airbag then it isn’t safe. 4. O: Why if your car does not have an airbag then it isn’t safe? 5. P : Because if my car does not have any airbag then I may die in an accident, and if I may die in an accident then my car isn’t safe.
Let “my car is safe” be S, “my car has an airbag” be A, and “I may die in an accident” be B. Let the basis B be {¬A ! B, B ! ¬ S, A}. Then, the above dialogue is represented by the following WB-dialogue.
(¬A ! B, B ! ¬ S ` [¬A ! ¬ S]) (¬A ! ¬ S, A ` [S])
By conducting Lorenzen dialogues further, we obtain the following dialogue of GKDwb. Since we consider only ^ and ¬ in this article, we translate the above formulas as follows. ¬A ! B ⌘ ¬ (¬A ^ ¬ B), B ! ¬ S ⌘ ¬ (B ^ S), ¬A ! ¬ S ⌘ ¬ (¬A ^ S). In the following dialogue, to save the space, we omit formulas duplicated in an application of a move in GKD.
(P wins) (P wins) (P wins)
AA, ,¬¬A(,B¬^(BS^ ) `S)A` P a¬ ¬¬AA^ ^ SS,,BB``[BB] P d SS `` [SS,,[¬¬BB]] P d ¬[(¬¬B¬AAA^],,,¬S¬¬()((B,BB¬^ ^^ASSS^)))S````[[¬¬¬[AA¬A]A]OP]OadP¬da^ ¬¬AA ^^ SS ``¬¬[(¬BBBA,,¬^^[BBSS]]),`PO¬daBA¬^^ SS¬, A`[[¬S[^B¬]`BS]][`SP,[S¬a,B¬¬]BO]dPOaaA^^(P,Alo`se[sS) ] ¬(¬¬(AB^ ^¬ SB),)¬,¬A(^B S^ `S)¬, A¬ A^¬^ BS ` P a¬ Oa^ AA `` [¬¬AA,,[SS]] POda¬ A(P`lo[Sse,sS)] ¬(¬A ^ ¬ B), ¬(B ^ S) ` ¬(¬A ^ S) Oa¬ A ` ¬A ^ S, [S] (¬(¬A ^ ¬ B), ¬(B ^ S) ` [¬(¬A ^ S)]) P d (¬(¬A ^ S), A ` [S]) P a¬ Oa^
Since P loses the dialogue for ¬(¬A ^ S), A ` [S], and there exists no winning strategy thereof, the rst P ’s claim S (“My car is safe.”) cannot be justi ed.
Since our investigation in this article is a rst step toward applying proof theory to the study of
argumentation, there are many possible future work. Among others, we will extend our sequent
calculus representation to the full fragment of Lorenzen-Hamblin Natural Dialogue LHND [