The
Dialogical Dynamics of Adaptive Paraconsistency
*
Abstract
The dialogical approach
to paraconsistency as developed by Rahman and Carnielli ([1]), Rahman and Roetti ([2]) and Rahman ([3], [4] and [5]) suggests a way of studying the dynamic
process of arguing with inconsistencies.
In his paper on
Paraconsistency and Dialogue Logic ([6]) Van Bendegem suggests that an adaptive version of paraconsistency is the natural way of capturing the inherent
dynamics of dialogues. The aim of this paper is to develop a formulation of
dialogical paraconsistent logic in the spirit of
an adaptive approach and which explores the possibility of eliminating inconsistencies
by means of logical preference strategies.
Introduction
The dialogical approach
to paraconsistency as developed by Rahman and Carnielli ([1]), Rahman and Roetti ([2]) and Rahman ([3]), ([4]) and ([5]) suggests a way of studying the
dynamic process of arguing with inconsistencies.
In his paper on
Paraconsistency and Dialogue Logic ([6]) Van Bendegem, who supports the dialogical approach to paraconsistency, argues however that Rahman-Carnielli's
formulation defeats the aim of a general dynamic structure of dialogical paraconsistent logics because their formulation uses a paraconsistency rule which applies not only to arguments containing
inconsistent formulae but also to arguments where no inconsistent formulae
occur. Van Bendegem suggests that an adaptive version
of paraconsistency is the natural way of capturing
the inherent dynamics of dialogues. In fact, Diderik Batens proposed in his paper
A survey of inconsistency-adaptive logics
([7]) that the study of adaptive logic should be carried out in the context
of argumentation.
The aim of this
paper is to develop a formulation of dialogical paraconsistent
logic in the spirit of an adaptive approach and which explores the possibility
of eliminating inconsistencies by means of logical preference strategies.
1 The Dialogical Literal Approach to
Paraconsistency and its Problems
1.1 Literal
Paraconsistency
One way to formulate
paraconsistent logic within the dialogical approach
as developed in Rahman and Carnielli ([1]), Rahman and Roetti ([2]) and Rahman ([4]) can
be achieved in the following way. Assume that to the structural rules of the
standard dialogical logic
[i]
we add the following:
·
Negative
Literal Rule:
The
Proponent is allowed to attack the negation of an atomic (propositional) statement
(the so called negative literal)
if and only if the Opponent has already attacked the same statement
before.
This structural
rule can be considered in analogy to the formal rule for positive literals.
The idea behind this rule is the following: An inconsistency of the Opponent
may be tolerated by using a type of charity principle. The inconsistency might
involve different semantic contexts in which, say, a
and Øa have been asserted. Now, if the Opponent attacks Øa with a he concedes thereby that there is some
common context between Øa and a which
makes an attack on Øa possible. This allows the Proponent to attack the
corresponding negation of the Opponent.
In Rahman and Carnielli ([1]) the logics
produced by this rule were called Literal
Dialogues, or shorter: L-D. In order to distinguish between the intuitionistic and the classical version Rahman and Carnielli wrote L-Di (for the intuitionistic
version) and L-Dc (for the classical version). To be precise we
should call these logical systems literal dialogues with classical structural
rules and literal dialogues with intuitionistic
structural rules respectively.
In L-D the (from
a paraconsistent point of view) dangerous formulae
(aÙØa)®b, a®(Øa®b) and (a®b)®((a®Øb)®Øa) are not valid.
Let us see the corresponding literal dialogues in L-Dc for the
first one:
|
O |
P |
|
|
|
|
(1) aÙØa 0 (3) a (5) Øa The Opponent wins |
(aÙØa)®b (0) 1 ?L
(2) 1 ?R
(4) |
The Proponent loses
because he is not allowed to attack the move (5) (see negative literal rule).
In other words the Opponent may have contradicted himself, but the semantic
context of the negative literal is not available to the Proponent until the
Opponent starts an attack on the same negative literal ¾ an attack which in this case
will not take place.
All classically
valid formulae without negation are also valid in L-Dc. All intuitionistically valid formulae without negation are also
valid in L-Di. As in da
Costa's system C1 neither of the following is valid in L-Dc:
|
(aÙØa)®b |
|
(a®(bÚc))®((aÙØb)®c) |
|
(aÙØa)®Øb |
|
((a®Øa)Ù(Øa®a))®Øb |
|
Ø(aÙØa) |
|
((aÙb)®c)®((aÙØc)®Øb) |
|
a®ØØa |
|
((aÚb)ÙØa))®b |
|
(a®b)®((a®Øb)®Øa) |
|
aÚb)®(Øa®b) |
|
((a®b)Ù(a®Øb))®Øa |
|
(a®b)®(Øb®Øa) |
|
((Øa®b)Ù(Øa®Øb))®a |
|
(a®b)Ú(Øa®b) |
|
Øa®(a®b) |
|
(ØaÚØb)®Ø(aÙb) |
|
Øa®(a®Øb) |
|
(ØaÙØb)®Ø(aÚb) |
|
a®(Øa®b) |
|
(ØaÚb)®(a®b) |
|
a®(Øa®Øb) |
|
(a®b)®Ø(aÙØb) |
|
((a®Øa)Ù(Øa®a))®b |
|
a®((ØaÚb)®b) |
In L-Di all the intuitionistically
non-valid formulae have to be added to the list, for example:
ØØA®A AÚ(A®B)
AÚØA AÚ((AÚB)®B)
((A®B)®A)®A
Ø(A®B)®A
Validity is defined
in dialogical logic via winning strategies for the Proponent. A systematic
description of the winning strategies for these logics can be obtained from
appropriate tableau systems.
[ii]
The extension of literal dialogues for propositional logic
to first-order quantifiers is straightforward: We only have to extend the
structural negative literal rule to elementary statements of first-order logic.
[iii]
Now we shall consider
the problems.
1.2 Problems
of the Literal Approach
The large number
of non-valid formulae listed above suggests that the literal approach presented
is too restrictive. There are many formulae in this list we would like to
have as valid. A further problem is what to do with inconsistencies between
complex propositions. One could argue that contradictions which cannot be
carried on at the literal level should be released of paraconsistency
restrictions ¾ this was defended
in Rahman ([3], [4] and [5]) where a distinction
between internal or de re and external
or de dicto
negation was introduced. One can also follow another complementary strategy
and introduce a device combining two types of restrictions, one applying to
the literal case and the other to the complex case. Thus, it looks like more
has to be done than just introducing a structural rule restricting the use
of negations. One first idea is to introduce an adaptive extension of the
literal negative rule making use of the dynamics of argumentation. That is,
one argues consistently as long as possible and when necessary adapts to the
specific inconsistencies that occur. In other words, the consistency of all
sentences is presupposed unless and until proven otherwise (cf. Batens
[7], 1). This fits nicely with the problem of complex inconsistencies: If
one analyses the complex inconsistency until the literal level has been reached
and no inconsistency occurs, then one continues using a non-paraconsistent
framework. But as remarked by Max Urchs the adaptive
logic of Batens has another deep and appealing contribution
to paraconsistency: What is really dangerous is
not inconsistency as such, but contradictions
(the latter are also called explosive
inconsistencies) ([8]). Overlooking such a distinction leads to a uniform
treatment of some types of formulae which should be kept apart ¾ e.g. the inconsistency which
can occur in a dialogue for disjunctive syllogism or de Morgan should be distinguished
from the inconsistency produced by ex falso sequitur
quodlibet. The idea is that if you have an inconsistency
in the premises you can either isolate it and continue with the rest or take
that part of the inconsistency which is necessary for the proof ¾ this strategy has been called
by Batens the logical preferential mechanism ¾ in contrast to the non-logical
preferential mechanisms of standard non-monotonic logics. Now what distinguishes
inconsistencies from contradictions? Our proposal is the following: While
contradictions (i.e. explosive inconsistencies) in the concessions of an argument
make at least one defensive or aggressive move redundant, non-explosive inconsistencies
do not. That is why contradictions lead in this approach to the paraconsistent
non-validity of those formulae in which they occur. Moreover, some parts of
the (non-explosive) inconsistencies can be used for the defence of the argument
(the other parts can be dismissed). Thus, an appropriate concept of redundancy
should be introduced here. This is the line we are going to follow in this
paper.
2 The Dialogical Way to
Adaptive Paraconsistency
at the Game Level
As mentioned above,
we introduce here a redundancy concept which can be applied in order to distinguish
between non-explosive inconsistencies and contradictions. Clearly, this procedure
should be understood adaptively. That is, if no inconsistencies are present,
use the standard definition of dialogical validity (see the appendix). If
inconsistencies appear, restrict the definition of validity by means of the
redundancy principle.
2.1 Formulae Which are Paraconsistently
Free of Redundancies:
Dialogical Adaptivity
We will present
here one concept of redundancy which is a variation of some ideas on dialogical
relevance logic developed in Rahman and Rückert [9]. In fact other versions based on relevance considerations
introduced in the above-mentioned paper could also be applied. We have chosen
this version because it seems more inherent to the paraconsistent point of view in the sense that it stresses
the point of having inconsistency without triviality.
The idea behind
our dialogical approach to adaptivity is that in
the case an inconsistency occurs the Proponent can try one of the following
procedures:
i) He may try to win by isolating the inconsistency.
That is, he will just ignore it and continue with the rest. If he can answer
all the attacks of the Opponent anyway the inconsistency was redundant and
he is through.
ii) He may try to win using only one part of the inconsistency
and continue with the rest just as in i.
iii) He may try to win using the inconsistency and ignoring the
rest of the moves of the Opponent.
We will say that
the inconsistency is explosive and the thesis not paraconsistently
valid iff the third case is the only successfully
proceeding available. Shorter, we call explosive such inconsistencies which
make a defensive move redundant.
Now, what happens
in the case of a negation occurring in the then-part of a conditional, as
in (aÙØa)®Ør? Well, if nothing
is added we obtain a minimal logic; if we want more than minimality then here again various options are available.
We will discuss an option which tolerates inconsistencies, does not lead to
triviality but renders the principle of non-contradiction as valid. The idea
is that a non-explosive inconsistency should not make any defensive move redundant,
that is, the Proponent has to use all his defensive moves. (Counterattacks
resulting from an attack on negations are considered to be defensive moves.)
Suppose the Proponent states the thesis Ø(aÙØa). The Opponent
will attack with move (m)(aÙØa). The Proponent
should now use this move. Now, this leads to an awkward formulation where
two types of structural rules have to be distinguished: one applying to attacks
and the other to counterattacks. A more general approach results from the
following considerations: Suppose, on
one hand, that the Proponent notices that he can win without using (or with
only one part of) the inconsistency which appears in a conjunction stated
by the Opponent, then he should be allowed to attack only one part of this
conjunction. Suppose, on the other hand, that the Proponent notices that he
can win without using (or with only one part of) the inconsistency which appears
in a disjunction stated by himself, then he should be allowed to defend only
one part of this disjunction
Thus, if an inconsistency
in the concessions occurs, the Proponent must attack each formula at least
once, use all the atomic formulae of the Opponent and defend himself against
all attacks. It is time to be a little more precise:
DEFINITION
1: O-Variants: Any possible development of a dialogue as determined by
the choice of the Opponent constitutes a variant. Thus, the developments of
a dialogue as determined by the choice between attacks ?L and ?R, or ?R after
L? on a conjunction, the different possible defences of a disjunction (left
or right side) and the choice between defence and counterattack while reacting
to an attack on a conditional are said to be different O-variants.
DEFINITION
2: O-Inconsistency: It is said that
an O-inconsistency occurs iff
1.
The Opponent stated (n)A, Ø(m) A, where n and m signalise the numbers of the
respective moves and A is a formula.
2.
The Opponent stated a negative refutable formula
(like Ø(AÚØA); Ø(A®A))
Notice that here
we make paraconsistency for complex formulae possible.
Clearly, a more restrictive definition applying to literals is possible.
If we want to put the idea of adaptivity into practice we need to precise the notion
of used
1.
An atomic O-formula has been used iff the Proponent states this formula in order to state an
aggressive (=attack) or a defensive move.
2.
A complex formula A has been used iff all the aggressive and
defensive moves related to A have
been stated according to the conditions stated by definition 3 (below).
DEFINITION
3: A formula is said to be free of paraconsistent
redundancies iff
the Proponent wins under the standard structural rules and he can win under the following conditions:
1. He can attack every O-formula at least once (e.g. he can win
with only one of the possible attacks on a conjunction) in any of the possible
O-variants (not necessarily in the same O-variant).
2. He can defend himself at least once against all attacks (e.g.
he can win defending only one part of the disjunction) in any of the possible
O-variants (not necessarily in the same O-variant)
3. He can use at least one occurrence of any atomic O-formula
in any of the possible O-variants (not necessarily in the same O-variant).
DEFINITION
4: A formula is said to contain
paraconsistent redundancies iff
the Proponent cannot win without dismissing at least one of the conditions
stated before.
We will tag all
attacked O-formulae and all atomic O-formulae used. We do not need to tag
the defences because they can be recognised by the closed rounds – see appendix.
Now the definition
of formulae which are valid by adaptation:
DEFINITION
5: A formula in the dialogical proof
of which an inconsistency occurs is valid
by adaptation if this formula is valid by the standard definition of validity
and is free of paraconsistent redundancies. Inconsistencies
occurring in the dialogical proof of formulae not paraconsistently free of redundancies are called explosive inconsistencies or contradictions.
Let us study some
examples. In example 1 of chapter 1.1 (played in standard dialogical logic)
it is clear that the inconsistency occurring in the concessions (O-formulae)
is explosive: The Proponent wins according to the standard definition of validity,
but there is no variant where the Proponent can win by stating the (redundant)
defence b. In the next two examples
the inconsistencies do not collapse into contradictions.
Example 2
|
O |
P |
|
|
|
|
(1) Øa 0Ö (3) a 2 (5) aÙb 4Ö (7) a Ö Ä |
Øa®(a®Ø(aÙb))
(0) a®Ø(aÙb)
(2) Ø(aÙb)
(4) Ä 5 ?L
(6) 1
a |
Because of the inconsistency
occurring in 1, 3 the Proponent plays adaptively. In doing so, in a first
stage he ignores the inconsistency. Then he uses move 7 (or move 3) to attack
Øa and wins. Moreover, since there is no other variant
to be considered the formula is valid.
It should not be
difficult for the reader to check that neither Øa®(a®b) nor (ØaÙa)®b hold and that Ø(ØaÙa), Øa®(a®Øa), (ØaÙa)®a
and (a®ØØa) hold.
The next example
will lead us to determine how to check whether a given formula is redundant.
In this example two variants have to be considered. In order to keep track
of the possible redundancies at the game level we will introduce subdialogues
(the tableau system due to be introduced later will include all the variants,
but at the strategy level).
[iv]
The idea is quite simple. Suppose that at a given stage
of the dialogue, the Opponent, who stated an inconsistency realises that he
loses by the standard rules but he realises too that one defensive move has
been dismissed. He then can ask something like: Well, I will lose in this
way, but what about, say, the defensive move b?
(shorter ?b)
You did not show me that I can win using that. In this case the Proponent
will open a subdialogue where he will have to show
that he can win with the move challenged. Now, it can be the case that the
Proponent says: I can win using b,
but I will use it only if in your variant (i.e., the O-variant) you choose,
say, the right part ¾ notice that this
is a consequence of condition 3 of definition 3 which states that the Proponent
can use one of the defensive answers in only one of the O-variants. This can
be formulated with a new structural rule:
R5
(subdialogues): The Opponent may at a given stage
m of the dialogue ask for some
unused formula which has been dismissed so far and which should be used according
to definition 3. The Proponent will have to defend this challenge by asking
the Opponent to develop all of his O-variants by means of subdialogues. Those formula of the initial dialogue which
define the O-variant can be used in the subdialogue.
Example
3
|
O |
P |
|
(1) (aÚb)ÙØa 0Ö (3) aÚb Ö (5) a Ö (7) Øa Ö |
((aÚb)ÙØa))®b (0)
1 ?L (2) 3 ? (4) 1 ?R (6) 7 a
(8) |
At this stage, where
the Opponent is going to lose he realises that round 1 is still open. O then
asks for a response to 1 and
P will ask O to open a subdialogue for the right-side variant of the defence to the
attack 4. In this subdialogue P will show that b is not redundant because if the Opponent
chooses b at move 5 he will answer
the attack of move 1 and win. Thus the dialogue now looks as follows:
|
O |
P |
|
(1) (aÚb)ÙØa 0Ö (3) aÚb Ö (5) a Ö (7) Øa Ö Ä (9) ?1
Ö |
((aÚb)ÙØa))®b (0) b
(12) 1 ?L (2) 3 ? (4) 1 ?R (6) 7 a
(8) 3 ?b
(10) |
O
|
P |
|
(11) b |
|
At move 9 the Opponent
asks for the round opened at move 1. The Proponent counterattacks by asking
for the O-variant b in the defence
of the disjunction. After this counterattack the Proponent uses b to close the opened round. Actually we
could rewrite all the variant again but we dispense with doing so by allowing
jumping from the subdialogue to the initial dialogue.
Notice that a clever
Proponent will always try to play classically because the adaptive rules restrict
his own moves and not the moves of the Opponent. Thus, the Opponent will try
to state an inconsistency as fast as he can in order to play paraconsistently. For example, in the dialogue for ((ØaÚb)Ùa))® a the Proponent will
not try to produce the O-inconsistency Øa, a. He will instead attack the right part
of the conjunction obtaining a and
then he will immediately close the first round using precisely this a and win.
2.2 Quantifiers
and Ontological Adaptivity
The quantifiers
do not in this approach present any special problems in relation to inconsistencies.
But there are some interesting considerations about the ontological status
of inconsistencies. Actually there are two main interpretations of paraconsistency
possible. The one, called the compelling
interpretation, stresses that paraconsistent theories are ontologically committed to inconsistent
objects. The other, called the permissive
interpretation, does not assume this ontological commitment of paraconsistent theories. Da Costa
formulates this latter approach in the following way:
I suggest to address the inconsistency
issue differently. We may well explore the rich representational devices allowed
by the use of paraconsistency in inconsistent domains,
but withholding any claim to the effect that there are 'inconsistent objects'
in reality. (Da
Costa [14], 33).
This allows for the accommodation of
inconsistency by acknowledging that it is not a permanent feature of reality
to which theories must correspond, but is rather a temporary aspect of such
theories [...]. In this view, to accept a
theory is to be committed, not to believing it to be true per se, but to holding
it as if it were true, for the purposes of further elaboration, development
and investigation. (Da Costa, Bueno and French [15], 616-617).
In Rahman ([4] and [5]) a logic was developed in which the temporary
acceptance of inconsistencies will be abandoned as soon as the singular terms
occurring in the elementary propositions producing these inconsistencies are
ontologically committed. In other words, the Proponent concedes the Opponent's
inconsistency AtÙØAt iff
the constant t carries no ontological
commitment. Actually we are not only differentiating between explosive and
non-explosive inconsistencies: we propose here to distinguish between inconsistencies
which are ontologically committing and those which are not. This distinction
can be considered in the context of Da Costa's epistemology
of quasi truths. The idea is the following. It could well be that, say,
Bt has somehow been
verified in reality and thus we commit ontologically with it and reject ØBt But it could also happen that
there is no verification either of At or of ØAt and according to
our theory it seems we should concede At and ØAt In this case, though
we will concede it, we will not take this concession as being ontologically
committed.
The introduction
of ontologically committing quantifiers can be achieved through the following
definition and a new structural rule:
DEFINITION
6: A constant t is said to be introduced with ontological commitment by X
if
(1) X states a formula A[t/x] to defend ÚxA or
(2) X attacks a formula Ùx A with ?n/t, and t has not been used in the same
way before.
R6
(formal introduction of constants): P may not introduce constants with ontological
commitment: any such constant must first be introduced by O according to definition
6. (cf. [16])
The intuitive idea behind the ontologically committing quantifiers should
be clear: The Proponent is allowed to use a constant for a defence (of an
existential quantifier) or an attack (on a universal quantifier) iff the Opponent has already conceded that this constant has
ontological commitment by an attack (on a universal quantifier) or by a defence
(of an existential quantifier).
This logic also
contains the quantifiers $ and " for which neither
definition 6 nor R6 hold. Since the quantifiers of $ and " are ruled by the standard
and structural rules it looks like these quantifiers work as in the standard
logic. Actually they are very different: here they work as quantifiers without any ontological commitment at all.
In the standard logic the ontological commitment is presupposed by the use
of these quantifiers. Here this is not the case.
Our adaptive rule
for quantified adaptive paraconsistent logic is
the following:
R7
(ontological adaptivity): If an O-inconsistency
occurs and its constants were not introduced according to definition 6 and
R6, replace these quantifiers with $ and " and run an adaptive
dialogue as described in the definitions 1 to 5. Proceed classically otherwise.
Example 4
|
O |
P
|
|
(1) Ùx((AxÚBx)ÙØAx)) 0Ö (3) ?
2Ö (5)
(AtÚBt)ÙØAt (7) AtÚBt (9) At (11) ØAt |
(Ùx((AxÚBx)ÙØAx)))® Úx(ØØBxÚCx) (0) Úx(ØØBxÚCx) (2) 1 ?t
(4) 5 ?L (6) 7 ? (8) 5 ?R (10) |
At moves 9 and 11
an O-inconsistency occurs. The Proponent will concede the inconsistency and
thus, run an adaptive dialogue, but he will not take it as ontologically committing:
|
O |
P
|
|
(1) "x((AxÚBx)ÙØAx)) 0Ö (3) ?
2Ö (5)
(AtÚBt)ÙØAt (7) AtÚBt (9) At (11) ØAt Ä (13) ?3
Ö |
("x((AxÚBx)ÙØAx)))®$x (ØØBxÚCx) (0) $x (ØØBxÚCx) (2) ØØBtÚCt (16) 1 ?t (4) 5 ?L (6) 7 ? (8) 5 ?R (10) 7 At (12) 7 ? Bt (14) |
|
O |
P |
|
(15) Bt Ö 17) ?
16Ö (19) ØBt 18Ö Ä The Proponent wins
|
ØØBt (18) Ä 19 Bt (20) |
Now it could well
be that we do not want to replace every quantifier automatically. It could
be the case that some formulae in which these quantifiers occur are known
to have an empirical verification and thus should be read as ontologically
committing. In fact, the different quantifiers allow us to think about different
possible combinations between types of quantifiers. We could, as already mentioned,
study the possibility that not all of the quantifiers lose their ontological
commitment. This would allow one part to have ontological commitment and the
other not. In this case we could, for example, proceed with an anti Meinongian point of view and give priority to the existent.
That is, we could understand that if one part of the inconsistency carries
ontological commitment the inconsistency cannot hold anymore because this
part will be considered to be verified and we should proceed classically.
This can be made explicit by copying the quantifiers with ontological commitment
in the P-column at the start of the dialogue:
Example 5
In this example
we will not go into the process of replacing. We will instead replace at the
start what has not been conceded as ontologically committing:
|
O |
P |
|
|
[Not committing quantifer:
ÙxØ(AxÙBx)] |
|
(1) "x(ØAxÙAx) 0Ö (3) ?t 2Ö (5) AtÙBt 4Ö (7) At Ö (9) ØAtÙAt Ö (11) ØAt Ö Ä |
"x(ØAxÙAx)® Ùx Ø(AxÙBx) (0) ÙxØ(AxÙBx) (2) Ø(AtÙBt) (4) Ä 5 ?L (6) 1
?t (8) 9
?L (10) 11 At (12) |
Another possibility
due to be explored is to introduce many quantifiers with different grades
of ontological commitment or verification. Furthermore it could be that we
have a hierarchy of quantifiers corresponding to grades of confirmation. We
could in this case require that if a constant of level n has been introduced with the
help of quantifiers of level m<n then this constant should
be considered as having ontological commitment in m. More precisely, think of
the first pair of quantifiers as having the upper index 0 and add new pairs
of quantifiers with higher indices, as many as we need to express every type
of (verified) reality (or fiction) that could possibly appear. The extended
set of quantifiers requires a new notion of introduction.
·
A constant t is said to be introduced with ontological commitment as belonging
to the type i iff
it is used to attack a universal quantifier of type i
or to defend an existential quantifier of type i
and has not been used in the same way before.
·
For each type of quantification the following
rule holds: Constants may only be introduced by O.
Now the hierarchy:
·
P may introduce a constant t with ontological commitment
on a level m iff O has introduced t in the same way on some level
n with n<m before.
2. (Ú1xAx Ù Ùx2(Ax®Bx)) ® Ú1xBx
Thus, in our paraconsistent context we could
think of applying the following rule:
·
if an O-inconsistency occurs at level m, check first whether the corresponding
constants have been introduced at level n<m.
If constants have
been introduced in n two procedures
are possible:
1. stay at level m, ignore this, and
use an adaptive paraconsistency,
2. stay at level m, proceed classically
for the inconsistency with constants introduced at level n but paraconsistently
with the rest of the inconsistencies of level m. After doing so jump to another
level.
The jumps might be regulated by subdialogues.
The choice between procedures 1 and 2 could be part of the agreements either
at the very start or, more dynamically, during the dialogue. Here many details
have to be fixed, for example: what happens if one constant is ontologically
committed but for a given predicate different from those defining the O-inconsistency?
We will leave this and other related problems for a future research where
we will study the combination of the hierarchy of quantifiers with Newton
da Costa's theory of partial truth.
Now although we
believe that all this is congenial to the spirit of adaptive logic our approach
does not seem to agree exactly with the present adaptive systems developed
in
3 Winning Strategies
As already mentioned, validity is defined in dialogical logic via winning
strategies of P, i.e. the thesis A
is logically valid iff P can succeed in defending
A against all possible allowed criticism
by O. In this case, P has a winning
strategy for A. A systematic
description of the winning strategies available can be obtained from the following
considerations:
If P is to win against any choice of O, we will have
to consider two main different situations, namely the dialogical situations
in which O has stated a (complex) formula and those in which P has stated
a (complex) formula. We call these main situations the O-cases and the P-cases
respectively.
In both of these situations another distinction has to be examined:
1.
P wins by choosing
an attack in the O-cases or a defence in the P-cases, iff
he can win at least one of the dialogues
he can choose.
2.
When O can choose a defence in the O-cases or an attack in the P-cases, P can
win iff he can win all of the dialogues O can choose.
The closing rules for dialogical tableaux are the usual ones: a branch
is closed iff it contains two copies of the same
atomic formula, one stated by O and the other one by P. A tableau for (P)A (i.e. starting with (P)A) is closed iff
each branch is closed. This shows that strategy systems for classical and
intuitionistic logic are nothing other than the very well
known tableau systems for these logics.
For the intuitionistic
tableau system, the structural rule about the restriction on defences has
to be considered. The idea is quite simple: the tableau system allows all
the possible defences (even the atomic ones) to be written down, but as soon
as determinate formulae (negations, conditionals, universal quantifiers) of
P are attacked all other P-formulae will be deleted ¾ this is an implementation
of the structural rule RI4 for intuitionistic
logic. Clearly, if an attack on a P-statement causes the deletion of the others,
then P can only answer the last attack. Those formulae which compel the rest
of P’s formulae to be deleted will be indicated with the expression ”å[O]Ó which reads: in
the set å save O’s formulae and delete all of P’s formulae stated
before.
[v]
3.1 Classical
Tableaux
|
(O)-Cases |
(P)-Cases |
|
å, (O)AÚB |
å, (P)AÚB |
|
------------------------------- |
-------------------- |
|
å, <(P)?>(O)A | å, <(P)?>(O)B |
å, <(O)?>(P)A å, <(O)?>(P)B |
|
|
|
|
å, (O)AÙB |
å, (P)AÙB |
|
--------------------- |
------------------------------- |
|
å, <(P)?L>(O)A å, <(P)?R>(O)B |
å, <(O)?L>(P)A | å, <(O)?R>(P)B |
|
|
|
|
å, (O)A®B |
å, (P)A®B |
|
------------------------------- |
------------------- |
|
å, (P)A ... | <(P)A>(O)B |
å, (O)A; å,(P)B |
|
|
|
|
å, (O)¬A |
å, (P)¬A |
|
------------------ å, (P)A; Ä |
--------------- å, (O)A; Ä |
|
å, (O)ÙxA |
å,
(P)ÙxA |
|
-------------------- |
-------------------- |
|
å,
<(P)?t>(O)A[t/x] |
å,
<(O)?t>(P)A[t/x] t is new |
|
å, (O)ÚxA |
å, (P)ÚxA |
|
-------------------- |
-------------------- |
|
å,
<(P)?>(O)A[t/x] t is new |
å,
<(O)?>(P)A[t/x] |
By a dialogically signed formula we mean (P)X or (O)X where X is a formula. If å is a set of dialogically
signed formulae and X is a single
dialogically signed formula, we will write å, X for å È{X}. Observe that the formulae below the
line always represent pairs of attack and defence moves. In other words, they
represent rounds. Note that the expressions between the symbols "<"
and ">", such as <(P)?> or <(O)?> are moves
– more precisely they are attacks – but not statements.
3.2 Intuitionistic Tableaux
|
(O)-Cases |
(P)-Cases |
|
å, (O)AÚB |
å, (P)AÚB |
|
------------------------------- |
-------------------- |
|
å, <(P)?>(O)A | å, <(P)?>(O)B |
å, <(O)?>(P)A å, <(O)?>(P)B |
|
|
|
|
å, (O)AÙB |
å, (P)AÙB |
|
--------------------- |
------------------------------- |
|
å, <(P)?L>(O)A å, <(P)?R>(O)B |
å, <(O)?L>(P)A | å, <(O)?R>(P)B |
|
|
|
|
å,(O)A®B |
å, (P)A®B |
|
------------------------------- |
------------------- |
|
å, (P)A ... | <(P)A>(O)B |
å[O], (O)A; (P)B |
|
|
|
|
å, (O)¬A |
å, (P)¬A |
|
------------------ å, (P)A; Ä |
--------------- å[O], (O)A; Ä |
|
å, (O)ÙxA |
å,
(P)ÙxA |
|
-------------------- |
-------------------- |
|
å,
<(P)?t>(O)A[t/x] |
å[O], <(O)?t>(P)A[t/x] t is new |
|
å, (O)ÚxA |
å, (P)ÚxA |
|
-------------------- |
-------------------- |
|
å,
<(P)?>(O)A[t/x] t is new |
å,
<(O)?>(P)A[t/x] |
Let us look at two examples, namely one for classical logic and one for
intuitionistic logic. We use the tree shape of the
tableau made popular by Smullyan ([18]) and omit
the expressions between < and >:
Example 6
(P) ÙxØPx®ØPt
(O) ÙxØPx
(P) ØPt
(O) Pt
(O) ØPt
(P) Pt
The tableau closes.
The following intuitionistic tableau makes use
of the deletion rule:
Example 7
(P) ØØa®a
(O)[O] ØØa
(P) a
(P) Øa
(O)[O] a
The tableau remains open.
3.3 Winning
Strategies for Adaptive Paraconsistency as Tableaux
In order to introduce a tableau system for dialogical adaptively paraconsistent logic which captures the idea of redundancy
described above the rule for closing branches has to be reformulated.
For this aim we will use a notational system which makes use of the device
of tagging those formulae which have been used in the sense of our definition
of adaptive paraconsistency. More precisely:
Tagging Rule:
1. We will tag any O-atomic formula at least one
occurrence of which has been used to close at least one branch (and delete
the unused occurrences).
2. We will tag any O-conjunctive formula iff at least one of the conjuncts has been used in at least
one branch (and delete the unused conjunct).
3. We will tag any O-complex formula other than
a conjunction which has been used in at least one branch.
4. We will tag any P-atomic formula at least one
occurrence of which has been used to close at least one branch.
5. We will tag any P-disjunctive formula iff at least one of the disjuncts
has been used in one branch (and delete the unused occurrences).
6. We will tag any P-complex formula other than
a disjunction which has been used in at least one branch.
Now the instructions for developing an adaptive tableau:
·
If it is possible to close the tableau without
producing an inconsistency of the forms described in definition 6 use the
standard closing rules. If an inconsistency occurs develop the tableau completely,
tag the formulae according to the tagging rule and apply the following adaptive
rule.
·
A tableau
for (P)A (i.e. starting with
(P)A) is adaptively closed iff each branch is closed
by the standard closing rule and there are no untagged formulae.
Example 8
i) (P)(aÙØa)®Ø(aÙb)
ii) (O)(aÙØa)
iii) (P)Ø(aÙb)
iv) (O)aÙb
v) <(P)?L> (O)a
vi) <(P)?R> (O)b
vii) <(P)?R> (O)Øa
First we use the
standard rules and develop the tableau. In doing so we realise that lines
v and vii state an inconsistency. We then develop an adaptive strategy applying
the tagging rule. In doing so the Proponent deletes the redundant formula
b of the conjunction at move iv and the
redundant conjunct a of the conjunction
at move ii. The Proponent then uses the resulting atomic formulae to close
the branch and the tree:
i) (P)(aÙØa)®Ø(aÙb) Ö
ii) (O)(aÙØa) Ö
iii) (P)Ø(aÙb)
Ö
iv) (O)aÙb
Ö
v) <(P)?L> (O)a
Ö
vi) <(P)?R> (O)Øa Ö
vii) (P)a Ö
Example 9
i) (P)((aÚb)Ù Øa))®(ØØbÚc) Ö
ii) (O)(aÚb)ÙØa)
Ö
iii) (P) ØØbÚc Ö
iv) <(O)?> (P)ØØb
Ö
v) <(P)L?>(O)(aÚb)
Ö
vi) <(P)R?> (O)Øa)
Ö
vii) <(P)?>(O)a Ö½ viii) <(P)?>(O)b Ö
ix) (P)a Ö½ x) (O)Øb Ö
½ xi)
(P)b
Ö
Each branch is closed.
Moreover every formula has been tagged. Thus, everything that should be used
has been used and the tableau is adaptively closed.
As far as quantification
is concerned we will only suggest how to produce tableau systems with ontologically
committed quantifiers and leave the rest of the work to the reader:
Rewrite the rules
for the quantifiers in the following way:
|
(O)-Cases |
(P)-Cases |
|
å, (O)ÙixA |
å,
(P)ÙixA |
|
-------------------- |
-------------------- |
|
å,
<(P)?t*>(O)A[t/x] t has been
labelled with an asterisk before |
å[O], <(O)?t*>(P)A[t*/x] t is new |
|
å, (O)ÚixA |
å, (P)ÚixA |
|
-------------------- |
-------------------- |
|
å,
<(P)?>(O)A[t*/x] t is new |
å,
<(O)?>(P)A[t*/x] t has been labelled with an asterisk before |
DEFINITION
7: A constant t is said to be introduced with ontological commitment belonging
to the type i iff it has been labelled with an asterisk
by the use of quantifiers of the type i.
4 Final Remarks
As suggested in the text, several logics which we did not describe may
be introduced by changing the notions of redundancy, namely, not allowing
any occurrence of an atomic formula to be left unused, not allowing any O-formula
to be left unused and not allowing any P-formula to be left unused. This could
be combined with the option literal versus complex inconsistencies. Several
others result from combining these logics, with the idea of ontological adaptivity.
Neither did we explore how to combine the logical way of eliminating inconsistencies
by redundancy with a material strategy for establishing preferences. We will
leave this for future research.
5
Appendix:
A
Brief Introduction to Dialogical Logic
Dialogical logic, suggested by Paul Lorenzen
in 1958 and developed by Kuno Lorenz in several
papers from 1961 onwards,
[vi]
was introduced as a pragmatic semantics for both classical
and intuitionistic logic.
The dialogical approach studies logic as an inherently pragmatic notion
using an overtly externalised argumentation formulated as a dialogue between two parties taking up
the roles of an Opponent (O in the
following) and a Proponent (P) of
the issue at stake, called the principal thesis
of the dialogue. P has to try to defend the thesis against all possible allowed
criticism (attacks) by O, thereby
being allowed to use statements that O may have made at the outset of the
dialogue. The thesis A is logically
valid if and only if P can succeed in defending A against all possible allowed criticism by O. In the jargon of game
theory: P has a winning strategy
for A. We will now describe an intuitionistic and a classical dialogical logic.
Suppose the elements and the logical constants of first-order language
are given with small italic letters (a,
b, c, ...) for elementary formulae, capital italic letters for formulae
that might be complex (A, B, C,
...), capital italic bold letters (P,
Q, R, ...) for predicators and ti for constants.
A dialogue is a sequence of formulae of this first-order language that are
stated by either P or O.
[vii]
Every move ¾ with the exception
of the first move through which the Proponent states the thesis ¾ is an aggressive or a defensive
act. In dialogical logic the meaning in use of the logical particles is given
by two types of rules which determine their local and their global meaning
(particle and structural rules respectively).
The particle rules specify for each particle a pair of moves consisting
of an attack and (if possible) the corresponding defence. Each such pair is
called a round. A round is opened by an attack and is closed by a defence if one is possible.
PARTICLE
RULES
|
¬, Ù, Ú, ®, Ù, Ú |
Attack |
Defence |
|
¬A |
A |
Ä (The
symbol ' Ä' indicates that no defence, but only counter-attack
is allowed) |
|
AÙB |
?L ------------------------- ?R (The
attacker chooses) |
A ------------------------- B |
|
AÚB |
? |
A ------------------------- B (The
defender chooses) |
|
A®B |
A |
B |
|
ÙxA |
?t (The
attacker chooses) |
A[t/x] |
|
ÚxA |
? |
A[t/x] (The
defender chooses) |
The first column contains the form of the formula in question, the second
one possible attacks against this formula, and the last one possible defences
against those attacks. (The symbol ” Ä” indicates that
no defence is possible.) Note that for example ”?L” is a move ¾ more precisely it is an attack
¾ but not a formula.
Thus if one partner in the dialogue states a conjunction, the other may initiate
the attack by asking either for the left-hand side of the conjunction (”show
me that the left-hand side of the conjunction holds”, or ”?L” for short) or
the right-hand side (”show me that the right-hand side of the conjunction
holds”, or ”?R”). If, on the other hand, one partner in the dialogue states
a disjunction, the other may initiate the attack by asking to be shown any
side of the disjunction (”?”).
Next, we fix the way formulae are sequenced to form dialogues with a set
of structural rules (orig. Rahmenregeln):
R0 (starting rule):
Moves are alternately uttered by P and O. The initial formula is uttered by P. It provides
the topic of argument. Every move below the initial formula is either an attack
or a defence against an earlier move stated by the other player.
R1 (formal rule for atomic formulae):
P may not introduce atomic formulae: any atomic formula must be
stated by O first. Atomic formulae can not be attacked.
RI2 (intuitionistic
rule):
In any move, each player may attack a (complex) formula asserted
by his partner or he may defend himself against the last not already defended attack. Only the latest open attack
may be answered: if it is X’s turn at position n and there are two open attacks
m, l such that m < l < n, then X may not defend against
m.
[viii]
These rules define an intuitionistic logic.
To obtain the classical version simply replace RI2 by the following
rule:
RC2 (classical rule):
In any move, each player may attack a (complex) formula asserted
by his partner or he may defend himself against any attack (including those which have already been defended).
Before stating the next rule we need the following definition (the observation
about dialogical contexts in the
following definition is only relevant for relevance logic, modal logic and
linear logic with exponentials):
DEFINITION 8: We speak of the strict repetition of an attack iff
a.
A move is being attacked although the same move
(from the same dialogical context) has already been attacked with the same
attack before (notice that ?L and ?R are in this context different attacks).
In the case of moves where
a universal quantifier has been attacked with a new constant, the following
type of move has to be added to the list of strict repetitions:
b.
A universal-quantifier-move is being attacked
using a new constant, although the same move (from the same dialogical context)
has already been attacked before with a constant which was new at the time
of that attack.
DEFINITION 9: We speak of the strict repetition
of a defence iff
c.
An aggressive move (=attack) l which has been already with
the defensive move m (=defence) before, is being
defended from the challenge at l once more with
the same defensive formula (notice that the left part and the right
part of a disjunction are in this context two different defences)
In the case of moves where
an existential quantifier has been defended with a new constant, the following
type of move has to be added to the list of strict repetitions:
d.
An attack on an existential quantifier is being
defended using a new constant although the same quantifier (from the same
dialogical context) has already been defended before with a constant which
was new at the time of that defence.
R3 (no delaying tactics rule):
While playing with the classical structural rule (see RC2)
P may perform a strict repetition of a defence stating a (atomic) twice (or more) if and only
if O has conceded a twice (or more).
No other strict repetitions are allowed.
While playing with the intuitionistic
structural rule P may perform a strict repetition of an attack
(see RI2) if and only if O has introduced a new atomic formula
(see R1 below) which can now be used by P (or iff
O has introduced a new dialogical context which is now accessible for P).
(Notice that according to the definitions leading to this rule neither
the new defence of a existential quantifier nor a new attack on a universal
quantifier using a constant different (but not new) from the one used in the
first defence (in the first attack) represents a strict repetition)
R4 (winning rule):
X wins iff
it is Y’s turn but he cannot move (whether to attack or defend).
As already mentioned, validity is defined in dialogical logic via winning
strategies of P:
DEFINITION 10: Validity:
In a certain dialogical system a formula is said to be valid iff P has a (formal) winning strategy for it, i.e. P can in
accordance with the appropriate rules succeed in defending A against all possible allowed criticism by O.
[ix]
It is possible to
build tableau systems for winning strategies, which correspond to the well-known
semantic tableau methods. We present them in the text.
[x]
Example 10 (either with the classical or the intuitionistic
structural rule: it makes no difference):
|
O |
P |
|
(1) (a®b)Ùa 0 (3) a®b (5) a (7) b |
((a®b)Ùa)®b (0) b
(8) 1 ?L (2) 1 ?R (4) 3 a
(6) |
P
wins
Example 12 (classical):
|
O |
P |
|
(1) ?t 0 (3) ? 2 (5) Pt 4 (3’) ? 2 |
Ùx(PxÚØPx) (0) PtÚØPt (2) ØPt (4)
Ä Pt (6) |
P
wins
Remarks:
Notation: Moves are labelled in (chronological) order of appearance. They
are not listed in the order of utterance, but in such a way that every defence
appears on the same level as the corresponding attack. Thus, the order of
the moves is labelled by a number between brackets. Numbers without brackets
indicate which move is being attacked.
Example 12 shows how the classical
structural rule works: the Proponent may, according to the classical structural
rules, defend an attack which was not the last one. This allows the Proponent
to state Pt in move (6). For
notational reasons we repeated the attack of the Opponent, but actually this
move does not take place. That is why, instead of tagging the attack with
a new number, we repeated the number of the first attack and added an apostrophe.
The quite simple structure of
the dialogue in this and the following examples should make it possible to
recognise with the help of only one dialogue whether P has a winning strategy
or not.
The
next rule shows how the non-delaying rule works in classical logic:
[xi]
Example 13 (classical):
|
O |
P |
|
(1) (a®b)®a 0 (3) a (5) a 2 |
((a®b)®a)®a (0) a/a
(4)/(6) a®b (2) |
P
wins
Here, the clever
Opponent, who does not give up so easily, after the Proponents s defence 4,
attacks move 2 stating a once more.
But, the Opponent’s twofold use of a
allows the Proponent to repeat his defence.
The next two examples
deal with dialogues with hypotheses. In these dialogues the Proponent states
his thesis under the condition of some hypotheses. Any such hypothesis is
to be included as a concession of the Opponent at the very start of the dialogue.
The hypotheses will be formulated with schematic letters and the Proponent
can at any stage of the dialogue make use of these hypotheses asking first
for an adequate instantiation (chosen by the Proponent) of the according schematic
letters.
[xii]
In the first of the next two examples we show how to obtain
tertium non datur from
an adequate instantiation of Peirce’s Law:
Example 14 (intuitionistic):
|
O |
P
|
|
H: (®Á)®Â)®Â (1) ?
0
(3)
((aÚØa)®Ø(aÚØa))®(aÚØa) ® (aÚØa) (5) (aÚØa)®Ø(aÚØa) 4 (7) ?
6 (9) a 8 (11) Ø(aÚØa) Ä (13) ?
12 |
aÚØa (0)
H: ?
(aÚØa)/Â, Ø(aÚØa)/Á (2) 3 ((aÚØa)®Ø(aÚØa))®(aÚØa) (4) aÚØa (6) 3 Øa (8) Ä 5 aÚØa (10) 11 aÚØa (12) a
(14) |
P wins
With move 3, the
Proponent asks for an adequate instantiation of the schematic letters. The
reader can verify that if at move the Opponent instead of attacking move 4
he defends himself from move 4 he can loose even faster.
Our
last example show how to obtain tertium non datur from an adequate instantiation of double negation:
Example 15 (intuitionistic):
|
O |
P
|
|
H: ØØ® (1) ?
0 (3) ØØ(aÚØa)®(aÚØa) (5) Ø(aÚØa) 4 Ä (9) ?
6
(11)
a 8 Ä (13) ?
10 |
aÚØa (0)
H: ?
(aÚØa)/Â (2) 3 ØØ(aÚØa) (4) Ä 5 aÚØa (6) Øa (8) Ä 5 aÚØa (10) a
(12) |
P
wins
Here
the Proponent can repeat an attack on move 5 because the Opponent introduced
a new atomic formula at move 11.
[1]
Rahman, S. and Carnielli, W.A. The
Dialogical Approach to Paraconsistency. In D. Krause,
editor, The work of
[2]
Rahman, S. and Roetti, J. A. Dual
intuitionistic paraconsistency
without ontological commitments. In Proceedings
of the International Congress: Analytic Philosophy at the turn of the Millenium in Santiago de Compostela
(Spain), 1-4 December 1999, pages 120- 126, 1999.
[3]
Rahman, S. Ways of Understanding Hugh MacColl's
Concept of Symbolic Existence. Nordic
Journal of Philosophical Logic, volume 3 (1-2): 35-58, 1998.
[4]
Rahman, S. Argumentieren mit Widersprüchen
und Fiktionen. In K. Buchholz, S. Rahman
and I. Weber, editors, pages 131-148, Campus,
[5]
Rahman, S. On Frege's Nightmare.
In H. Wansing, editor, Essays on non-classical logic, King's College,
[6]
Van
Bendegem, J. P. Paraconsistency
and Dialogue Logic. Critical Examination and Further Explorations. In Rahman and Rückert, editors, 2000.
In Press.
[7]
Batens, D. A survey of inconsistency-adaptive logics. In Press,
2000.
[8]
Urchs, M. Recent
trends in paraconsistent logics.
[9]
Rahman, S. and Rückert, H. Dialogische
Logik und Relevanz. FR
5.1 Philosophie, Universität des Saarlandes, volume 27 (Memo),
1998.
[10]
Rahman, S. and
Rückert H. Dialogical Modal Logic.
Logique et Analyse, 2001, volume
March 2001. In Press.
[11]
Rahman, S. and Rückert, H. Eine neue dialogische Semantik für die lineare Logik.
In C.F. Gethmann, G. Kamp, Neue Entwicklungen der Konstruktiven Logik, 2001. In Press.
[12]
Rückert, H. Why Dialogical
Logic? In H. Wansing, editor, Essays on non-classical logic, King's College:
[13]
Rückert, H. Dialogue games and connexive
logic. In A. Baltag, M. Pauly, editor, Workshop Logic and Games, pages 35-42,
ILLC,
[14]
Da Costa, N. C. A. Paraconsistent Logic. In Stanislaw Jáskowski
Memorial Symposium. Paraconsistent Logic, Logical
Philosophy, Mathematics & Informatics at Torún,, pages 29-35, 1998.
[15]
Da Costa, N. C. A;
Bueno, O. and French, S. The Logic of Pragmatic Truth. Journal of Philosophical Logic. volume
26: 603-620, 1998.
[16]
Rahman, S., Rückert, H. and Fischmann, M.. On
Dialogues and Ontology. The dialogical approach to free logic. Logique et Analyse,
1997, volume 160, 327-374.
[17]
Meheus, J. Rich paraconsistent logics: the three-valued logic AN and the adaptive
logic ANA that is based on it. In print.
[18]
Smullyan, R.. First-Order Logic.
[19]
Lorenzen, P. and Lorenz,
K. Dialogische Logik. Wissenschaftliche Buchgesellschaft,
[20]
Rahman, S. Über Dialoge, protologische Kategorien
und andere Seltenheiten. Peter Lang,
[21]
Krabbe, E. C. W. Formal
Systems of Dialogue Rules. Synthese, volume 63(3): 295-328, 1985.
[22]
Rahman, S. and Rückert, H. Die pragmatischen Sinn- und Geltungskriterien der Dialogischen
Logik beim Beweis des Adjunktionssatzes. Philosophia Scientiae, volume 3(3): 145-170,
1999.
[23]
Felscher, W. Dialogues,
strategies and intuitionistic provability. Annals of Pure and Applied Logic, volume
28: 217-254, 1985.
[24]
Rahman, S. and Rückert, H., editors. New
Perspectives in Dialogical Logic. Special issue of Synthese with contributions of P.
Blackburn, D. Gabbay and J. Woods, J. Hintikka, E. Krabbe, K. Lorenz,
U. Nortmann, H. Prakken,
S. Rahman and H. Rückert,
G. Sandu, J. P. Van Bendegem, G. Vreeswijk, volume April 2001, 2001. In Press.
* We would like to thank Diderik Batens (
[i] For a short introduction to standard dialogical logic see the appendix.
[ii] See details on how to build the tableau systems in Rahman and Carnielli ([1]) and Rahman ([3] and [5]).
[iii] João Marcos (Unicamp) observed that the classical literal system corresponds to Sette's P1.
[iv] A systematic formulation of subdialogues for relevant aims can be found in Rahman and Rückert ([10] and [11]) and Rückert ([12] and [13]).
[vi] Cf. [19]. Further work has been done for example by Rahman ([20]).
[vii] Sometimes we use X and Y to denote P and O with X¹Y.
[viii] Notice that this does not mean that the last open attack was the last move.
[ix] See consistency and completeness theorems in Krabbe ([21]) and Rahman ([20]).
[x] See more details on how to build tableau systems from dialogues in Rahman ([20]), Rahman and Rückert ([22]). Alternative systems with the corresponding proofs have been given by Felscher ([23]) and by Krabbe ([21]).
[xi]
João Marcos (
[xii] Actually in the case of dialogues with hypotheses we need to extend the non-delaying rule in such a way that unnecessary repetitions of instantiations should be avoided. This extension is not difficult if we think that an aggressive instantiation-move works in a similar way as an attack on a universal quantifier: the Proponent may repeat instantiation-attacks until all propositional variables occurring in the thesis have been used for an instantiation. We leave the details for the reader.