chapter (see p. 53) and we simply refer the reader to that section as an explanation of the following table summing up these particle rules.

<table><caption>Table 6: Particle rules for dialogical games: propositional connectives</caption><thead><tr><th></th><th>Conjunction</th><th>Disjunction</th><th>Implication</th><th>Negation</th></tr></thead><tbody><tr><th>Move</th><td>X ! A ∧ B</td><td>X ! A ∨ B</td><td>X ! A ⊃ B</td><td>X ! ¬A</td></tr><tr><th>Challenge</th><td>Y ? L<sup>^</sup><br>or<br>Y ? R<sup>^</sup></td><td>Y ?<sub>V</sub></td><td>Y ! A</td><td>Y ! A</td></tr><tr><th>Defence</th><td>X ! A<br>(resp.)<br>X ! B</td><td>X ! A<br>or<br>X ! B</td><td>X ! B</td><td>—</td></tr></tbody></table>

The particle rules for quantifiers has not been introduced, so we will be commenting these rules briefly.

The rules for universal quantification are similar to those for conjunction: stating a universally quantified proposition means that the challenger may choose any individual constant $a_i$ and request of the utterer to make his statement by instantiating every free occurrence of $x$ with $a_i$. That is, the challenger chooses which proposition he wants the utterer to state.

**Properties of universal quantification:**

* the challenge is a request;

* the challenger has the choice;

* the defender must state the requested proposition.

The rules for existential quantification are similar to those for disjunction: it is the defender who chooses the proposition he wants to state in response to the challenge.

**Properties of existential quantification:**

* the challenge is a request;

* the defender has the choice;

* the defender chooses which proposition to state.

<table><caption>Table 7: Particle rules for dialogical games: quantifiers</caption><thead><tr><th></th><th>Universal quantification</th><th>Existential quantification</th></tr></thead><tbody><tr><th>Move</th><td>X ! ∀xB(x)</td><td>X ! ∃xB(x)</td></tr><tr><th>Challenge</th><td>Y ? [x/a<sub>i</sub>]</td><td>X ?<sub>∃</sub></td></tr><tr><th>Defence</th><td>X ! B(x/a<sub>i</sub>)</td><td>X ! B(x/a<sub>i</sub>)<br>with 1 ≤ i ≤ n</td></tr></tbody></table>
## Summing up

<table><caption>Table 8: Summing up the properties of the particle rules</caption><thead><tr><th></th><th>Nature of the challenge</th><th>Who has the choice</th><th>Step to defend</th></tr></thead><tbody><tr><th>Conjunction</th><td>Request</td><td>Challenger</td><td>State the requested proposition</td></tr><tr><th>Universal quantification</th><td>Request</td><td>Challenger</td><td>State the requested proposition</td></tr><tr><th>Disjunction</th><td>Request</td><td>Defender</td><td>State the desired proposition</td></tr><tr><th>Existential quantification</th><td>Request</td><td>Defender</td><td>State the desired proposition</td></tr><tr><th>Implication</th><td>Statement</td><td>No choice</td><td>State the consequent</td></tr><tr><th>Negation</th><td>Statement</td><td>No choice</td><td>None</td></tr></tbody></table>

<table><caption>Table 9: Summing up the particle rules</caption><thead><tr><th></th><th>Conjunction</th><th>Disjunction</th><th>Implication</th><th>Negation</th><th>Universal quantification</th><th>Existential quantification</th></tr></thead><tbody><tr><th>Move</th><td>X!A∧B</td><td>X!A∨B</td><td>X!Asup B</td><td>X!¬A</td><td>X!∀xB(x)</td><td>X!∃xB(x)</td></tr><tr><th>Challenge</th><td>Y?L<sup>^</sup><br>or<br>Y?R<sup>^</sup></td><td>Y?<sub>Y</sub></td><td>Y!A</td><td>Y!A</td><td>Y? [x/a<sub>i</sub>]</td><td>X?∃</td></tr><tr><th>Defence</th><td>X!A<br>(resp.)<br>X!B</td><td>X!A<br>or<br>X!B</td><td>X!B</td><td>—</td><td>X!B(x/a<sub>i</sub>)</td><td>X!B(x/a<sub>i</sub>)<br>with 1 ≤ i ≤ n</td></tr></tbody></table>

## IV.3 Symmetry and harmony

In providing the properties of the particle rules, a central feature we have distinguished is who has the choice: is it the challenger or the defender? The meaning of the logical constants is largely determined by who has the choice in the interaction. But notice that in formulating the particle rules, the players' identities are not specified: we do not use O and P but we use X and Y instead, thus only specifying who is the challenger and who is the defender *for this particular statement*. That is, we simply provide the appropriate challenge and defence for certain logical constants and determine in this way who has the choice: we provide their meaning in terms of interaction within a dialogue (a game of giving and asking for reasons).

It would not be reasonable to base a game-theoretical approach to the meaning of logical constants in which the meaning differs according to which players utters it: this approach would make interaction senseless, for each player would be meaning something different when uttering the same thing. Equality in action is precisely based on the possibility for a player to say *the same thing* as the other player, and by that to be meaning also the same thing. Equality in action is in this regard the idea that a statement
made by a player can be made by another player in a game of giving and asking for
reasons (a dialogue) with the exact same meaning as the statement made by the first
player, that is with the same particle rules for challenging and defending it. It is thus the
interaction based on player-independent rules that allows two different players to be
speaking of the same thing: equality between different statements emerges from the
interaction itself.

Since the rules for the logical constants are independent of the player's identities—
the rules are exactly the same for the two players—we say that these rules are symmetric.
This feature captures one of the strengths of the dialogical approach to meaning: the
dialogical approach is in this way immune to a wide range of trivializing connectives
such as Prior's *tonk*.<fnref n="54" />

Symmetry, or player-independence in the particle rules, must be contrasted with the
dialogical rendering of harmony, which concerns the structural rules and the strategy
level, not the particle rules. The structural rules, which will be introduced in the next
section, are not player independent: the first rule (SR0) specifies who the players are
(Proponent or Opponent) according to who plays the first move, that is who states the
thesis; that player will be the Proponent. But the rule that matters most in regard to
immanent reasoning is the Copy-cat rule (or Socratic rule in a CTT framework); this rule
puts a restriction on the Proponent's moves, while those of the Opponent are left
unrestricted: which the Proponent cannot play an elementary statement that has not been
previously stated by the Opponent.

The purpose of this restriction is to insure that the thesis will be grounded only on what
the Opponent has conceded, and thereby secure a form of analyticity that we call
immanent reasoning: the Proponent has to ground his thesis on what the Opponent brings
forward in the course of their interaction (the dialogue), an interaction that is initiated by
the Proponent stating a thesis, which the Opponent challenges with the ensuing series of
challenges and defences defined by the particle rules and constituting the dialogue. Thus
the Opponent will not bring forward anything that does not stem from the meaning
(defined by the particle rules) of the thesis, and the Proponent will not bring any
elementary proposition into the game that he cannot justify within that very same
dialogue by refering to the Opponent's own statements ("I am entitled to state this
because you have stated it yourself").

Symmetry and harmony are two essential aspects of the dialogical framework and are
the principles for immanent reasoning.

Dialogical harmony thus coordinates a player-independent level (the local meaning)
and a player-dependent level (the global meaning and the strategy level). This aspect
contrasts with the Constructive Type Theory notion of harmony which belongs to proof-
theory and stays only at the level of strategies.<fnref n="55" /> Immanent reasoning and equality in
action emerge from taking the specific aspects of the three levels (local, global and
strategic) into account and considering how they intertwine to build these complex and
dynamic frameworks that are dialogues.

IV.4 Global meaning:

The global meaning—as opposed to the local meaning defined by the particle
rules—is defined by means of *structural rules* which specify the general way plays

<footnote n="54">⁵⁴ See (Rahman, Clerbout, & Keiff, 2009) and (Redmond & Rahman, 2016).</footnote>

<footnote n="55">⁵⁵ See (Rahman & Redmond, 2016) and (Rahman, Redmond, & Clerbout, 2017).</footnote>
unravel by specifying who starts in a play, what moves are allowed and in which order, when a play ends and who wins it. For a more informal presentation of the structural rules determining the global meaning in the dialogical framework, see chapter III.2.2, p.55.

### IV.4.1 Preliminary terminology

**Terminal plays:**

A play is called *terminal* when it cannot be extended by further moves in compliance with the rules.

**X-terminal plays:**

A play is *X-terminal* when the play is terminal and the last move in the play is an *X*-move.

### IV.4.2 The structural rules

#### SR0 (Starting rule)

Any dialogue starts with the Opponent stating initial concessions (if any) and the Proponent stating the thesis (labelled move 0). After that, each player chooses in turn a positive integer called the *repetition rank* which determines the upper boundary for the number of attacks and of defences each player can make in reaction to each move during the play.

*Example: if the repetition rank of *O* is *m* := 1, then *O* may attack or defend against at most *once each move of P*. If *P*'s repetition rank is *n* := 2, then *P* may attack or defend against at most *twice each move of O*.*

#### SR1: Development rule

The Development rule depends on what kind of logic is chosen: if the game uses classical logic, then it is SR1c that should be used; but if intuitionistic logic is used, then SR1i must be used.

#### SR1c (Classical Development rule)

Players move alternately. Once the repetition ranks have been chosen, each move is either attacking or defending a move made by the other player, in accordance with the particle rules.

#### SR1i (Intuitionistic Development rule)

Players move alternately. Once the repetition ranks have been chosen, each move is either attacking or defending a move made by the other player, in accordance with the particle rules.

Players can respond only to the *last non-answered* challenge of the other player.

*Note: This last clause is known as the Last Duty First condition, and makes dialogical games suitable for intuitionistic logic (hence this rule's name).*

#### SR2 (Copy-cat rule)

*P* may not play an elementary statement unless *O* has stated it first.

Elementary propositions cannot be challenged.
*Note: The formulation of this rule has a downside: the thesis of a dialogical game cannot be an elementary statement. For a special version of the Copy-cat rule allowing plays on elementary statements, see below (section 0) where we link this rule to equality.*

**SR3 (Winning rule)**

Player X wins the play ζ only if it is X-terminal.

**Linking the Copy-cat rule (SR2) and equality**

The Copy-cat rule<fnref n="56" /> is one of the most salient characteristics of dialogical logic. As discussed by (Marion & Rückert, 2015), it can be traced back to Aristotle's reconstruction of the Platonic dialectics. A purely argumentative point of view can be defined within dialectics as refraining from calling on some authority beyond what has actually been brought forward during the current argumentative interaction, the ultimate authority being the fact that the other person has said it, any other consideration being set aside for the time of the dialectical exchange (in this argumentative perspective). Thus, when an elementary statement is challenged, the challenge can be answered only by invoking the challenger's own concessions. In such a context, the Copy-cat rule can be understood in the following way, when a player plays an elementary statement:

> *my grounds for stating the proposition you are challenging are exactly the same as the ones you brought forward when you yourself stated that very same proposition.*<fnref n="57" />

In this regard, elementary statements actually can be challenged (as opposed to the SR2 formulation above), the answer then being of the form “but you have said it yourself”. A special formulation of the Copy-cat rule SR2 addresses this problem.

**Special Copy-cat rule**

O's elementary statements cannot be challenged. However, O can challenge an elementary statement played by P. The challenge and corresponding defence is determined by the following table. Notice that this (structural) rule is not player-independent and uses the names of the players.

<table><caption>Table 10: SR2 special Copy-cat rule</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Special Copy-cat rule<br>(Structural rule 2)</th><td>P!A<br>For elementary A</td><td>O?A</td><td>P!sic(n)<br>P indicates that O<br>stated A at move n</td></tr></tbody></table>

The Copy-cat rule, and even more in this special formulation, introduces an asymmetry between the two players (the Proponent's moves are restricted in a way the Opponent's are not).

<footnote n="56">⁵⁶In previous literature on dialogical logic this rule has been called the *Formal rule*. Since here we will distinguish different formulations of this rule that yield different kind of dialogues we will use the term *Copy-cat rule* when we speak of the rule in standard contexts (such as in the present section)—contexts in which the constitution of the elementary propositions involved in a play is not rendered explicit. When we use the rule in a dialogical framework for CTT, as in the next chapter, we speak of the *Socratic rule*. However, we will continue to use the expression *Copy-cat move* in order to characterize moves of P that copies moves of O.</footnote>

<footnote n="57">⁵⁷See (Rahman, Clerbout, & Keiff, 2009) and (Rahman & Keiff, 2010).</footnote>
## IV.5 Examples of plays

These examples should allow the reader to fully understand the rules given above and their implications, especially the difference between SR1c (classical Development rule) and SR1i (intuitionistic Development rule). For an introduction to the table presentation of dialogues, see chapter III.3, p.56. In the next chapter (V), strategies will be introduced, which allow to compare different plays (with different choice sequences of the players) and build the best possible way of playing for one of the players.

### First example, the third excluded: $A \lor \neg A$

The third excluded (*tertium non datur*) is a principle stating that a proposition either is (*A*) or is not (*\neg A*), without any third possible option. This principle is much discussed in philosophy and logic,<fnref n="58" /> it is a valid principle in classical logic, but is not accepted in intuitionistic logic. If this principle is accepted, the principle of non-contradiction (*\neg(A \land \neg A)*) follows, but the reverse is not the case (and intuitionistic logic accepts the principle of non-contradiction but not the principle of third excluded). We will here give a play according to the classical (structural) rules, and then a play according to the intuitionistic (structural) rules.

### Play 4: the third excluded—classical rules

<table><thead><tr><th></th><th>O</th><th></th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$n := 1$</td><td></td><td></td><td>$!A \lor \neg A$</td><td>0</td></tr><tr><td>3</td><td>?<sub>v</sub></td><td>0</td><td></td><td>$m := 2$</td><td>2</td></tr><tr><td>5</td><td>!A</td><td>2</td><td></td><td>$!\neg A$</td><td>4</td></tr><tr><td>{3}</td><td>{?<sub>v</sub>}</td><td>{0}</td><td></td><td>—</td><td></td></tr><tr><td></td><td></td><td></td><td></td><td>!A</td><td>6</td></tr></tbody></table>

P wins (classical rules).

*Note*: the curly brackets are inserted to stress the fact that *O* is not actually making a move, but that *P* is using his repetition rank of 2 in order to defend twice *O*'s challenge (move 3). We repeat that challenge (in brackets) in order to know where *P*'s move 6 comes from.

Notice that *P* would not have won without a repetition rank higher than 1: he would not have been allowed to answer twice to *O*'s challenge (move 3), and thus use her own assertion of *A* (move 5) triggered by *P*'s first defence to *O*'s challenge (move 3). This example is a good illustration for the Copy-cat rule and for the use of repetition ranks.

Notice also that *P*'s move 6 is an answer to the challenge of move 3, that is a challenge preceeding the last unanswered challenge, which is move 5. This challenge of move 5 will never be answered, because an attack on the negation cannot be defended. So *P* wins because the classical rules for dialogues *do not* restrict *P*'s answers only to the last unanswered challenge. This fact is the key to understand the outcome of the next play, which uses the intuitionistic rules.

<footnote n="58">⁵⁸ For an overview of the philosophical positions behind such principles, see for instance (Read, 1995, pp. 222-224), or see (Dummett, 1978) for seminal papers.</footnote>
### Play 5: the third excluded—intuitionistic rules

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! A ∨ ¬ A</td><td>0</td></tr><tr><td>1</td><td>m := 2</td><td>2</td></tr><tr><td>3</td><td>?<sub>v</sub></td><td>0</td></tr><tr><td>5</td><td>! A</td><td>4</td></tr></tbody></table>

O wins (intuitionistic rules).

## Second example, the double negation elimination: $¬¬A ⊃ A$

The elimination of double negation is another example of a principle accepted in classical logic but rejected in intuitionistic logic. This principle is at the core of classical mathematics, for it is what is used in indirect proofs (concluding A from the demonstration that the negation of A leads to a contradiction, that is from the fact that $¬¬A$ holds). This principle is closely linked to the principle of excluded middle. Once again, we give a play with classical rules (P wins) and a play with intuitionistic rules (P loses).

### Play 6: the elimination of double negation—classical rules

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! ¬¬A ⊃ A</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>2</td></tr><tr><td>3</td><td>! ¬¬A</td><td>0</td></tr><tr><td>5</td><td>! A</td><td>4</td></tr></tbody></table>

P wins (classical rules).

Notice that as for the third excluded, P wins here because he does not have to answer only to the last unanswered challenge (which is move 5) but answers a previous challenge (his move 6 is an answer to the challenge of move 3). This move is forbidden by the intuitionistic (structural) rules ("Last Duty First") illustrated in the next play: P should play his move 6, but is not allowed to; it is his turn and he cannot play, so he loses.

### Play 7: the elimination of double negation—intuitionistic rules

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! ¬¬A ⊃ A</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>2</td></tr><tr><td>3</td><td>! ¬¬A</td><td>0</td></tr><tr><td>5</td><td>! A</td><td>4</td></tr></tbody></table>

O wins (intuitionistic rules).

It should be clear from these two examples that the intuitionistic rules for dialogues only concern the *structural* rules, namely *when* (in what conditions) a move (challenge or
defence) is allowed, but not the *particle* rules which determine *how* to challenge a move or *how* to answer a challenge.

The intuitionistic rules are only a *restriction* imposed on the classical rules, so if **P** wins a play according to the intuitionistic rules, *a fortiori* he should win according to the classical rules.

**Third example, the double negation of the third excluded: $\neg\neg(A \lor \neg A)$**

This example is a combination of the previous two. But whereas the principle of third excluded and the principle of double negation elimination are not intuitionistic principles (**P** loses), the double negation of the third excluded $\neg\neg(A \lor \neg A)$ does actually hold with intuitionistic rules. This clearly shows that, for intuitionistic logic, an expression is not equivalent to its double negation (the elimination of the double negation of the third excluded would not yield the third excluded, which would contradict the first example).

**Play 8: double negation of third excluded—intuitionistic rules**

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td>$!\neg\neg(A \lor \neg A)$</td><td>0</td></tr><tr><td>3</td><td>$!\neg(A \lor \neg A)$</td><td>0</td><td>$n := 2$</td><td>2</td></tr><tr><td></td><td>$—$</td><td></td><td>$—$</td><td></td></tr><tr><td></td><td></td><td>3</td><td>$!A \lor \neg A$</td><td>4</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td>$!\neg A$</td><td>6</td></tr><tr><td>7</td><td>!A</td><td>6</td><td>$—$</td><td></td></tr><tr><td></td><td>$—$</td><td></td><td>$!A \lor \neg A$</td><td>8</td></tr><tr><td>9</td><td>?<sub>v</sub></td><td>8</td><td>$!A$</td><td>10</td></tr></tbody></table>

**P** wins (intuitionistic rules).

In this play, **P** also uses his repetition rank of 2 (move 4 and move 8), but this time to challenge move 3 (instead of defending a move). As opposed to the previous examples, he does not need to defend a move preceeding the last unanswered challenge, so this play in winnable by **P** in the intuitionistic and in the classical contexts.
# V. ADVANCED DIALOGUES: STRATEGY LEVEL

The strategy standpoint is but a generalisation of the procedure which is implemented at the play level; it is a systematic exposition of all the relevant variants of a game—the relevancy of the variants being determined from the viewpoint of one of the two players. For a more intuitive approach of strategies and a step-by-step introduction of strategies as branching tables, see section III.5, p. 59. Such trees with branching tables are a good didactic approach to strategies, for the rules in building the tree are the same as those for building the plays: we simply use an algorithm yielding all the relevant plays for a player, keeping the table presentation we use for plays. The link from plays to strategies is thus clearly apparent. This method however is rather cumbersome and becomes unmanageable as soon as we deal with games involving more than two choices, the generated trees taking too much space. We will here present strategies from another perspective, that of extensive forms of dialogical games (more precisely from their core; see below, section V.3) rather than the table presentation; the extensive form presentation has this advantage over the table presentation that strategies can be linked more straightforwardly to demonstrations, which will be useful in chapter IX. This link is crucial to the logical framework of dialogues, for the dialogical notion of validity is secured through the notion of a *winning strategy* for the Proponent. Many metalogical results in the dialogical framework are obtained by leaving the level of rules and plays to move to the level of strategies; winning strategies for a player are one of these metalogical results.

We will here first (section V.1) provide some definitions pertaining to the strategy level along with three important results from existing litterature on this level; then (section V.2) we will introduce what the *core* of a strategy is and the assumptions on the plays we need in order to extract such a core from the extensive form of a strategy; we will then (section V.3) be able to provide the procedure for building a heuristical presentation of the core, that is a presentation of the strategy explicitly preserving the link with the play level; finally (section V.4) we will provide the procedure for building a tree-shaped presentation of the core, which takes up less space than the heuristical (table) presentation and makes it easier to establish links between the dialogical framework and other logical frameworks.

## V.1 Preliminary notions

### V.1.1 Definitions

**Extensive form of a dialogical game:**

The *extensive form* $E(\phi)$ of the dialogical game $D(\phi)$ is simply its tree presentation, also called the game-tree. Nodes are labelled with moves so that the root is labelled with the thesis and paths in $E(\phi)$ are linear representations of plays and maximal paths represent terminal plays in $D(\phi)$.

That is, the extensive form of a dialogical game is an infinitely generated tree in which each branch is of a finite length.
**Strategy**

A strategy for player X in D(φ) is a function which assigns an X-move M to every non terminal play ζ having a Y-move as last member, such that extending ζ with M results in a play.

**X-winning strategy (or X-strategy)**

An X-strategy is winning if playing according to it leads to X-terminal plays no matter how Y moves.

That is, a winning strategy for player X defines the situation in which, for any move choice made by player Y, X has at least one possible move at his disposal allowing him to win.

**Extensive form of an X-strategy**

Let sx be a strategy of player X in D(φ) of extensive form E(φ). The extensive form of sx is the fragment Sx of E(φ) such that:

1. The root of E(φ) is the root of Sx,

2. For any node t which is associated with an X-move in E(φ), any immediate successor of t in E(φ) is an immediate successor of t in Sx,

3. For any node t which is associated with a Y-move in E(φ), if t has at least one immediate successor in E(φ) then t has exactly one immediate successor in Sx, namely the one labelled with the X-move prescribed by sx.

**Validity**

A proposition is valid in a certain dialogical system if and only if P has a winning strategy for it.

V.1.2 Some results from existing literature on the strategy level

The following three results—extracted from existing literature on the subject— establish the correspondance between the dialogical framework and other frameworks involving classical and intuitionistic logics. We will be using them in order to facilitate the building of dialogical demonstrations: the procedure presented in the next section (V.2) will use results justified in this literature: for details and the proofs, see in particular (Clerbout, 2014a; 2014b) and (Felscher, 1985).

**P-winning strategies and leaves**

Let w be a P-winning strategy in D(φ). Then every leaf in the extensive form Wφ of w is labelled with an elementary P-sentence.

**Determinacy**

There is an X-winning strategy in D(φ) if and only if there is no Y-winning strategy in D(φ).

**Soundness and Completeness of Tableaux**

Consider first-order tableaux and first-order dialogical games. There is a tableau proof for φ if and only if there is a P-winning strategy in D(φ).

The fact that the existence of a P-winning strategy coincides with validity (there is a P-winning strategy in D(φ) if and only if φ is valid) follows from the soundness and completeness of the tableau method with respect to model-theoretical semantics.
This third metalogical result for the standard dialogical framework will be taken
here for granted (the proof is given for instance in (Clerbout, 2014a)), but we will provide
in chapter IX the algorithm transforming a P-winning strategy in the framework for
dialogues for immanent reasoning into CTT-demonstrations and reversewise.

V.2 Developping a dialogical demonstration: reaching the core of a strategy

Extensive forms of strategies have some redundant information—like the different order of moves—that can be set aside by extracting from the strategy its *core*.<fnref n="59" />

The core of a strategy will allow us to build translation algorithms from the dialogical framework to other logical frameworks; chapter IX will thus use the core of strategies in dialogues for immanent reasoning (the dialogical framework incorporating CTT features presented in chapters VI-VII) in order to build a translation procedure from winning strategies to CTT-demonstrations.

A dialogical game is the set of plays starting with the same thesis (see section IV.1, p. 65). Bear in mind that the extensive form of a game is simply its tree presentation. Since a game takes into account every possible choice for each player, its extensive form has an infinite number of branches (each of a finite length, because of the repetition ranks): there will be a branch for each possible combination of repetition ranks (**O** choosing 1 and **P** choosing 1 to *n* yields *n* branches with each combination, then if **O** chooses 2, **P** will have again the choice from 1 to *n*, etc.), there will be a branch for each possible choice of instantiation of the quantifiers, there will be different branches for different orders of moves, etc. In all these branches, many are not relevant, either because they do not add any information, or because the players did not play optimally (one of the greatest strengths of the dialogical framework, at least for its philosophical value, is that it allows players to play in a non-optimal fashion).

Extensive forms of strategies do not sift through these informations and thus keep a lot of pointless information. To obtain the core of the extensive form of a strategy, that is, to obtain only the relevant information for building a strategy for a player, we need some kind of heuristic procedure allowing us to deal with such bountiful arborescences. We will be using the three metalogical results provided in the previous section (V.1.2), pertaining to 1) P-winning strategies and leaves, 2) determinacy, and 3) the link with validity.

V.2.1 Features essential to the procedure yielding the core of a strategy

Here are a series of assumptions, definitions, and rules, that will allow us to speak
about the plays in the following procedures—the heuristical one (V.3), and the graphic
tree-shaped one (V.4)—linking the play level and the strategy level of the dialogical
framework. Since our goal is to build a procedure allowing us to arrive at the *strategy*
level through an arborescence of *plays*, we need to be able to speak *about* the plays, for
instance saying which player had which choices in a play, what other options were
available, and so on. We will name these plays $\rho_1, \rho_2, \text{etc.}$ in order to differenciate them
from each other; we classify them with respect to the last decision taken (see p. 78).

Our goal in this chapter is to find the games won by the Proponent; all the relevant

<footnote n="59">⁵⁹ See (Rahman & Clerbout, 2015).</footnote>
plays constituting the game therefore need to be **P**-terminal. But we are more specifically looking for a **P**-strategy, so only **O**-choices will matter: they are the ones that will show if **P** can win or not, whatever **O** chooses; that is, even if **O** plays optimally. Think for instance of chess-mate in *x* moves: what matters are the possible movements for **O**, and **P** adapts his moves according to the **O**-move actually played.

**Assumption on repetition ranks**

We assume that the number of repetition rank for **O** is 1.

*The point is that, since O is not restricted by the Copy-cat rule in any of its forms (including the Socratic rule), she can always choose the move that is the best for her own interests, and even if she makes a bad choice in a play, she can correct it in a new play. Thus, rank 1 is sufficient.*

We choose a repetition rank for **P** allowing him to win the first play (but not necessarily every possible play). Once the first play is won by **P**, the procedure will allow him to choose another repetition rank for a new play.

*Finding the right repetition rank for **P** that will always allow him to win is one of the objectives of developing demonstrations.*

**Assumption on move preferences for O**

When **O** has to choose an individual constant she will always choose a new one.

*The reason is pretty straight-forward: it is the best possible choice for **O**. Since **P** is restricted by the Copy-cat rule, he needs to rely on **O**'s choices in order to apply a Copy-cat move. In such a context, the only way to (try to) block the use of the Copy-cat move is to always choose a new constant, whenever a choice is to be made. Thus, this assumption is in **O**'s best interest.*

When **O** can challenge a move where **P** has several defensive options, **O** will launch the challenge before carrying out other moves.

*The reason is similar to the previous one: it is better for **O** to force **P** to make his choice as soon as possible.*

**O-Decisions**

We say that **O** makes a decision in $\wp_n$ in the following cases:

(i) When she challenges a conjunction or an existential: she must choose which side to ask for.

(ii) When she defends a disjunction: she must choose one of the sides of the disjunction.

(iii) When she has an implication to defend: she must choose either to defend it (state the consequent) or to counterattack, that is to launch a challenge on **P**'s attack of the implication (where he stated the antecedent of the initial implication).

(iv) When she defends an existential: she chooses a (new) constant.

(v) When she challenges a universal: she chooses a (new) constant.
## Assumption on O-decisions

The following procedure only takes into consideration decisions of type i) challenge a conjunction or existential, ii) defend a disjunction, and iii) defend an implication: decisions of type iv) defend an existential, and v) challenge a universal, are not really options since our assumptions stipulate that O will always choose a new constant and challenge if she can.

<table><caption>Table 11: O-decisions in a play</caption><tr><td colspan="2">O has a choice and takes a decision when</td></tr><tr><td>O challenges a...</td><td>O defends a...</td></tr><tr><td>Conjunction<br/>Existential</td><td>Disjunction<br/>Implication</td></tr></table>

## Choices: using up the available options

We say that a decision has *used up* the available options if and only if this decision chooses an option when the other option has previously been chosen.

We say that a decision has *not used up* the available options when, because of O's repetition rank 1, she chooses one of two available options, the other option not having been previously chosen: this second option, which remains unchosen, is said *unused*.

## Definition of dependent moves

We say that a move *M* depends on the move *M'* if there is a chain of applications of (particle) rules leading from *M'* to *M*.<fnref n="60" />

## Left and right decisions

We speak of a *left-decision* when O

* decides to defend the left side of a disjunction, or

* decides to challenge the left side of a conjunction, or

* decides to counterattack instead of defending an implication.

We speak of a *right-decision* when O

* decides to defend the right side of a disjunction, or

* decides to challenge the right side of a conjunction, or

* decides to defend her implication (instead of counterattacking).

## Last unused decision

The *last decision* is the last decision taken by O in a play *m*—proceeding bottom up in the order of the moves—such that this decision *does not use up* the available options.

## Labeling decisions: conjunctions and disjunctions

We label the moves for which a decision has been taken. For a disjunction or a conjunction, we simply add a label on the right hand side of the move:

<footnote n="60">⁶⁰ Dependent moves are important for building subplays triggered by P challenging an O-implication: the moves depending on O counterattacking must be separated from the moves depending on O defending her implication.</footnote>
* $[\delta_n, ...]$ when the left decision has been taken but the right option is still unused; or

* $[..., \delta_n]$ when the right decision has been taken but the left option is still unused.

* $[\delta_m, \delta_n]$ when both options have been chosen (the decision is thus used up): the left decision has been taken in play *m* and the right decision in play *n*.

The label $[\delta_3, ...]$ for instance spells out that the left decision has been taken in play 3, but that the right option has not at that point been chosen before. The label $[\delta_3, \delta_5]$ indicates that the left decision has been taken in play 3 and the right in play 5, so that from play 5 and on, this decision is considered used up.

**Labeling decisions: implications and subplays (branching rule)**

When **O** makes a decision for an *implication* in the play $\wp_n$, she opens two new *subplays* (and not plays) $\wp_{n,L}$ and $\wp_{n,R}$, one after the other, such that

* $\wp_{n,L}$ indicates the subplay where **O** decides to counterattack (left decision), and

* $\wp_{n,R}$ indicates the subplay where **O** decides to defend (right decision).

We say that the available choices for an implication have been used up if both of the subplays have been opened.

The idea of dividing the play into two subplays is to avoid giving **P** an unfair advantage: he cannot use what is given in the development of the left subplay within the development of the right one; **P** must be able to win without using the information of the other subplay. These are not full plays—contrary to the plays opened by using up a decision-option concerning conjunction or disjunction—but these subplays are only a division of the play: it is as if there were no splitting, but we do it in order to check the moves **P** uses.

It must be noted that the procedure prescribes to start with the subplay involving the counterattack (see the second move preference for **O**, p. 77); but once the counterattack on the antecedent has been launched, the repetition rank 1 has been used up. Thus, in the second subplay involving the defence, a challenge to the antecedent of the implication is no longer available. This shows that the two subplays are only a *graphical device* to present both options within the same (main) play. This is possible because **O** is not restricted by the Copy-cat rule and so, contrary to **P**, never needs the information provided in the other subplay in order to win. This branching rule simply divides the two decision-options of **O** in two subplays.

The opening of two subplays is called the *Branching rule* in (Rahman & Keiff, 2005, pp. 273-275). This rule has a strategic motivation, not a play level one. The reason is that we are after the development of a demonstration (this is the point of this chapter and the procedure for obtaining the core of a strategy). It is also possible to develop a notation where both responses are in the same play, counterattack as well as defence, but this comes with a heavy notation. Moreover, in the present study we have repetition ranks and thus we can use them: the rank 1 of **O** blocks from the branch involving the defence of the implication the problematic second counterattack upon **P**'s-challenge.<fnref n="61" /> This shows that the subplays are really two options in the same (main) play.

<footnote n="61">⁶¹ For a discussion of this problem see section 1.6 in (Rahman, Clerbout, & Keiff, 2009).</footnote>
## Starting a subplay

Each subplay starts with the **O**-move immediately succeeding the **P**-move challenging the **O**-implication.

So if the implication was challenged in move *n* of play $\wp_n$, then both $\wp_{n,L}$ and $\wp_{n,R}$ start with move *n+1*.

The first move of the play $\wp_{n,R}$ is the defence of the challenge. Graphically, dots are inserted in the upperplay in the space of the defence, and in the subplay in the space of the challenge.

## Moving from subplays to upperplays

O's moves in a subplay may allow P to make a move in the upperplay. In such a case, the move in the upperplay depending on a move in a subplay will be indexed with its origin (e.g. 12 [$\wp_{n,R}$]).

<figure><img src="image_13.png" /><figcaption>Play 9: Illustration of subplays and upperplays</figcaption></figure>

## P- and O-terminal plays

The play $\wp_n$ is **P**-terminal if and only if every path starting with the thesis, continuing with $\wp_{n,L}$, $\wp_{n,R}$ and all further subplays, are **P**-terminal.

The play $\wp_n$ is **O**-terminal if and only if one of the paths is **O**-terminal.

## V.3 Heuristical presentation of the core (succession of plays)

Assume we have a play $\wp_n$ won by P where O played according to the assumptions mentioned above (pertaining to repetition ranks, move preferences and O-decisions). The following procedure allows us to build a collection of the relevant plays for a P-strategy, taking into account all the O-decisions. The core of a P-winning strategy for the thesis is the collection of plays thus generated: $\wp_1, \wp_2, \wp_3, \dots$

Note: the final repetition rank for P is the highest repetition number chosen in $\wp_i$.
### V.3.1 Procedure

#### Step 0: starting with P-terminal $\wp_1$

The process starts with a P-terminal play $\wp_1$ for which O's repetition rank is 1, P's rank is high enough to allow him to win the first play. If you cannot find one, then stop the process: P does not have a winning strategy.

#### Step 1: unused decisions?

If there is no (remaining) unused decision to be taken by O in $\wp_n$ then go to step 4. Otherwise go to step 2.

#### Step 2: using up decisions

Proceeding bottom up in the flow of moves, take in $\wp_n$ O's last unused decision:<fnref n="62" />

* if it concerns a conjunction or a disjunction and has not been labeled yet, label it $[\delta_n, ...]$ or $[..., \delta_n]$ respectively for a left or right decision;

* if it concerns a conjunction or disjunction which has already been labeled, open a new play by applying one of the following substeps 2.1 or 2.2, as the case may be;

* if it concerns an implication, open two subplays following substep 2.3.

*Note: when a new play is opened P may change his repetition rank.*

#### Step 2.1: the decision concerns a challenge on a conjunction or an existential

If $\delta_n$ concerns the challenge of a conjunction or existential, then open a new play $\wp_{m=n+1}$ in which the move uses the other decision-option:

* P may change his repetition rank;

* if the decision in $\wp_n$ was a right-decision, take now the left-decision and reversewise to end up with both sides of the conjunction being challenged in the two different plays, $\wp_m$ and $\wp_n$.

* Label the decision in $\wp_m$ as $[\delta_m, \delta_n]$ or $[\delta_n, \delta_m]$, respectively, if it is a left decision or a right decision, to indicate that it used up both of the available decision-options.

* The new play then proceeds as if the $\wp_n$ challenge of the conjunction or existential had not taken place.<fnref n="63" />

* The $\wp_n$ moves previous to $\delta_n$ are imported into the new play.

* If the new play is O-terminal, go to step 3; otherwise, go to step 1.

<footnote n="62">⁶² The bottom up procedure can be understood through two aspects:</footnote>

<footnote>* from the viewpoint of O: she is trying to win a play but with the minimal cost; so if she can win by changing a minimum amount of moves, she will choose that option. The last decision reveals this economy: if O changed the first decision, then all of the play would have to be replayed; whereas simply changing the last decision allows to keep all the rest. If this last decision was not the faulty decision bringing her to lose, then she goes to the decision before last, etc. up to the very first decision.</footnote>

<footnote>* From the viewpoint of the logician: the bottom up procedure allows us to build the core of the strategy: it reveals what is important in the strategies.</footnote>

<footnote n="63">⁶³ The idea is that O has just lost the previous play with the left- or right-decision she made; so she is now looking for what has gone wrong and tries to change her way of playing in order to win. Her last decision was the left- or right-decision for the conjunction; so a way of seeing if she can win is to start the game again with exactly the same moves up to this decision, choose the other decision this time, and play with that. This is the whole idea of the core: allowing O to go through all of her possible decisions, and if in this rational way of proceeding that takes all of her opportunities into account, P still wins, then P has a winning strategy. The core is all of these relevant plays, bringing the strategy to its minimal aspect.</footnote>
**Step 2.2: the decision concerns a defence of a disjunction**

If $\delta_n$ concerns a defence of a disjunction, then open a new play $\wp_{m=n+1}$ in which the move uses the other decision-option:

* P may change his repetition rank;

* if the decision in $\wp_n$ was a right decision, take now the left decision and reversewise to end up with both sides of the disjunction being defended in the two different plays, $\wp_m$ and $\wp_n$.

* Label the decision in $\wp_m$ as $[\delta_m, \delta_n]$ or $[\delta_n, \delta_m]$, respectively, if it is a left decision or a right decision.

* The new play then proceeds as if the $\wp_n$ defence of the disjunction had not taken place.

* The $\wp_n$ moves previous to $\delta_n$ are imported into the new play.

* If the new play is O-terminal, go to step 3; otherwise, go to step 1.

**Step 2.3: the decision concerns an implication**

Recall that the two decision-options for O when one of her implications is challenged is either to counterattack (challenging the antecedent posited by P), or to defend the implication (providing the consequent), and that the branching here is not the starting of two new plays, as for the conjunction, existential, and disjunction, but only two subplays.

* If O counterattacks, start a new subplay $\wp_{n,L}$ in which figure all the moves depending on O counterattacking (and not on O defending her implication).
  If the development of the subplay yields that $\wp_n$ is O-terminal, go to step 3; otherwise go to step 1.

* If O defends an implication, start a new subplay $\wp_{n,R}$ in which figure all the moves depending on O defending her implication (and not on the counterattack).
  If the development of the subplay yields that $\wp_n$ is O-terminal, go to step 3; otherwise go to step 1.

**Step 3: O-terminal plays**

If there is no (remaining) unused decision to be taken by O in play $\wp_m$ and $\wp_n$ is O-terminal, then stop the process and start again at Step 0 with another play $\wp'_0$ won by P—if you can find any; if you cannot find any other play won by P, it simply means he lost and O has a way of winning.

**Step 4: stopping the process**

If there is no (remaining) unused decision to be taken by O in play $\wp_m$ and $\wp_n$ is P-terminal, then stop the process. P has a winning strategy.

**Two examples of the heuristical procedure**

To illustrate this procedure, let us take two examples:

1. the first on the thesis $((A \lor B) \land \neg A) \supset B$ for which a strategy has already been provided in the solution of the exercise of section III.5, p. 61;
2. the second on the thesis $((A \lor (B \land C) ) \land \neg A) \supset (B \land C) \land ((D \lor E) \supset (D \lor E)),^{64}$ which has many **O**-decisions to be processed.

Note: the labels are added after the play has been carried out, they do not belong to the play but are labels to navigate between the different plays.

$$ \textbf{First example: } ((A \lor B) \land \neg A) \supset B $$

We start the procedure with step 0: we build a **P**-terminal play $\mathcal{P}_1$ with **O**'s repetition rank being 1:

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td>$!((A \lor B) \land \neg A) \supset B$</td><td>0</td></tr><tr><td>3</td><td>$! (A \lor B) \land \neg A$</td><td>0</td><td>$n := 2$</td><td>2</td></tr><tr><td>5</td><td>$! \neg A$</td><td></td><td>$3$</td><td>? $R^\wedge$</td></tr><tr><td>7</td><td>$! A \lor B$</td><td></td><td>$3$</td><td>? $L^\wedge$</td></tr><tr><td>9</td><td>$! A$</td><td></td><td>$7$</td><td>?$_V$</td></tr><tr><td></td><td></td><td></td><td>$5$</td><td>$! A$</td></tr></tbody></table>

**P** wins (intuitionistic rules)

Now that we have our **P**-terminal play $\mathcal{P}_1$, we can proceed to step 1, finding unused **O**-decisions. Recall the **O**-decisions given in section V.2.1 p. 78:

<table><tr><td colspan="2">O has a choice and takes a decision when</td></tr><tr><td>O challenges a...</td><td>O defends a...</td></tr><tr><td>Conjunction</td><td>Disjunction</td></tr><tr><td>Existential</td><td>Implication</td></tr></table>

In $\mathcal{P}_1 O$ takes a decision move 9, when she defends a disjunction. So we proceed to step 2 of the procedure: going bottom up in the flow of the moves (from move 10 to move 0) we stop on the last unused decision—which, going bottom up is the first decision for which the two decision-options have not already been taken—, and so we stop move 9. This decision concerns a disjunction and has not been labelled yet, so we insert a label, that of the left-decision because **O** provided the left disjunct in her defence.

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td>$!((A \lor B) \land \neg A) \supset B$</td><td>0</td></tr><tr><td>3</td><td>$! (A \lor B) \land \neg A$</td><td>0</td><td>$n := 2$</td><td>2</td></tr><tr><td>5</td><td>$! \neg A$</td><td></td><td>$3$</td><td>? $R^\wedge$</td></tr></tbody></table>

<footnote n="64">⁶⁴ Notice that the structure of this thesis is the following one, using schematic letters: $((X \lor Y) \land \neg X) \supset Y) \land (Z \supset Z)$.</footnote>
<table><tr><td>7</td><td>! A ∨ B</td><td>3</td><td>? L<sup>^</sup></td><td>6</td></tr><tr><td>9</td><td>! A [δ<sub>1</sub>, ...]</td><td>7</td><td>?<sub>V</sub></td><td>8</td></tr><tr><td></td><td></td><td>5</td><td>! A</td><td>10</td></tr></table>

P wins (intuitionistic rules)

We go to step 1: there is an unused decision, so we go to step 2: going bottom up, we stop again on move 9 since that decision has still not been used up (the right decision-option has not been used). Since there is already a label on this decision, we open a new play $\mathcal{P}_2$ by following step 2.2. Since we open a new play, $\mathbf{P}$ may choose to change his repetition rank. Let us assume he does not. In this play $\mathcal{P}_2$, $\mathbf{O}$ will be taking the left decision-option, so every move up to move 9 remains identical, move 9 is the defence of the right disjunct, which we label $[\delta_1, \delta_2]$ to show both decision-options have been used, and we proceed with the play $\mathcal{P}_2$ from there on.

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!((A ∨ B) ∧ ¬A) ⊃ B</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>! (A ∨ B) ∧ ¬A</td><td>0</td><td>! B</td><td>10</td></tr><tr><td>5</td><td>! ¬A</td><td>3</td><td>? R<sup>^</sup></td><td>4</td></tr><tr><td>7</td><td>! A ∨ B</td><td>3</td><td>? L<sup>^</sup></td><td>6</td></tr><tr><td>9</td><td>! B [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>7</td><td>?<sub>V</sub></td><td>8</td></tr></tbody></table>

P wins (intuitionistic rules)

Since the play $\mathcal{P}_2$ is not $\mathbf{O}$-terminal, we do not go to step 3 but go to step 1 again, and then to step 2: we scan in $\mathcal{P}_2$ bottom up for the last unused decision, and since there are none left, we proceed to step 4. There is no unused decision left in $\mathcal{P}_2$ and the play is $\mathbf{P}$-terminal, so we stop the process. $\mathbf{P}$ has a winning strategy.

The core for the thesis $((A ∨ B) ∧ ¬A) ⊃ B$ is the collection of plays $\wp_1$ and $\wp_2$; this result demonstrates the validity of the thesis, based on the third metalogical result provided in section V.1.2, p. 75 on the soundness and completeness of tableaux.

Second example: $(( (A ∨ (B ∧ C)) ∧ ¬A ) ⊃ (B ∧ C) ) ∧ ((D ∨ E) ⊃ (D ∨ E))$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!((((A ∨ (B ∧ C)) ∧ ¬A) ⊃ (B ∧ C)) ∧ ((D ∨ E) ⊃ (D ∨ E)))</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>^</sup></td><td>0</td><td>!((A ∨ (B ∧ C)) ∧ ¬A) ⊃ (B ∧ C)</td><td>4</td></tr><tr><td>5</td><td>! (A ∨ (B ∧ C)) ∧ ¬A</td><td>4</td><td></td><td></td></tr><tr><td>7</td><td>! A ∨ (B ∧ C)</td><td>5</td><td>? L<sup>^</sup></td><td>6</td></tr><tr><td>9</td><td>! A [δ<sub>1</sub>, ...]</td><td>7</td><td>?<sub>V</sub></td><td>8</td></tr></tbody></table>
<table><tr><td>11</td><td>! ¬A</td><td>5</td><td>?</td><td>R<sup>∧</sup></td><td>10</td></tr><tr><td></td><td></td><td>11</td><td>A</td><td></td><td>12</td></tr></table>

P wins.

The last decision (move 9) has not been used up; it is a left-decision, so we label it [δ₁, ...].

<figure><img src="image_14.png" /></figure>

O can now open a new play $\wp_2$ in which she defends the other available option: the right disjunct:

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!(((A ∨ (B ∧ C)) ∧ ¬A) ∨ (B ∧ C))<br>∧ ((D ∨ E) ∨ (D ∨ E))</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∧</sup></td><td>0</td><td>!((A ∨ (B ∧ C)) ∧ ¬A) ∨ (B ∧ C)</td><td>4</td></tr><tr><td>5</td><td>! (A ∨ (B ∧ C))<br>∧ ¬A</td><td>4</td><td></td><td></td></tr><tr><td>7</td><td>! A ∨ (B ∧ C)</td><td>5</td><td>? L<sup>∧</sup></td><td>6</td></tr><tr><td>9</td><td>! B ∧ C [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>7</td><td>?<sub>∧</sub></td><td>8</td></tr><tr><td>11</td><td>? L<sup>∧</sup> [δ<sub>2</sub>, ...]</td><td>10</td><td>! B</td><td>14</td></tr><tr><td>13</td><td>! B</td><td>9</td><td>? L<sup>∧</sup></td><td>12</td></tr></tbody></table>

P wins.

The available decision-options in $\wp_2$ pertaining to the disjunction have both been used up: we now have the label [δ₁, δ₂] showing this fact.

<figure><img src="image_15.png" /></figure>

The last decision [δ₂, ...] (move 11) has not been used up so O can now open a new play $\wp_3$ in which she challenges the right-hand side of the conjunction: at move 11 in $\wp_3$, O does not play ?L<sup>∧</sup> but ?R<sup>∧</sup>. We therefore delete all the moves after move 11; we keep exactly the same moves up to move 11, and we change move 11 to the other decision-option: ?R<sup>∧</sup>. We then proceed as if the other play had not taken place:

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!(((A ∨ (B ∧ C)) ∧ ¬A) ∨ (B ∧ C))<br>∧ ((D ∨ E) ∨ (D ∨ E))</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∧</sup> [δ<sub>3</sub>, ...]</td><td>0</td><td>!((A ∨ (B ∧ C)) ∧ ¬A) ∨ (B ∧ C)</td><td>4</td></tr></tbody></table>
<table><tr><td>5</td><td>!(A ∨ (B ∧ C))<br/>∧ ¬A</td><td>4</td><td>!B ∧ C</td><td>10</td></tr><tr><td>7</td><td>!A ∨ (B ∧ C)</td><td>5</td><td>?L<sup>^</sup></td><td>6</td></tr><tr><td>9</td><td>!B ∧ C [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>7</td><td>?<sub>v</sub></td><td>8</td></tr><tr><td>11</td><td>?R<sup>^</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>10</td><td>!C</td><td>14</td></tr><tr><td>13</td><td>!C</td><td>9</td><td>?R<sup>^</sup></td><td>12</td></tr></table>

P wins.

Both of the available challenges of the conjunction have been used up in $\wp_3$: we label this move $[\delta_2, \delta_3]$ to show this fact.

<figure><img src="image_16.png" /></figure>

O has one more unused decision left, namely move 3. So we add the label $[\delta_3, ...]$ to that move and start a new play $\wp_4$ with O choosing the other option, that is, attacking the left-hand side of the conjunction in the thesis:

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>m := 1</td><td></td><td>!(((A ∨ (B ∧ C)) ∧ ¬A) ⊃ (B ∧ C)) ∧ ((D ∨ E) ⊃ (D ∨ E))</td><td>0</td></tr><tr><td>3</td><td>?R<sup>^</sup> [δ<sub>3</sub>, δ<sub>4</sub>]</td><td>0</td><td>n := 2</td><td>2</td></tr><tr><td>5</td><td>!D ∨ E</td><td>4</td><td>! (D ∨ E) ⊃ (D ∨ E)</td><td>4</td></tr><tr><td>7</td><td>?<sub>v</sub></td><td>6</td><td>!D ∨ E</td><td>6</td></tr><tr><td>9</td><td>!D [δ<sub>4</sub>, ...]</td><td>5</td><td>?<sub>v</sub></td><td>8</td></tr></tbody></table>

P wins.

The decision-options in move 3 have all been used up in $\wp_4$.

<figure><img src="image_17.png" /></figure>

Repeating step 2, a new unused decision appears: move 9, which is labelled accordingly $[\delta_4, ...]$; we start a new play $\wp_5$ with O defending the right-hand side of the disjunction:

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>m := 1</td><td></td><td>!(((A ∨ (B ∧ C)) ∧ ¬A) ⊃ (B ∧ C)) ∧ ((D ∨ E) ⊃ (D ∨ E))</td><td>0</td></tr><tr><td>3</td><td>?R<sup>^</sup> [δ<sub>3</sub>, δ<sub>4</sub>]</td><td>0</td><td>n := 2</td><td>2</td></tr><tr><td>5</td><td>!D ∨ E</td><td>4</td><td>! (D ∨ E) ⊃ (D ∨ E)</td><td>4</td></tr><tr><td>7</td><td>?<sub>v</sub></td><td>6</td><td>!D ∨ E</td><td>6</td></tr><tr><td>9</td><td>!E [δ<sub>4</sub>, δ<sub>5</sub>]</td><td>5</td><td>?<sub>v</sub></td><td>8</td></tr></tbody></table>
P wins.

Every possible option for **O** has now been tried out, we arrive at step 4, the procedure stops and defeat for **O** must be acknowledged: each of the plays are won by **P**.

The core for the thesis (((A ∨ (B ∧ C)) ∧ ¬A) ⊃ (B ∧ C)) ∧ ((D ∨ E) ⊃ (D ∨ E)) is the collection of plays $\wp_1, \wp_2, \wp_3, \wp_4$ and $\wp_5$; this result demonstrates the validity of the thesis; to obtain a tree representation of it, see the next section.

## V.4 Graphic presentation of the core (tree-shaped)

The heuristic procedure provided above shows plainly how the play level is linked to the strategy level; there is a continuity between the two. The downside of that method is that it becomes cumbersome as soon as there are more than a couple of **O**-choices to take into account; we rather use, for the strategy level, a tree presentation, which is much easier to manage and provides the added benefit that metalogical correspondences with sequent calculus and CTT-demonstrations are simplified, making the validity of dialogical demonstrations more straightforward to see (cf. chapter IX).

### The graphic presentation without the heuristic procedure

The graphic tree presentation of the core corresponds to a tree in which the nodes are the players' moves displayed in vertical sequences of dialogical **P**-steps and **O**-steps; **O**-decisions trigger a branching in the tree yielding the different plays of the core.

Here is a simple way to sketch the procedure for the development of such a tree:

1. The root of the tree is the thesis.

2. The next step is either **O** challenging the thesis or **O** positing the required initial concessions.

3. The tree develops as a vertical sequence of dialogical **P**- and **O**-steps, until the first **O**-decision occurs.

4. When the first **O**-decision occurs, split the tree in two branches and explore one of them.

5. If the branch ends with an **O**-move, then **O** won and the procedure terminates.

6. Otherwise, start exploring the second main branch and so on until the end.

*Note: As opposed to the heuristic method presented above, the graphic (tree-shaped) presentation of the core is built top to bottom, that is from the first decision of the first play and not from the last decision of the first play.*

Clearly, the whole demonstration—or **P**-winning strategy for the given thesis— could be developped directly in such a tree from, without going through the table presentation of the heuristic procedure. But the table presentation highlights the dialogical background from which the strategy emerges, and shows the continuity between the two levels.

It is important to stress this continuity because the play level is what differentiates the dialogical framework from proof-theory; but without the heuristic procedure, there seems to be a cleft in the framework between strategies and plays: there is one method for plays (table dialogues) and one method for strategies (trees), but nothing showing how the two levels unite. The two perspectives (plays and strategies) could thus be considered separate, and have often been, proof-theoricians feeling concerned only with the
dialogical demonstrations of the strategy level and not with the play level. We however believe the two levels are closely linked, and that the framework's strength and fruitfulness stems from its capacity to move seamlessly from one perspective to another. The heuristic procedure is a way of showing this link, which will be further stressed in section VII.7 through the notion of strategic reasons, and in chapter X; harmony and symmetry mentioned above (IV.3, p. 67) is another one.

We will therefore provide a procedure for building a graphic presentation of the core, but assuming that the heuristic procedure has been carried out and that the strategy is thus at hand.

## V.4.1 Building the graphic (tree-shaped) presentation of the core

We assume we actually have carried out the heuristic procedure for finding the core of a P-strategy, and have found one. We will thus be using the same assumptions as for the heuristic procedure concerning O's repetition rank, her move preferences and decisions (see V.2.1 p. 76). Here are the instructions for transforming the core of a P-strategy from the heuristic table presentation to the graphical tree presentation; thus simply providing a new exposition of the core.

### Dissociating the core from the plays it stems from

Take the collection of plays constituting the core that the heuristic procedure has yielded; proceed in the following way, from the first play to the last, and in each play from top to bottom, in order to erase the table presentation of the plays but without deleting any information; this is simply a new exposition of the core, we need to be able to go back to the other exposition and not lose important information along the way. Repetition ranks are made implicit: they do not appear in the tree but still regulate the players' moves.

i. Start the tree with the number of the move for the thesis (that is 0);

ii. Insert to the right of the number of the move the name of the player (P);

iii. Insert to the right of the player:

a. "! proposition" if the move is a statement and the proposition stated, or

b. "? request" if the move is a request and the matter of the request;

iv. Proceed from there on, following the order of the moves, by writing each player's move one under the other according to the same notation as in steps i-iii:

[number of move][P/O][! proposition/? request]

v. Insert to the right of each proposition the following indication:

a. If the move is a challenge, add [?n], where n is the number of the move being challenged.

b. If the move is a defence, add [!n], where n is the number of the move launching the challenge to which this move is a response.

*Note: this is much like erasing the lines of the dialogue table and writing the moves one under the other.*

vi. When you come across an O-decision, insert between the move and the indication of it being a challenge or a defence the indication of the O-decisions provided by the heuristic procedure, and branch the tree:

a. In the left branch of the tree, continue down the play implementing O's left decision-option;
b. in the right branch of the tree, continue down the play implementing O's right decision-option.

## Two examples of the graphic presentation of the core

In order to illustrate the procedure for building a graphic (tree-shaped) presentation of the core of the extensive form of a P-winning strategy, but also to show plainly the similarities with and the differences from the heuristic procedure, we will take the same two examples as in the previous section (V.3, see p. 83 for the first example and p. 84 for the second) and build a graphic presentation of their core.

$$ \textbf{First example: } ((A \lor B) \land \neg A) \supset B $$

We start by writing the number of the move of the thesis (0), the name of the player (P), the force of the utterance (statement: !) and the proposition stated, that is ((A ∨ B) ∧ ¬A) ⊃ B). This is the root of the tree:

$$ 0 P! ((A \lor B) \land \neg A) \supset B $$

We then proceed down the first play of the core, $\wp_1$, and write each move one under the other, recording the challenges and defences, until reaching an O-decision:

$$ 0 P! ((A \lor B) \land \neg A) \supset B $$

1 O!m := 1

2 P!n := 2

3 O!(A ∨ B) ∧ ¬A [? 0]

4 P?R^[? 3]

5 O!¬A [! 4]

6 P?L^[? 3]

7 O!A ∨ B [! 6]

8 P?_ [? 7]

We have reached the move 9 which requires O to make a decision. So we branch the tree and carry on each branch, with the left branch being $\wp_1$ from move 9 down, and the right branch being $\wp_2$ from move 9 down:

$$ 0 P! ((A \lor B) \land \neg A) \supset B $$

1 O!m := 1

2 P!n := 2

3 O!(A ∨ B) ∧ ¬A [? 0]

4 P?R^[? 3]

5 O!¬A [! 4]

6 P?L^[? 3]

7 O!A ∨ B [! 6]

8 P?_ [? 7]

9 O!A [δ₁, ...][! 8]
10 P!A [? 5]

9 O!B [δ₁, δ₂][! 8]
10 P!B [! 3]
P wins

P wins

We have thus transformed the heuristic presentation of the core into its graphic tree presentation that keeps the information of the play level and yet provides a synoptic view of all the relevant plays for a **P**-winning strategy.

$$ \textbf{Second example:} \left( \left( (A \lor (B \land C)) \land \neg A \right) \supset (B \land C) \right) \land \left( (D \lor E) \supset (D \lor E) \right) $$

Applying the same procedure to the heuristic presentation of the core for this second thesis, we obtain the following tree presentation of the core. Since there are five plays in the core ($\wp_1 - \wp_5$), there will be four branchings in the tree:

<figure><img src="image_18.png" /></figure>
# VI. LOCAL REASONS AND DIALOGUES FOR IMMANENT REASONING

In this chapter we will provide the logical framework of dialogues for immanent reasoning, the dialogical framework incorporating features of Constructive Type Theory and making explicit the players’ reasons for asserting a proposition. We will therefore be using the material provided in chapters II-V on CTT and on the standard dialogical framework and assume the reader is familiar enough with it. The framework of dialogues for immanent reasoning takes a further step in the task of making explicit the dynamic foundations of reasoning, based on equality in action: reasons adducing statements are introduced in the object-language, and the Proponent’s task in formal dialogues is to force the Opponent to provide herself the reasons the Proponent needs in order to justify his thesis; once the Opponent has produced her reasons, the Proponent uses equality rules (the Socratic rule for instance) to copy these reasons and use them to his own ends. In this respect, CTT proof-objects are adapted to the dialogical framework, yielding two new elements in our framework: local reasons, the backbone of dialogues for immanent reasoning at the play level which will be introduced in this chapter and the next (VI-VII); and strategic reasons, justifications at the strategy level corresponding to proof-objects which will be the object of chapter IX. Having local reasons in the dialogical framework provides a structure in which the reasons given and asked for actually appear in the object-language, and the Proponent can then (locally) justify his statements by explicitly copying the Opponent’s reasons for his own statements.

This chapter will first present the motivation behind dialogues for immanent reasoning (a dialogical framework) by providing some philosophical considerations in relation to the modern developments of logic (section VI.1), thus extending the enquiries initiated in the introduction. A second section (VI.2) will present a limit of the current study, that is the link between local reasons and material truth, in order to better grasp the potency of local reasons, but also to better understand the scope of formal plays through this insight into what they are not; more on material dialogues can be found in the last chapter (X). A third section (VI.3) will introduce progressively the rules defining local reasons in formal plays: formation rules (VI.3.1), the synthesis rules (VI.3.2), and the analysis rules (VI.3.3). A fourth section (VI.4) will expatiate on the link between local reasons and equality before providing an example with step-by-step explanations in order to grasp the meaning of the rules presented and how they intertwine in an actual play.

This chapter is to be read in connection with the following two chapters (VII-VII.7): chapter VII provides the rules for dialogues for immanent reasoning without much explanations, considering that this chapter VI is enough to follow on local reasons; it thus provides the local and global meanings for immanent reasoning, as well as the rules for the strategy level using local reasons; chapter VII.7 develops extensively the case of the Axiom of Choice and how the framework of dialogues for immanent reasoning is capable of dealing with it. The presentation of this framework will nonetheless be incomplete until strategic reasons are introduced in chapter IX, wrapping up in a notion the specificities of this framework, and yet still dovetailing other logical frameworks.

## VI.1 Introductory remarks on the choice of CTT

Recent developments in dialogical logic show that the Constructive Type Theory approach to meaning is very natural to the game-theoretical approaches in which
(standard) metalogical features are explicitly displayed at the object language-level.<fnref n="65" />
This vindicates, albeit in quite a different fashion, Hintikka’s plea for the fruitfulness of
game-theoretical semantics in the context of epistemic approaches to logic, semantics,
and the foundations of mathematics.<fnref n="66" />

From the dialogical point of view, the actions—such as choices—that the particle
rules associate with the use of logical constants are crucial elements of their full-fledged
(local) meaning: if meaning is conceived as constituted during interaction, then all of the
actions involved in the constitution of the meaning of an expression should be made
explicit; that is, they should all be part of the object-language.

This perspective roots itself in Wittgenstein's remark according to which one
cannot position oneself outside language in order to determine the meaning of something
and how it is *linked to syntax*; in other words, language is unavoidable: this is his
*Unhintergehbarkeit der Sprache*, one of Wittgenstein's tenets that Hintikka explicitly
rejects.<fnref n="67" /> According to this perspective of Wittgensteins, language-games are supposed to
accomplish the task of studying language from a perspective that acknowledges its
*internalized feature*. This is what underlies the approach to meaning and syntax of the
dialogical framework in which all the speech-acts that are relevant for rendering the
meaning and the "formation" of an expression are made explicit. In this respect, the
metalogical perspective which is so crucial for model-theoretic conceptions of meaning
does not provide a way out. It is in such a context that Lorenz writes:

> Also propositions of the metalanguage require the understanding of propositions, [...] and thus cannot in a sensible way have this same understanding as their proper object. The thesis that a property of a propositional sentence must always be internal, therefore amounts to articulating the insight that in propositions about a propositional sentence this same propositional sentence does not express a meaningful proposition anymore, since in this case it is not the propositional sentence that is asserted but something about it.

> Thus, if the original assertion (i.e., the proposition of the ground-level) should not be abrogated, then this same proposition should not be the object of a metaproposition [...].<fnref n="68" />

> While originally the semantics developed by the picture theory of language aimed at
determining unambiguously the rules of “logical syntax” (i.e. the logical form of linguistic
expressions) and thus to justify them [...]—now language use itself, without the mediation of
theoretic constructions, merely via “language games”, should be sufficient to introduce the
talk about “meanings” in such a way that they supplement the syntactic rules for the use of
ordinary language expressions (superficial grammar) with semantic rules that capture the
understanding of these expressions (deep grammar).<fnref n="69" />

Similar criticism to the metalogical approach to meaning has been raised by Göran
Sundholm (1997; 2001) who points out that the standard model-theoretical semantic turns
semantics into a meta-mathematical formal object in which syntax is linked to meaning
by the assignation of truth values to uninterpreted strings of signs (formulae). Language
does not express *content* anymore, but it is rather conceived as a system of signs that
speak *about* the world—provided a suitable metalogical link between the signs and the
world has been fixed. Moreover, Sundholm (2016) shows that the cases of quantifier-
dependences motivating Hintikka’s IF-logic can be rendered in the CTT framework.
What we will here add to Sundholm’s observation is that even the interactive features of

<footnote n="65">⁶⁵ See for instance (Clerbout & Rahman, 2015) (Rahman & Clerbout, 2013; 2015), (Dango, 2014; 2015; 2016), (Jovanovic, 2013; 2015), (Rahman, Clerbout, & McConaughey, 2014) (Rahman, Clerbout, & Jovanovic, 2015).</footnote>

<footnote n="66">⁶⁶ Cf. (Hintikka, 1973; 1983; 1996b).</footnote>

<footnote n="67">⁶⁷ Hintikka (1997) shares this rejection with all those who endorse model-theoretical approaches to meaning.</footnote>

<footnote n="68">⁶⁸ (Lorenz, 1970, p. 75), translated from the German by Shahid Rahman.</footnote>

<footnote n="69">⁶⁹ (Lorenz, 1970, p. 109), translated from the German by Shahid Rahman.</footnote>
these dependences can be given a CTT formulation, provided the latter is developed
within a dialogical setting.

Ranta (1988) was the first to link game-theoretical approaches with CTT. Ranta took Hintikka's (1973) Game-Theoretical Semantics (GTS) as a case study, though his point does not depend on that particular framework: in game-based approaches, a proposition is a set of winning strategies for the player stating the proposition.<fnref n="70" /> In game-based approaches, the notion of truth is at the level of such winning strategies. Ranta's idea should therefore in principle allow us to apply, safely and directly, instances of game-based methods taken from CTT to the pragmatist approach of the dialogical framework.

From the perspective of a general game-theoretical approach to meaning however,
reducing a proposition to a set of winning strategies is quite unsatisfactory. This is
particularly clear in the dialogical approach in which different levels of meaning are
carefully distinguished: there is indeed the level of strategies, but there is also the level of
plays in the analysis of meaning which can be further analysed into local, global and
material levels. The constitutive role of the play level for developing a meaning
explanation has been stressed by Kuno Lorenz in his (2001) paper:

> Fully spelled out it means that for an entity to be a proposition there must exist a dialogue game associated with this entity, i.e., the proposition A, such that an individual play of the game where A occupies the initial position, i.e., a dialogue D(A) about A, reaches a final position with either win or loss after a finite number of moves according to definite rules: the dialogue game is defined as a finitary open two-person zero-sum game. Thus, propositions will in general be dialogue-definite, and only in special cases be either proof-definite or refutation-definite or even both which implies their being value-definite.

> Within this game-theoretic framework [...] truth of A is defined as existence of a winning strategy for A in a dialogue game about A; falsehood of A respectively as existence of a winning strategy against A.<fnref n="71" />

Given the distinction between the play level and the strategy level, and deploying
within the dialogical framework the CTT-explicitation program, it seems natural to
distinguish between *local* reasons and *strategic* reasons: only the latter correspond to the
notion of *proof-object* in CTT and to the notion of *strategic-object* of Ranta. In order to
develop such a project we enrich the language of the dialogical framework with
statements of the form “*p* : A”. In such expressions, what stands on the left-hand side of
the colon (here *p*) is what we call a *local reason*; what stands on the right-hand side of
the colon (here *A*) is a proposition (or set).<fnref n="72" /> Strategic reasons will be introduced in
chapter IX.

The *local* meaning of such statements results from the rules describing how to
compose (*synthesis*) within a play the suitable local reasons for the proposition *A* and
how to separate (*analysis*) a complex local reason into the elements required by the
composition rules for *A*. The synthesis and analysis processes of *A* are built on the
formation rules for *A*.

VI.2 Local reasons and material truth

The most basic contribution of a local reason is its contribution to a material
dialogue involving an elementary proposition. Informally, we can say that if the

<footnote n="70">⁷⁰ That player can be called Player 1, Myself or Proponent.</footnote>

<footnote n="71">⁷¹ (Lorenz, 2001, p. 258).</footnote>

<footnote n="72">⁷² See (Rahman, Redmond, & Clerbout, 2017), (Clerbout & Rahman, 2015) (Rahman & Clerbout, 2013; 2015).</footnote>
Proponent **P** states the elementary proposition *A*, it is because **P** claims that he can bring forward a reason in defence of his statement. It is the Socratic rule that determines the precise form of that local reason, *specific to A*.<fnref n="73" /> Our study focuses on formal—not material—dialogues, but we will still provide some basic elements on material truth in regard to local reasons so as to render in a clearer fashion the limits of our study and its philosophical background, the meaning of formal plays by contrast with what they are not, and the further work that can be carried out from this presentation of dialogues for immanent reasoning.

## Approaching material truth

Assume the Proponent states that 1 is an odd number:

P!1 is an odd number

the Opponent can then express the following demand, asking **P** for reasons for his statement:

O! find a natural number n such that 1 = 2.n + 1

Because of the restriction the Socratic rule imposes on **P**, he can defend his statement by choosing "0", provided that **O** has already endorsed the statement "0 is a natural number" (0: N). This produces *material truth*.

Material truth can then be described in the following way: the statement that a given proposition is materially true requires displaying a local reason *specific to that very proposition*.

## Material truth and local reasons

A local reason adduced in defence of a proposition thus prefigures a material dialogue displaying the specific content of that proposition. This constitutes the bottom of the normative approach to meaning of the dialogical framework: *use* (dialogical interaction) is to be understood as *use prescribed by a rule of dialogical interaction*. This applies not only to the meaning of logical constants, but also to the meaning of elementary propositions. This is what Jaroslav Peregrin (2014, pp. 2-3) calls the *role* of a linguistic statement: according to this terminology, and if we place his suggestion in our dialogical setting, we can say that the meaning of an elementary proposition amounts to its *role* in that form of interaction that the Socratic rule for a material dialogue prescribes for that specific proposition.<fnref n="74" /> It follows from such a perspective that material dialogues are important not only for the general question of the normativity of logic, but also for the elaboration of a language with content.

## Material dialogues and formal dialogues

Summing up, what distinguishes formal dialogues from material dialogues resides in the following:

* The formulation of the Socratic rule of a formal dialogue prescribes a form of interaction based only on the meaning of the logical constant(s) involved, irrespective of the meaning of the elementary propositions in the scope of that constant.

<footnote n="73">⁷³ Recall that the Socratic rule does not prohibit the Opponent **O** from challenging an elementary proposition of **P**; the rule only restricts **P**'s authorized moves.</footnote>

<footnote n="74">⁷⁴ In the last chapter (0) we come back to the relation between normativity and material dialogues.</footnote>
* The choice of the local reason for the elementary propositions involved is left to the authority of the Opponent.

In other words, in a formal dialogue the Socratic rule is *not* specific to any elementary proposition in particular, but it is *general*; definitions that distinguish one proposition from another are introduced during the game according to the local meaning of the logical constant involved: formal dialogues are the purest kind of immanent reasoning.

The synthesis and analysis of local reasons for a proposition *A* are determined by the actions prescribed by the Socratic rule specific to the kind of play in which *A* has been stated:

* If the play is *material*, the Socratic rule will describe a kind of action specific to the formation of *A*.

* If the play is *formal*, as assumed in the main body of our study, the Socratic rule will allow **O** to bring forward the relevant local reasons during the development of the play.

The point is that in formal dialogues, when the Opponent challenges the thesis, the thesis is assumed to be well-formed up to the logical constants, so the formation of the elementary statements is displayed during the development of the dialogue and left to the authority of **O**. So the formation rule for elementary statements does not really take place at the level of local meaning but at level of global meaning.

Our study here focuses on *formal plays* of immanent reasoning. A thorough development of material dialogues will be left for future work, though in the last chapter of the book (chapter X) we will provide some insights as to their structure and discuss how to "internalize" empirical content within a game.

Since the local reasons for the elementary statements are left to **O**'s authority, what we now need is to describe the process of *synthesis* and *analysis* for local reasons of the logical constants. However, before starting to enrich the language of the standard dialogical framework with local reasons for logical constants let us discuss how to implement a dialogical notion of *formation rules*. The formation rules together with the synthesis and analysis rules settle the local meaning of dialogues for immanent reasoning.

## VI.3 The local meaning of local reasons

Here is an introduction of the formation rules (section VI.3.1), the synthesis rules (section VI.3.2), and the analysis rules (section VI.3.3) for local reasons. But we first need to make a clarification on statements and add a piece of notation to the framework:

### Statements in dialogues for immanent reasoning

Dialogues are games of giving and asking for reasons; yet in the standard dialogical framework, the reasons for each statement are left implicit and do not appear in the notation of the stament: we have statements of the form $X!A$ for instance where *A* is an elementary proposition. The framework of dialogues for immanent reasoning allows to have explicitly the reason for making a statement, statements then have the form $X a : A$ for instance where *a* is the (local) reason $X$ has for stating the proposition $A$. But even in dialogues for immanent reasoning, all reasons are not always provided, and sometimes statements have only implicit reasons for bringing the proposition forward, taking then the same form as in the standard dialogical framework: $X!A$. Notice that when (local)
reasons are not explicit, an exclamation mark is added before the proposition: the statement then has an implicit reason for being made.

A statement is thus both a proposition and its local reason, but this reason may be left implicit, requiring then the use of the exclamation mark.

### Adding concessions

In the context of the dialogical conception of CTT we also have statements of the form

$$X ! \pi(x_1, \dots, x_n) [x_i : A_i]$$

where "π" stands for some statement in which $(x_1, \dots, x_n)$ occurs, and where $[x_i : A_i]$ stands for some condition under which the statement $\pi(x_1, \dots, x_n)$ has been brought forward. Thus, the statement reads:

X states that $\pi(x_1, \dots, x_n)$ under the condition that the antagonist concedes $x_i : A_i$.

We call required concessions the statements of the form $[x_i : A_i]$ that condition a claim. When the statement is challenged, the antagonist is accepting, through his own challenge, to bring such concessions forward. The concessions of the thesis, if any, are called initial concessions. Initial concessions can include formation statements such as A : prop, B : prop, for the thesis, $A \supset B : prop$.

### VI.3.1 Formation rules for local reasons: an informal overview

It is presupposed in standard dialogical systems that the players use well-formed formulas (wff). The well formation can be checked at will, but only with the usual meta reasoning by which one checks that the formula does indeed observe the definition of a wff. We want to enrich our CTT-based dialogical framework by allowing players themselves to first enquire on the formation of the components of a statement within a play. We thus start with dialogical rules explaining the formation of statements involving logical constants (the formation of elementary propositions is governed by the Socratic rule, see the discussion above on material truth). In this way, the well formation of the thesis can be examined by the Opponent before running the actual dialogue: as soon as she challenges it, she is de facto accepting the thesis to be well formed (the most obvious case being the challenge of the implication, where she has to state the antecedent and thus explicitly endorse it). The Opponent can ask for the formation of the thesis before launching her first challenge; defending the formation of his thesis might for instance bring the Proponent to state that the thesis is a proposition, provided, say, that A is a set is conceded; the Opponent might then concede that A is a set, but only after the constitution of A has been established, though if this were the case, we would be considering the constitution of an elementary statement, which is a material consideration, not a formal one.

These rules for the formation of statements with logical constants are also particle rules which are added to the set of particle rules determining the local meaning of logical constants (called synthesis and analysis of local reasons in the framework of dialogues for immanent reasoning).

These considerations yield the following condensed presentation of the logical constants (plus falsum), in which "K" in AKB " expresses a connective, and "Q" in "(Qx : A) B(x) " expresses a quantifier.
<table><caption>Table 12: Formation rules, condensed presentation</caption><thead><tr><th></th><th>Connective</th><th>Quantifier</th><th>Falsum</th></tr></thead><tbody><tr><th>Move</th><td>X A:B : prop</td><td>X (Qx : A) B(x) : prop</td><td>X ⊥ : prop</td></tr><tr><th>Challenge</th><td>Y ?<sub>F<sub>K</sub>1</sub> and/or<br>Y ?<sub>F<sub>K</sub>2</sub></td><td>Y ?<sub>F<sub>A1</sub></sub> and/or<br>Y ?<sub>F<sub>A2</sub></sub></td><td>—</td></tr><tr><th>Defence</th><td>X A : prop (resp.)<br>X B : prop</td><td>X A : set (resp.)<br>X B(x) : prop (x : A)</td><td>—</td></tr></tbody></table>

Because of the *no entity without type* principle, it seems at first glance that we should specify the type of these actions during a dialogue by adding the type “*formation-request*”. But as it turns out, we should not: an expression such as “`?F: formation-request`” is a judgement that some action `?F` is a formation-request, which should not be confused with the actual act of requesting. We also consider that the force symbol `?F` makes the type explicit.

### VI.3.2 Synthesis of local reasons

The synthesis rules of local reasons determine how to produce a local reason for a statement; they include rules of interaction indicating how to produce the local reason that is required by the proposition (or set) in play, that is, they indicate what kind of dialogic action—what kind of move—must be carried out, by whom (challenger or defender), and what reason must be brought forward.

#### Implication

For instance, the synthesis rule of a local reason for the implication $A \supset B$ stated by player X indicates:

i. that the challenger Y must state the antecedent (while providing a local reason for it): $Y p_1 : A$.<fnref n="75" />

ii. that the defender X must respond to the challenge by stating the consequent (with its corresponding local reason): $X p_2 : B$.

In other words, the rules for the synthesis of a local reason for implication are as follows:

<table><caption>Table 13: Synthesis of a local reason for implication</caption><thead><tr><th></th><th>Implication</th></tr></thead><tbody><tr><th>Move</th><td>X ! A ⊃ B</td></tr><tr><th>Challenge</th><td>Y p<sub>1</sub> : A</td></tr><tr><th>Defence</th><td>X p<sub>2</sub> : B</td></tr></tbody></table>

Notice that the initial statement ($X ! A \supset B$) does not display a local reason for the claim the implication holds: player X simply states that he has some reason supporting the claim. We express such kind of move by adding an *exclamation mark*.

<footnote n="75">⁷⁵ This notation is a variant of the one used by (Keiff, 2004).</footnote>
before the proposition. The further dialogical actions indicate the moves required for producing a local reason in defence of the initial claim.

### Conjunction

The synthesis rule for the conjunction is straightforward:

<table><caption>Table 14: synthesis of a local reason for conjunction</caption><thead><tr><th></th><th>Conjunction</th></tr></thead><tbody><tr><th>Move</th><td>X ! A ∧ B</td></tr><tr><th>Challenge</th><td>Y ? L<sup>^</sup> or Y ? R<sup>^</sup></td></tr><tr><th>Defence</th><td>X p<sub>1</sub>: A (resp.) X p<sub>2</sub>: B</td></tr></tbody></table>

### Disjunction

For disjunction, as we know from the standard rules, it is the defender who will choose which side he wishes to defend: the challenge consists in requesting of the defender that he chooses which side he will be defending:

<table><caption>Table 15: Synthesis of a local reason for disjunction</caption><thead><tr><th></th><th>Disjunction</th></tr></thead><tbody><tr><th>Move</th><td>X ! A ∨ B</td></tr><tr><th>Challenge</th><td>Y ?<sub>ν</sub></td></tr><tr><th>Defence</th><td>X p<sub>1</sub>: A or X p<sub>2</sub>: B</td></tr></tbody></table>

### The general structure for the synthesis of local reasons

More generally, the rules for the synthesis of a local reason for a constant $\mathcal{K}$ is determined by the following triplet:

<table><caption>Table 16: general structure for the synthesis of a local reason for a constant</caption><thead><tr><th></th><th>A constant <i>K</i></th><th>Implication</th><th>Conjunction</th><th>Disjunction</th></tr></thead><tbody><tr><th>Move</th><td>X ! φ[<i>K</i>]<br>X claims that φ</td><td>X ! A ⊃ B</td><td>X ! A ∧ B</td><td>X ! A ∨ B</td></tr><tr><th>Challenge</th><td>Y asks for the reason<br>backing such a claim</td><td>Y p<sub>1</sub>: A</td><td>Y ? L<sup>^</sup> or Y ? R<sup>^</sup></td><td>Y ?<sub>ν</sub></td></tr><tr><th>Defence</th><td>X p : φ[<i>K</i>]<br>X states the local reason p for<br>φ[<i>K</i>] according to the rules<br>for the synthesis of local<br>reasons prescribed for <i>K</i>.</td><td>X p<sub>2</sub>: B</td><td>X p<sub>1</sub>: A<br>(resp.)<br>X p<sub>2</sub>: B</td><td>X p<sub>1</sub>: A<br>or<br>X p<sub>2</sub>: B</td></tr></tbody></table>
### VI.3.3 Analysis of local reasons

Apart from the rules for the synthesis of local reasons, we need rules that indicate how to parse a complex local reason into its elements: this is the *analysis* of local reasons. In order to deal with the complexity of these local reasons and formulate general rules for the analysis of local reasons (at the play level), we introduce certain operators that we call *instructions*, such as $L^v(p)$ or $R^v(p)$.

#### Approaching the analysis rules for local reasons

Let us introduce these instructions and the analysis of local reasons with an example: player $X$ states the implication $(A \land B) \supset A$. According to the rule for the synthesis of local reasons for an implication, we obtain the following:

<table><tr><td>Move</td><td>X ! (A &amp; B) ⊃ B</td></tr><tr><td>Challenge</td><td>Y p<sub>1</sub> : A &amp; B</td></tr></table>

Recall that the synthesis rule prescribes that $X$ must now provide a local reason for the consequent; but instead of defending his implication (with $X p_2: B$ for instance), $X$ can choose to parse the reason $p_1$ provided by $Y$ in order to force $Y$ to provide a local reason for the right-hand side of the conjunction that $X$ will then be able to copy; in other words, $X$ can force $Y$ to provide the local reason for $B$ out of the local reason $p_1$ for the antecedent $A \land B$ of the initial implication. The analysis rules prescribe how to carry out such a parsing of the statement by using *instructions*. The rule for the analysis of a local reason for the conjunction $p_1: A \land B$ will thus indicate that its defence includes expressions such as

* the left instruction for the conjunction, written $L^v(p_1)$, and

* the right instruction for the conjunction, written $R^v(p_1)$.

These instructions can be informally understood as carrying out the following step: for the defence of the conjunction $p_1: A \land B$ separate the local reason $p_1$ in its left (or right) component so that this component can be adduced in defence of the left (or right) side of the conjunction.

Here is a play with local reasons for the thesis $(A \land B) \supset B$ using instructions:

<table><thead><tr><th></th><th>O</th><th></th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td></td><td>! $(A \land B) \supset B$</td><td>0</td></tr><tr><td>3</td><td>$p_1 : A \land B$</td><td>0</td><td></td><td>$n := 2$</td><td>2</td></tr><tr><td>5</td><td>$R^v(p_1) : B$</td><td></td><td>3</td><td>$R^v(p_1) : B$</td><td>6</td></tr><tr><td></td><td></td><td></td><td></td><td>$? R^v$</td><td>4</td></tr></tbody></table>

P wins.

In this play, $P$ uses the analysis of local reasons for conjunction in order to force $O$ to state $R^v(p_1) : B$, that is to provide a local reason$^{76}$ for the elementary statement $B$; $P$ can then copy that local reason in order to back his statement $B$, the consequent of his initial implication. With these local reasons, we explicitly have in the object-language the reasons that are given and asked for and which constitute the essence of an argumentative dialogue.

<footnote>$^{76}$ Speaking of local reasons is a little premature at this stage, since only instructions are provided and not actual local reasons; but the purpose is here to give the general idea of local reasons, and instructions are meant to be resolved into proper local reasons, which requires only an extra step.</footnote>
## The general structure for the analysis rules of local reasons

<table><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Conjunction</th><td><i>X</i> p: A ∧ B</td><td><i>Y</i> ? <i>L</i><sup>^</sup><br>or<br><i>Y</i> ? <i>R</i><sup>^</sup></td><td><i>X</i> <i>L</i><sup>^</sup>(<i>p</i>)<sup><i>X</i></sup>: A<br>(resp.)<br><i>X</i> <i>R</i><sup>^</sup>(<i>p</i>)<sup><i>X</i></sup>: B</td></tr><tr><th>Disjunction</th><td><i>X</i> p: A ∨ B</td><td><i>Y</i> ?<sub>ν</sub></td><td><i>X</i> <i>L</i><sup>ν</sup>(<i>p</i>)<sup><i>X</i></sup>: A<br>or<br><i>X</i> <i>R</i><sup>ν</sup>(<i>p</i>)<sup><i>X</i></sup>: B</td></tr><tr><th>Implication</th><td><i>X</i> p: A ⊃ B</td><td><i>Y</i> <i>L</i><sup>⊺</sup>(<i>p</i>)<sup><i>Y</i></sup>: A</td><td><i>X</i> <i>R</i><sup>⊺</sup>(<i>p</i>)<sup><i>X</i></sup>: B</td></tr></tbody></table>

The superscripts with the player label indicate which player is entitled to decide how to resolve the instruction, that is, to decide which local reason to bring forward when carrying out the instruction.

## Interaction procedures embedded in instructions

Carrying out the prescriptions indicated by instructions require the following three interaction-procedures:

1. *Resolution of instructions:* this procedure determines how to carry out the instructions prescribed by the rules of analysis and thus provide an actual local reason.

2. *Substitution of instructions:* this procedure ensures the following; once a given instruction has been carried out through the choice of a local reason, say *b*, then every time the same instruction occurs, it will always be substituted by the same local reason *b*.

3. *Application of the Socratic rule:* the Socratic rule prescribes how to constitute equalities out of the resolution and substitution of instructions, linking synthesis and analysis together.

Let us discuss how these rules interact and how they lead to the main thesis of this study, namely that immanent reasoning is equality in action.

## VI.4 From Reasons to Equality

As we have already discussed to some extent one of the most salient features of dialogical logic is the so-called, *Socratic rule* (or Copy-cat rule in the standard—that is, non-CTT—context), establishing that the Proponent can play an elementary proposition only if the Opponent has played it previously.

The Socratic rule is a characteristic feature of the dialogical approach: other game-based approaches do not have it. With this rule the dialogical framework comes with an internal account of elementary propositions: an account in terms of interaction only, without depending on metalogical meaning explanations for the non-logical vocabulary. More prominently, this means that the dialogical account does not rely—contrary to Hintikka's GTS games—on the model-theoretical approach to meaning for elementary propositions.

The rule has a clear Platonist and Aristotelian origin and sets the terms for what it is to carry out a *formal argument*: see for instance Plato's *Gorgias* (472b-c). We can sum up the underlying idea with the following statement:
there is no better grounding of an assertion within an argument than indicating that it
has been already conceded by the Opponent or that it follows from these concessions.<fnref n="77" />

What should be stressed here are the following two points:

1. formality is understood as a kind of *interaction*; and

2. formal reasoning *should not* be understood here as devoid of content and reduced to purely syntactic moves.

Both points are important in order to understand the criticism often raised against formal reasoning in general, and in logic in particular. It is only quite late in the history of philosophy that formal reasoning has been reduced to syntactic manipulation—presumably the first explicit occurrence of the syntactic view of logic is Leibniz’s “pensée aveugle” (though Leibniz’s notion was not a reductive one). Plato and Aristotle’s notion of formal reasoning is neither “static” nor “empty of meaning”.<fnref n="78" /> In the Ancient Greek tradition logic emerged from an approach of assertions in which meaning and justification result from what has been brought forward during argumentative interaction. According to this view, dialogical interaction is constitutive of meaning.

Some former interpretations of standard dialogical logic did understand formal plays in a purely syntactic manner. The reason for this is that the standard version of the framework is not equipped to express meaning at the object-language level: there is no way of asking and giving reasons for elementary propositions. As a consequence, the standard formulation simply relies on a syntactic understanding of *Copy-cat moves*, that is, moves entitling **P** to copy the elementary propositions brought forward by **O**, regardless of its content.

The dialogical approach to CTT (dialogues for immanent reasoning) however provides a fine-grain study of the contentual aspects involved in formal plays, much finer than the one provided by the standard dialogical framework. In dialogues for immanent reasoning which we are now presenting, a statement is constituted both by a proposition and by the (local) reason brought forward in defence of the claim that the proposition holds. In formal plays not only is the Proponent allowed to copy an elementary proposition stated by the Opponent, as in the standard framework, but he is also allowed to adduce in defence of that proposition the *same* local reason brought forward by the Opponent when she defended that same proposition. Thus immanent reasoning and equality in action are intimately linked. In other words, a formal play displays the *roots of the content* of an elementary proposition, and *not* a syntactic manipulation of that proposition.

Statements of definitional equality emerge precisely at this point. In particular
reflexivity statements such as

$p = p : A$

express from the dialogical point of view the fact that if **O** states the elementary proposition **A**, then **P** can do the same, that is, play the same move and do it on the same grounds which provide the meaning and justification of **A**, namely **p**.

<footnote n="77">⁷⁷ Recent work (Crubellier, 2014, pp. 11-40) and (Crubellier, Marion, McConaughey, & Rahman, 2018) claim that this rule is central to the interpretation of dialectic as the core of Aristotle's logic. Neither Ian Lukasiewicz's (1957) famous reconstruction of Aristotle's syllogistic, nor the Natural deduction approach of Kurt Ebbinghaus (1964) and John Corcoran (1974) deploy this rule, but Marion and Rückert (2015) showed that this rule displays Aristotle's view on universal quantification.</footnote>

<footnote n="78">⁷⁸ (Smith R., 1982; Smith R., 1989), (Crubellier, 2014).</footnote>
These remarks provide an insight only on simple forms of equality and barely touch upon the finer-grain distinctions discussed above; we will be moving to these by means of a concrete example in which we show, rather informally, how the combination of the processes of analysis, synthesis, and resolution of instructions lead to equality statements.

### Example

Assume that the Proponent brings forward the thesis $(A \land B) \supset (B \land A)$:

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr></tbody></table>

Both players then choose their repetition ranks:

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td></tr><tr><td></td><td>p : A ∧ B</td><td>0</td></tr></tbody></table>

O must now challenge the implication if she accepts to enter into the discussion. The rule for the synthesis of a local reason for implication (provided above) stipulates that in order to challenge the thesis, O must state the antecedent and provide a local reason for it:

Synthesis of a local reason for conjunction

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>0</td></tr></tbody></table>

According to the same synthesis-rule P must now state the consequent, which he is allowed to do because the consequent is not elementary:

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>0</td></tr></tbody></table>

The Opponent launches her challenge asking for the left component of the local reason *q* provided by P, an application of the rule for the analysis of a local reason for a conjunction described above.

Analysis of a local reason for conjunction

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>0</td></tr><tr><td>5</td><td>? L<sup>∧</sup></td><td>4</td></tr></tbody></table>

Assume that P responds immediately to this challenge:

<table><thead><tr><th>O</th><th>P</th></tr></thead></table>
<table><tr><td></td><td></td><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>0</td><td>q : B ∧ A</td><td>4</td></tr><tr><td>5</td><td>? L<sup>^</sup></td><td>4</td><td>L<sup>^</sup>(q) : B</td><td>6</td></tr></table>

O will now ask for the resolution of the instruction:

Resolution of an instruction

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>q : B ∧ A</td><td>4</td></tr><tr><td>5</td><td>? L<sup>^</sup></td><td>L<sup>^</sup>(q) : B</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>^</sup>(q)</td><td></td><td></td></tr></tbody></table>

In this move 7, O is asking P to carry out the instruction $L^>(q)$ by bringing forward the local reason of his choice. The act of choosing such a reason and replacing the instruction for it is called *resolving the instruction*.

In this case, resolving the instruction will lead P to bring forward an *elementary statement*—that is, a statement in which both the local reason and the proposition are elementary, which falls under the restriction of the Socratic rule. The idea for P then is to postpone his answer to the challenge launched with move 7 and to force O to choose a local reason first so as to copy it in his answer to the challenge. This yields a further application of the *analysis rule* for the conjunction:

O responds according to the *analysis rule*

O responds to the challenge by choosing the local reason b

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>! (A ∧ B) ⊃ (B ∧ A)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>p : A ∧ B</td><td>q : B ∧ A</td><td>4</td></tr><tr><td>5</td><td>? L<sup>^</sup></td><td>L<sup>^</sup>(q) : B</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>^</sup>(q)</td><td>b : B</td><td>12</td></tr><tr><td>9</td><td>R<sup>^</sup>(p) : B</td><td>? R<sup>^</sup></td><td>8</td></tr><tr><td>11</td><td>b : B</td><td>? .../R<sup>^</sup>(p)</td><td>10</td></tr></tbody></table>

P launches his challenge asking for the right side of the concession move 3

P asks O to resolve the instruction by providing a local reason

P wins.

Move 11 thus provides P with the information he needed: he can then copy O's choice to answer the challenge she launched at move 7.

*Note:* It should be clear that a similar end will come about if O starts by challenging the right component of the conjunction statement, instead of challenging the left component.

## Analysis of the example

Let us now go deeper in the analysis of the example and make explicit what happened during the play:
# VII. THE DIALOGICAL ROOTS OF EQUALITY: DIALOGUES FOR IMMANENT REASONING

In this chapter we will spell out all the relevant rules of dialogues for immanent reasoning, that is, the dialogical framework incorporating features of Constructive Type Theory—a dialogical framework making the players’ reasons for asserting a proposition explicit. The rules can be divided, just as in the standard framework, into rules determining local meaning and rules determining global meaning. These include:

1. Concerning *local meaning* (section VII.1):

a. formation rules (p. 105);

b. rules for the synthesis of local reasons (p. 108); and

c. rules for the analysis of local reasons (p. 109).

2. Concerning *global meaning*, we have the following (structural) rules (section VII.2):

a. rules for the resolution of instructions (p. 112);

b. rules for the substitution of instructions (p. 113);

c. equality rules determined by the application of the Socratic rules (p. 113); and

d. rules for the transmission of equality (p. 115).

We will be presenting these rules in this order in the next two sections, along with the adaptation of the other structural rules to dialogues for immanent reasoning in the second section. The following section (VII.4) provides a series of exercises for the play level.

A fourth section (VII.5) will deal with the strategic level of dialogues for immanent reasoning, and will be followed with solved exercises (VII.6).

A final section (VII.7) will introduce *strategic reasons*, a fundamental notion for dialogues for immanent reasoning, and will be accompanied with two examples showing how to build these reasons of a special kind.

## VII.1 Local meaning in dialogues for immanent reasoning

### VII.1.1 The formation rules

**Formation rules for logical constants and falsum**

The formation rules for *logical constants* and for *falsum* are given in the following table. Notice that a statement ‘⊥ : **prop**’ cannot be challenged; this is the dialogical account for falsum ‘⊥’ being by definition a proposition.

<table><caption>Table 17: Formation rules</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Conjunction</th><td>X A ∧ B: prop</td><td>Y ? F<sub>Λ1</sub><br>or<br>Y ? F<sub>Λ2</sub></td><td>X A: prop<br>(resp.)<br>X B: prop</td></tr><tr><th>Disjunction</th><td>X A ∨ B: prop</td><td>Y ? F<sub>ν1</sub><br>or<br>Y ? F<sub>ν2</sub></td><td>X A: prop<br>(resp.)<br>X B: prop</td></tr></tbody></table>
<table><tr><td>Implication</td><td>X A ⊃ B: prop</td><td>Y ? F<sub>1</sub> or Y ? F<sub>2</sub></td><td>X A: prop (resp.) X B: prop</td></tr><tr><td>Universal quantification</td><td>X (∀x: A)B(x): prop</td><td>Y ? F<sub>∀1</sub> or Y ? F<sub>∀2</sub></td><td>X A: set (resp.) X B(x): prop[x: A]</td></tr><tr><td>Existential quantification</td><td>X (∃x: A)B(x): prop</td><td>Y ? F<sub>∃1</sub> or Y ? F<sub>∃2</sub></td><td>X A: set (resp.) X B(x): prop[x: A]</td></tr><tr><td>Subset separation</td><td>X {x : A | B(x)}: prop</td><td>Y ? F<sub>1</sub> or Y ? F<sub>2</sub></td><td>X A: set (resp.) X B(x): prop[x: A]</td></tr><tr><td>Falsum</td><td>X ⊥: prop</td><td>—</td><td>—</td></tr></table>

## The substitution rule within dependent statements

The following rule is not really a formation-rule but is very useful while applying formation rules where one statement is dependent upon the other such as $B(x): prop[x: A]$.<fnref n="79" />

<table><caption>Table 18: Substitution rule within dependent statements (subst-D)</caption><tr><td></td><td>Move</td><td>Challenge</td><td>Defence</td></tr><tr><td>Subst-D</td><td>X π(x<sub>1</sub>, ..., x<sub>n</sub>)[x<sub>i</sub>: A<sub>i</sub>]</td><td>Y τ<sub>1</sub>: A<sub>1</sub>, ..., τ<sub>n</sub>: A<sub>n</sub></td><td>X π(τ<sub>1</sub>, ..., τ<sub>n</sub>)</td></tr></table>

In the formulation of this rule, “π” is a statement and “τ<sub>i</sub>” is a local reason of the form either a<sub>i</sub>: A<sub>i</sub> or x<sub>i</sub>: A<sub>i</sub>.

A particular case of the application of Subst-D is when the challenger simply chooses the same local reasons as those occurring in the concession of the initial statement. This is particularly useful in the case of formation plays:

## Example of a formation-play

Here is an example of a formation play with some explanation. The standard development rules are enough to understand the following plays (see the rules provided in chapter III or IV).

In this example, the Opponent provides initial concession before the Proponent states his thesis. Thus the Proponent’s thesis is

$$ (\forall x: A)(B(x) \supset C(x)) : prop $$

given these three provisos that appear as initial concessions by the Opponent:

$A : set,$

$B(x) : prop [x : A]$

$C(x) : prop [x : A],$

<footnote n="79">⁷⁹ This rule is an expression at the level of plays of the rule for the substitution of variables in a hypothetical judgement. See (Martin-Löf, 1984, pp. 9-11).</footnote>
This yields the following play:

<table><caption>Play 10: formation-play with initial concessions: first decision-option of O</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>A : set</td><td colspan="2"></td></tr><tr><td>0.2</td><td>B(x) : prop [x : A]</td><td colspan="2"></td></tr><tr><td>0.3</td><td>C(x) : prop [x : A]</td><td>(∀x : A) B(x) ⊃ C(x) : prop</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? F<sub>∀1</sub></td><td>A : set</td><td>4</td></tr></tbody></table>

P wins.

**Explanation:**

* 0.1 to 0.3: **O** concedes that A is a **set** and that B(x) and C(x) are propositions provided x is an element of A.

* Move 0: **P** states that the main sentence, universally quantified, is a proposition (under the concessions made by **O**).

* Moves 1 and 2: the players choose their repetition ranks.

* Move 3: **O** challenges the thesis by asking the left-hand part as specified by the formation rule for universal quantification.

* Move 4: **P** responds by stating that A is a **set**. This has already been granted with the concession 0.1 so even if **O** were to challenge this statement the Proponent could refer to her initial concession.

This dialogue obviously does not cover all the aspects related to the formation of

$$ (\forall x : A) B(x) \supset C(x) : prop. $$

Notice however that the formation rules allow an alternative move for the Opponent's move 3,<fnref n="80" /> so that **P** has another possible course of action, dealt with in the following play.

<table><caption>Play 11: formation-play with initial concessions: second decision-option of O</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>A : set</td><td colspan="2"></td></tr><tr><td>0.2</td><td>B(x) : prop [x : A]</td><td colspan="2"></td></tr><tr><td>0.3</td><td>C(x) : prop [x : A]</td><td>(∀x : A) B(x) ⊃ C(x) : prop</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? F<sub>∀2</sub></td><td>B(x) ⊃ C(x) : prop [x : A]</td><td>4</td></tr><tr><td>5</td><td>x : A</td><td>B(x) ⊃ C(x) : prop</td><td>6</td></tr><tr><td>7</td><td>? F<sub>sup</sub></td><td>B(x) : prop</td><td>10</td></tr></tbody></table>

<footnote n="80">⁸⁰ As a matter of fact, increasing her repetition rank would allow **O** to play the two alternatives for move 3 within a single play. But increasing the Opponent's rank usually yields redundancies (Clerbout, 2014a; 2014b) making things harder to understand for readers not familiar with the dialogical approach; hence our choice to divide the example into different simple plays.</footnote>
<table><tr><td>9</td><td><i>B(x) : prop</i></td><td>0.2</td><td><i>x : A</i></td><td>8</td></tr></table>

P wins.

**Explanation:**

The second play starts like the first one until move 2. Then:

* Move 3: this time **O** challenges the thesis by asking for the right-hand part.

* Move 4: **P** responds, stating that $B(x) \supset C(x)$ is a proposition, provided that $x : A$.

* Move 5: **O** challenges the preceding move by granting the proviso and asking **P** to respond (this kind of move is governed by a Subst-D rule).

* Move 6: **P** responds by stating that $B(x) \supset C(x)$ is a proposition.

* Move 7: **O** challenges move 6 by asking the left-hand part, as specified by the formation rule for material implication.

To defend against this challenge, **P** needs to make an elementary move. But since **O** has not played it yet, **P** cannot defend it at this point. Thus:

* Move 8: **P** launches a counterattack against initial concession 0.2 by granting the proviso $x : A$ (that has already been conceded by **O** in move 5), making use of the same kind of statement-substitution (Subst-D) rule deployed in move 5.

* Move 9: **O** answers to move 8 and states that $B(x)$ is a proposition.

* Move 10: **P** can now defend the challenge initiated with move 7 and win this dialogue.

Once again, there is another possible choice for the Opponent because of her move 7: she could ask the right-hand part. This would yield a dialogue similar to the one above except that the last moves would be about $C(x)$ instead of $B(x)$.

**Concluding on the formation-play example:**

By displaying these various possibilities for the Opponent, we have entered the strategic level. This is the level at which the question of the good formation of the thesis gets a definitive answer, depending on whether the Proponent can always win—that is, whether he has a winning strategy. The basic notions related to this level of strategies are to be found in our presentation of standard dialogical logic (see section III.5 or chapter V.1); section VII.5 below will deal with local reasons in this strategy level in the framework of dialogues for immanent reasoning and section VII.7 will introduce strategic reasons.

### VII.1.2 The rules for local reasons: synthesis and analysis

Now that the dialogical account of formation rules has been clarified, we may further develop our analysis of plays by introducing local reasons. Let us do so by providing the rules that prescribe the synthesis and analysis of local reasons. For more details on each rule, see section VI.3.

<table><caption>Table 19: synthesis rules for local reasons</caption><tr><td>Move</td><td>Challenge</td><td>Defence</td></tr></table>
<table><caption>Table 20: analysis rules for local reasons</caption><tr><td>Conjunction</td><td>X! A ∧ B</td><td>Y?L<sup>^</sup><br>or<br>Y?R<sup>^</sup></td><td>Xp<sub>1</sub>: A<br>(resp.)<br>Xp<sub>2</sub>: B</td></tr><tr><td>Existential quantification</td><td>X!(∃x: A)B(x)</td><td>Y?L<sup>∃</sup><br>or<br>Y?R<sup>∃</sup></td><td>Xp<sub>1</sub>: A<br>(resp.)<br>Xp<sub>2</sub>: B(p<sub>1</sub>)</td></tr><tr><td>Subset separation</td><td>X!{x: A | B(x)}</td><td>Y?L<br>or<br>Y?R</td><td>Xp<sub>1</sub>: A<br>(resp.)<br>Xp<sub>2</sub>: B(p<sub>1</sub>)</td></tr><tr><td>Disjunction</td><td>X!A ∨ B</td><td>Y?<sup>ν</sup></td><td>Xp<sub>1</sub>: A<br>or<br>Xp<sub>2</sub>: B</td></tr><tr><td>Implication</td><td>X! A ⊃ B</td><td>Yp<sub>1</sub>: A</td><td>Xp<sub>2</sub>: B</td></tr><tr><td>Universal quantification</td><td>X!(∀x: A)B(x)</td><td>Yp<sub>1</sub>: A</td><td>Xp<sub>2</sub>: B(p<sub>1</sub>)</td></tr><tr><td>Negation</td><td>X! ¬A<br>Also expressed as<br>X! A ⊃ ⊥</td><td>Yp<sub>1</sub>: A</td><td>X! ⊥<br>(X gives up<sup>81</sup>)</td></tr></table>

<table><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><td>Conjunction</td><td>Xp: A ∧ B</td><td>Y?L<sup>^</sup><br>or<br>Y?R<sup>^</sup></td><td>X L<sup>^</sup>(p)<sup>X</sup>: A<br>(resp.)<br>X R<sup>^</sup>(p)<sup>X</sup>: B</td></tr><tr><td>Existential quantification</td><td>Xp: (∃x: A)B(x)</td><td>Y?L<sup>∃</sup><br>or<br>Y?R<sup>∃</sup></td><td>X L<sup>∃</sup>(p)<sup>X</sup>: A<br>(resp.)<br>X R<sup>∃</sup>(p)<sup>X</sup>: B(L<sup>∃</sup>(p)<sup>X</sup>)</td></tr><tr><td>Subset separation</td><td>Xp: {x: A | B(x)}</td><td>Y?L<br>or<br>Y?R</td><td>X L<sup>{...}</sup>(p)<sup>X</sup>: A<br>(resp.)<br>X R<sup>^</sup>(p)<sup>X</sup>: B(L<sup>{...}</sup>(p)<sup>X</sup>)</td></tr><tr><td>Disjunction</td><td>Xp: A ∨ B</td><td>Y?<sup>ν</sup></td><td>X L<sup>ν</sup>(p)<sup>X</sup>: A<br>or<br>X R<sup>ν</sup>(p)<sup>X</sup>: B</td></tr><tr><td>Implication</td><td>Xp: A ⊃ B</td><td>Y L<sup>∃</sup>(p)<sup>Y</sup>: A</td><td>X R<sup>∃</sup>(p)<sup>Y</sup>: B</td></tr><tr><td>Universal quantification</td><td>Xp: (∀x: A)B(x)</td><td>Y L<sup>ν</sup>(p)<sup>Y</sup>: A</td><td>X R<sup>ν</sup>(p)<sup>Y</sup>: B(L<sup>ν</sup>(p)<sup>Y</sup>)</td></tr><tr><td>Negation</td><td>Xp: ¬A<br>Also expressed as<br>Xp: A ⊃ ⊥</td><td>Y L<sup>¬</sup>(p)<sup>Y</sup>: A<br>Y L<sup>∃</sup>(p)<sup>Y</sup>: A</td><td>X R<sup>¬</sup>(p)<sup>Y</sup>: ⊥<br>X R<sup>∃</sup>(p)<sup>Y</sup>: ⊥</td></tr></tbody></table>

<footnote n="81">81 The reading of stating bottom as giving up stems from (Keiff, 2007).</footnote>
**Anaphoric instructions: dealing with cases of anaphora**

One of the most salient features of the CTT framework is that it contains the means to deal with cases of anaphora,<fnref n="82" /> and some of the demonstrations for the exercises of chapter II required them, as in exercise 4 formalizing Barbara in CTT (p. 44).

Recall the formalization of exercise 4, where the projection **fst**(z) can be seen as the tail of the anaphora whose head is z:

(∀z : (∃x : D)A)B[**fst**(z)] true premise 1

(∀z : (∃x : D)B)C[**fst**(z)] true premise 2

(∀z : (∃x : D)A)C[**fst**(z)] true conclusion

In dialogues for immanent reasoning, when a local reason has been made explicit, this kind of anaphoric expression is formalized through instructions, which provides a further reason for introducing them. For example if *a* is the local reason for the first premise we have

$$ \mathbf{P} p : (\forall z : (\exists x : D)A(x))B(L^{\exists}(L^{\forall}(p)^{\circ})) $$

However, since the thesis of a play does not bear an explicit local reason (we use the exclamation mark to indicate there is an implicit one), it is possible for a statement to be bereft of an explicit local reason. When there is no explicit local reason for a statement using anaphora, we cannot bind the instruction $L^{\forall}(p)^{\circ}$ to a local reason $p$. We thus have something like this, with a blank space instead of the anaphoric local reason:

$$ \mathbf{P} ! (\forall z : (\exists x : D)A(x))B(L^{\exists}(L^{\forall}()^{\circ})) $$

But this blank stage can be circumvented: the challenge on the universal quantifier will yield the required local reason: **O** will provide *a*: (∃x:D)A(x), which is the local reason for *z*. We can therefore bind the instruction on the missing local reason with the corresponding variable—*z* in this case—and write

$$ \mathbf{P} ! (\forall z : (\exists x : D)A(x))B(L^{\exists}(L^{\forall}(z)^{\circ})) $$

We call this kind of instruction, *Anaphoric instructions*. For the substitution of Anaphoric instructions the following two cases are to be distinguished:

**Substitution of Anaphoric Instructions 1**

Given some Anaphoric instruction such as $L^{\forall}(z)^{\circ}$, once the quantifier $(\forall z : A)B(...)$ has been challenged by the statement $a : A$, the occurrence of $L^{\forall}(z)^{\circ}$ can be substituted by *a*. The same applies to other instructions.

In our example we obtain:

$$ \mathbf{P} ! (\forall z : (\exists x : D)A(x))B(L^{\exists}(L^{\forall}(z)^{\circ})) $$

$$ \mathbf{O} a : (\exists x : D)A(x) $$

$$ \mathbf{P} b : B(L^{\exists}(L^{\forall}(z)^{\circ})) $$

$$ \mathbf{O} ? a / L^{\forall}(z)^{\circ} $$

$$ \mathbf{P} b : B(L^{\exists}(a)) $$

...

<footnote n="82">⁸² See (Sundholm, 1986, pp. 501-503) and (Ranta, 1994, pp. 77-99).</footnote>
## Substitution of Anaphoric Instructions 2

Given some Anaphoric instruction such as $L^{
abla}(z)^Y$, once the instruction $L^{
abla}(c)$— resulting from an attack on the universal $\forall z : \varphi$—has been resolved with $a : \varphi$, then any occurrence of $L^{
abla}(z)^Y$ can be substituted by $a$. The same applies to other instructions.

# VII.2 Global Meaning in dialogues for immanent reasoning

We here provide the structural rules for dialogues for immanent reasoning, which determine the global meaning in such a framework. They are for the most part similar in principle to the precedent logical framework for dialogues; the rules concerning instructions are an addition for dialogues for immanent reasoning.

The structural rules for formal dialogues (as opposed to material dialogues; see chapter X) are of three kinds: starting rules (SR0 and SR2i), the Socratic rules that are player dependent rules for elementary statements (SR5), and global rules that are player independent procedural rules (SR1, 2ii, 3-4 and 6-7).

## VII.2.1 Structural Rules

### SR0: Starting rule

The start of a *formal dialogue of immanent reasoning* is a move where **P** states the *thesis*. The thesis can be stated under the condition that **O** commits herself to certain other statements called *initial concessions*; in this case the thesis has the form ! *A* [*B*₁, ..., *B*ₙ], where *A* is a statement with implicit local reason and *B*₁, ..., *B*ₙ are statements with or without implicit local reasons.

A dialogue with a thesis proposed under some conditions starts if and only if **O** accepts these conditions. **O** accepts the conditions by stating the *initial concessions* in moves numbered 0.1, ..., 0.n before choosing the repetition ranks.

After having stated the thesis (and the initial concessions, if any), each player chooses in turn a positive integer called the *repetition rank* which determines the upper boundary for the number of attacks and of defences each player can make in reaction to each move during the play.

### SR1: Development rule

The Development rule depends on what kind of logic is chosen: if the game uses intuitionistic logic, then it is SR1i that should be used; but if classical logic is used, then SR1c must be used.

### SR1i: Intuitionistic Development rule, or Last Duty First

Players play one move alternately. Any move after the choice of repetition ranks is either an attack or a defence according to the rules of formation, of synthesis, and of analysis, and in accordance with the rest of the structural rules.

If the logical constant occurring in the thesis is not recorded by the table for local meaning, then either it must be introduced by a nominal definition, or the table for local meaning needs to be enriched with the new expression.<fnref n="83" />

Players can answer only against the *last non-answered* challenge by the adversary.

<footnote n="83">⁸³ If the logical constant occurring in the thesis is not recorded by the table for local meaning, then either it must be introduced by a nominal definition based on some logical constant already present in the particle rules, or the table for local meaning needs to be enriched with the new expression.</footnote>
*Note: This structural rule is known as the Last Duty First condition, and makes dialogical games suitable for intuitionistic logic, hence the name of this rule.*

**SR1c: Classical Development rule**

Players play one move alternately. Any move after the choice of repetition ranks is either an attack or a defence according to the rules of formation, of synthesis, and of analysis, and in accordance with the rest of the structural rules.

If the logical constant occurring in the thesis is not recorded by the table for local meaning, then either it must be introduced by a nominal definition, or the table for local meaning needs to be enriched with the new expression.

*Note: The structural rules with SR1c (and not SR1i) produce strategies for classical logic. The point is that since players can answer to a list of challenges in any order (which is not the case with the intuitionistic rule), it might happen that the two options of a P-defence occur in the same play—this is closely related to the classical development rule in sequent calculus allowing more than one formula at the right of the sequent.*

**SR2: Formation rules for formal dialogues**

**SR2i: Starting a formation dialogue**

A formation-play starts by challenging the thesis with the formation request **O** ?<sub>prop</sub>; **P** must answer by stating that his thesis is a proposition.

**SR2ii: Developing a formation dialogue**

The game then proceeds by applying the formation rules up to the elementary constituents of **prop/set**.

After that **O** is free to use the other particle rules insofar as the other structural rules allow it.

*Note: The constituents of the thesis will therefore not be specified before the play but as a result of the structure of the moves (according to the rules recorded by the rules for local meaning).*

**SR3: Resolution of instructions**

1. A player may ask his adversary to carry out the prescribed instruction and thus bring forward a suitable local reason in defence of the proposition at stake. Once the defender has replaced the instruction with the required local reason we say that the instruction has been resolved.

2. The player index of an instruction determines which of the two players has the right to choose the local reason that will resolve the instruction.

a. If the instruction $\mathcal{S}$ for the logical constant $\mathcal{K}$ has the form $\mathcal{S}^{\mathcal{K}}(p)^{\mathcal{X}}$ and it is **Y** who requests the resolution, then the request has the form $\mathcal{Y} ? \dots / \mathcal{S}^{\mathcal{K}}(p)^{\mathcal{X}}$, and it is **X** who chooses the local reason.

b. If the instruction $\mathcal{S}$ for the logic constant $\mathcal{K}$ has the form $\mathcal{S}^{\mathcal{K}}(p)^{\mathcal{Y}}$ and it is player **Y** who requests the resolution, then the request has the form $\mathcal{Y} p_i / \mathcal{S}^{\mathcal{K}}(p)^{\mathcal{Y}}$, and it is **Y** who chooses the local reason.

3. In the case of a sequence of instructions of the form $\pi[\mathcal{S}_i(...(\mathcal{S}_k(p))...)]$, the instructions are resolved from the inside $(\mathcal{S}_k(p))$ to the outside $(\mathcal{S}_i)$. This rule also applies to functions.
### SR4: Substitution of instructions

Once the local reason *b* has been used to resolve the instruction $G^k(p)^X$, and if the same instruction occurs again, players have the right to require that the instruction be resolved with *b*. The substitution request has the form $?b/G_k(p)^X$. Players cannot choose a different substitution term (in our example, not even $X$, once the instruction has been resolved).

This rule also applies to functions.

### SR5: Socratic rule and definitional equality

The following points are all parts of the Socratic rule, they all apply.

#### SR5.1: Restriction of P statements

P cannot make an elementary statement if O has not stated it before<fnref n="84" />, except in the thesis.

An elementary statement is either an elementary proposition with implicit local reason, or an elementary proposition and its local reason (not an instruction).

#### SR5.2: Challenging elementary statements in formal dialogues

Challenges of elementary statements with implicit local reasons take the form:

$X!A$

$Y?_{reason}$

$Xa:A$

Where *A* is an elementary proposition and *a* is a local reason.<fnref n="85" />

P cannot challenge O's elementary statements, except if O provides an elementary initial concession with implicit local reason, in which case P can ask for a local reason, or in the context of transmission of equality.

#### SR5.3: Definitional equality

O may challenge elementary P-statements; P then answers by stating a definitional equality expressing the equality between a local reason and an instruction both introduced by O (for non-reflexive cases, that is when O provided the local reason as a resolution of an instruction), or a reflexive equality of the local reason introduced by O (when the local reason was not introduced by the resolution of an instruction, that is either as such in the initial concessions or as the result of a synthesis of a local reason). We thus distinguish two cases of the Socratic rule:

1. non-reflexive cases;<fnref n="86" />

2. reflexive cases.<fnref n="87" />

These rules do not cover cases of transmission of equality. The Socratic rule also applies to the resolution or substitution of functions, even if the formulation mentions only instructions.

<footnote n="84">⁸⁴ This yields an asymmetry in the structural rules. For a discussion on the consequences of this feature and how it is closely linked to the symmetry of the particle rules, see section IV.3, p. 67, and section XI.3.</footnote>

<footnote n="85">⁸⁵ Note that P is allowed to make an elementary statement only as a thesis (Socratic rule); he will be able to respond to the challenge on an elementary statement only if O has provided the required local reason in her initial concessions.</footnote>

<footnote n="86">⁸⁶ See below, section VII.3, for an illustration.</footnote>

<footnote n="87">⁸⁷ See for instance $P_1$ in VII.6.10 for an illustration.</footnote>
### SR5.3.1: Non-reflexive cases of the Socratic rule

We are in the presence of a *non-reflexive case* of the Socratic rule when **P** responds to the challenge with the indication that **O** gave the same local reason for the same proposition when she had to resolve or substitute instruction $\mathcal{S}$.

Here are the different challenges and defences determining the meaning of the three following moves:

<table><caption>Table 21: Non-reflexive cases of the Socratic rule</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><td>SR5.3.1a</td><td><b>P</b> a : A</td><td><b>O</b> ? = a</td><td><b>P</b> <i>S</i> = a : A</td></tr><tr><td>SR5.3.1b</td><td><b>P</b> a : A(b)</td><td><b>O</b> ? = b<sup>A(b)</sup></td><td><b>P</b> <i>S</i> = b : D</td></tr><tr><td>SR5.3.1c</td><td><b>P</b> <i>S</i> = b : D<br>(this statement stems from SR5.3.1b)</td><td><b>O</b> ? = A(b)</td><td><b>P</b> A(<i>S</i>) = A(b) : prop</td></tr></tbody></table>

**Presuppositions:**

(i) The response prescribed by SR5.3.1a presupposes that **O** has stated **A** or $a = b : A$ as the result of the resolution or substitution of instruction $\mathcal{S}$ occurring in $\mathcal{S} : A$ or in $\mathcal{S} = b : A$.

(ii) The response prescribed by SR5.3.1b presupposes that **O** has stated **A** and $b : D$ as the result of the resolution or substitution of instruction $\mathcal{S}$ occurring in $a : A(\mathcal{S})$.

(iii) SR5.3.1c assumes that $\mathbf{P} \mathcal{S} = b : D$ is the result of the application of SR5.3.1b. The further challenge seeks to verify that the replacement of the instruction produces an equality in **prop**, that is, that the replacement of the instruction with a local reason yields an equal proposition to the one in which the instruction was not yet replaced. The answer prescribed by this rule presupposes that **O** has already stated $A(b) : prop$ (or more trivially $A(\mathcal{S}) = A(b) : prop$).

The **P**-statements obtained after defending elementary **P**-statements cannot be attacked again with the Socratic rule (with the exception of SR5.3.1c), nor with a rule of resolution or substitution of instructions.

### SR5.3.2: Reflexive cases of the Socratic rule

We are in the presence of a *reflexive case* of the Socratic rule when **P** responds to the challenge with the indication that **O** adduced the same local reason for the same proposition, though that local reason in the statement of **O** is not the result of any resolution or substitution.

The attacks have the same form as those prescribed by SR5.3.1 (see Table 21). Responses that yield *reflexivity* presuppose that **O** has previously stated the same statement or even the same equality.

The response obtained cannot be attacked again with the Socratic rule.

### SR6: Transmission of definitional equality

Transmission of definitional equality I: Substitution within dependent or independent statements. The expression “type” refers to either **prop** or **set**. For more explanations on this structural rule, see below, section VII.2.2.
<table><caption>Table 22: Transmission of definitional equality I: Substitution within dependent or independent statements</caption><thead><tr><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><td>X b(x) : B(x) [x : A]</td><td>Y a = c : A</td><td>X b(a) = b(c) : B(a)</td></tr><tr><td>X b(x) = d(x) : B(x) [x : A]</td><td>Y a : A</td><td>X b(a) = d(a) : B(a)</td></tr><tr><td>X B(x) : type [x : A]</td><td>Y a = c : A</td><td>X B(a) = B(c) : type</td></tr><tr><td>X B(x) = D(x) : type [x : A]</td><td>Y ?<sub>B(x)=D(x)</sub> a : A<br>or<br>Y ?<sub>B(x)=D(x)</sub> a = c : A</td><td>X B(a) = D(a) : type<br>or<br>X B(a) = D(c) : type</td></tr><tr><td>X A = B : type</td><td>Y ?<sub>A=D</sub> a : A<br>or<br>Y ?<sub>A=D</sub> a = c : A</td><td>X a : B<br>or<br>X a = c : B</td></tr></tbody></table>

<table><caption>Table 23: Transmission of definitional equality II</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Type-reflexivity</th><td>X A : type</td><td>Y ?<sub>type</sub>- refl</td><td>X A = A : type</td></tr><tr><th>Type-symmetry</th><td>X A = B : type</td><td>Y ?<sub>B-symm</sub></td><td>X B = A : type</td></tr><tr><th>Type-transitivity</th><td>X A = B : type<br>X B = C : type</td><td>Y ?<sub>A-trans</sub></td><td>X A = C : type</td></tr><tr><th>Reflexivity</th><td>X a : A</td><td>Y ?<sub>a-refl</sub></td><td>X a = a : A</td></tr><tr><th>Symmetry</th><td>X a = b : A</td><td>Y ?<sub>b-symm</sub></td><td>X b = a : A</td></tr><tr><th>Transitivity</th><td>X a = b : A<br>X b = c : A</td><td>Y ?<sub>a-trans</sub></td><td>X a = c : A</td></tr></tbody></table>

### SR7: Winning rule for plays

The player who makes the last move wins. If the last O-move in the play is ⊥ then P can bring forward the local reason *you*<sub>*gave up*</sub>(*n*) in support for any statement that he has not defended before O stated ⊥ at move *n* (even if that statement is ⊥, see for instance VII.6.2 for an illustration).

## VII.2.2 Rules for the transmission of definitional equality

As can be expected, definitional equality is transmitted by *reflexivity*, *symmetry*<sup>88</sup>, and *transitivity*. Definitional equalities however can also be used in order to carry out a substitution within dependent statements—they can in fact be seen as a special form of application of the substitution rule for dependent statement Subst-D presented in the first section for local meaning, with the formation rules (VII.1.1, p. 106). We use the expression "type" as encompassing **prop** and **set**.

<footnote n="88"><sup>88</sup> Symmetry used here is not the same notion as the symmetry of section IV.3.</footnote>
**Reading adjuvant for the fourth rule (dependent statements) in Table 22:**

If $X$ stated that $B(x)$ and $D(x)$ are equal propositional functions, provided that $x$ is an element of the set $A$—that is, $X B(x)=D(x) : \mathbf{prop} [x : A]$, then $Y$ can carry out two kinds of attacks:

1. Stating himself that some local reason, say $a$, can be adduced for $A—Y a: A—$, and request at the same time of $X$ that he replaces $x$ with $a$ in $B(x)=D(x)$, that is stating $B(a)=D(a) : \mathbf{prop}$.

2. Stating himself an equality such as $a = c: A$, and request at the same time $X$ to carry out the corresponding substitutions in $B(x)=D(x)$, that is to state $X B(a)=D(c) : \mathbf{prop}$.

**Reading adjuvant for Table 23:**

In order to trigger reflexivity, transitivity, and symmetry from some equality statements the challenger can attack an equality by asking for each of these properties. For example, if $X$ stated $A = B : \mathbf{prop/set}$, $Y$ can ask $X$ to state the commutated equality $B = A : \mathbf{prop/set}$ by calling on symmetry. The notation of such an attack is as follows: $Y ?_{B-symm}$. Similarly, $Y ?_{A-refl}$ and $Y ?_{A-trans}$ respectively request reflexivity and transitivity.

**VII.3 Example: $(\forall x: D)(Q(x) \supset Q(x))$**

<table><thead><tr><th></th><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td rowspan="2">synthesis of local reason</td><td>1</td><td>$m := 1$</td><td>!($\forall x: D$)($Q(x) \supset Q(x)$)</td><td>0</td></tr><tr><td>3</td><td>$d_1: D$</td><td>$n := 2$</td><td>2</td></tr><tr><td rowspan="3">Analysis of local reason</td><td>5</td><td>$L^2(d_2): Q(d_1)$</td><td>$d_2: Q(d_1) \supset Q(d_1)$</td><td>4</td></tr><tr><td>7</td><td>$d_{2,1}: Q(d_1)$</td><td>$R^2(d_2): Q(d_1)$</td><td>8</td></tr><tr><td>9</td><td>? .../R<sup>2</sup>(d<sub>2</sub>)</td><td>? .../L<sup>2</sup>(d<sub>2</sub>)</td><td>6</td></tr><tr><td rowspan="2">SR5.3</td><td>11</td><td>? = $d_{2,1}$</td><td>$d_{2,1}: Q(d_1)$</td><td>10</td></tr><tr><td></td><td></td><td>$L^2(d_2) = d_{2,1}: Q(d_1)$</td><td>12</td></tr></tbody><tfoot><tr><td colspan="5" style="text-align: center;">P wins</td></tr></tfoot></table>

**VII.4 Solved exercises for the play level in dialogues for immanent reasoning**

Build a play for the following theses in dialogues for immanent reasoning.

1. $B \lor A$ [c: $A \lor B$]

That is, build a play for $B \lor A$ with the initial concession $c: A \lor B$.

2. $((A \lor (A \supset \top)) \supset \top) \supset \top$

Alternative notation: $\neg(\neg(A \lor \neg A))$; for a play of this game in the standard framework, see section IV.5. For all the plays in immanent reasoning, see section VII.6.

3. $(A \land (A \supset \top)) \supset \top$

Alternative notation: $\neg(A \land \neg A)$; for all the plays, see section VII.6.

4. $((A \supset B) \supset A) \supset A$

5. $(A \land (B \supset \top)) \supset ((A \supset B) \supset \top)$
6. $(A \land B) \land C [c: A \land (B \land C)]$

7. $(B \land A) \supset C [c: (A \land B) \supset C]$

As for the other cases, section VII.6 provides all the plays through the heuristical procedure for building a winning strategy; but the theses 5 and 6 will also have their strategic reason built in section VII.7.4, with an exposition of the tree-shaped core and the core turned into a natural deduction style demonstration in section IX.5.

8. $(\forall x: D)A(x) \supset \bot [(\exists x: D)(A(x) \supset \bot)]$

9. $(\exists x: D)A(x) \land (\exists x: D)B(x) [(\exists x: D)(A(x) \land B(x))]$

10. $(\exists x: D)(\exists y: D)(A(x) \supset B(y)) [A(a) \supset B(b); a: D; b: D]$

11. $(\exists x: D)B(x) \land (\exists x: D)P(x) [B(a) \land P(b); a: D; b: D]$

12. $(\exists x: D)(\exists y: D)A(x, y)[(\exists x: D)A(x, x)]$

13. $(\forall x: D)(\forall y: D)(A(x, y) \land A(y, x))[(\forall x: D)(\forall y: D)A(x, y)]$

14. $(\exists x: D)(A(x) \supset (\forall x: D)A(x)) [((\exists x: D)(A(x) \supset \bot)) \lor ((\forall x: D)(A(x)); a: D)]$

The graphic (tree) presentation of the strategy is also provided for this thesis.

In general, the solutions will be found in section (VII.6) which provides the **P**-winning strategies through the heuristical procedure, thus providing all the relevant plays for each thesis.

## VII.5 The strategy level in dialogues for immanent reasoning

The strategy level in dialogues for immanent reasoning is analogous to that of the standard framework: the core of a **P**-strategy can be built by means of the heuristical procedure which allows to find *all* of the *relevant* plays for a given thesis. However, since the local and structural rules have been modified in the framework for dialogues for immanent reasoning in order to incorporate features of CTT, the plays from which the strategy emerges will be modified in consequence. The procedure and the assumptions are thus the same as in chapter V—to which we refer the reader—but the result of their application will differ, especially because of local reasons and instructions, absent of the standard dialogical framework. A few remarks are due before proceeding to the exercises.

**Adding to the assumptions on O's move preferences:**

1. When **O** has to choose a local reason she will always choose a new one.<fnref n="89" />

2. **O** will challenge instructions (if there are any) before carrying out other moves.<fnref n="90" />

A direct consequence of this—added to the assumption that **O** will always challenge first, if she can (see p. 77)—is that in the case that **P** challenges a material implication or a universal, **O** will first counterattack the instructions $L^\neg$ or $L^\vee$ before responding to the challenge.

<footnote n="89">⁸⁹ This assumption is analogous to the assumption in section V.2 that **O** chooses a new constant when she can. The reason is the same: it is the best possible choice for **O**. Indeed, here also **P** is restricted by the Socratic rule, so he needs to rely on **O**'s choices in order to copy a move. In such a context, the only way to (try to) block the use of this kind of equality is to always choose, whenever possible, a new local reason.</footnote>

<footnote n="90">⁹⁰ The reason is similar to the previous one: it is better for **O** to force **P** to makes his choice as soon as possible.</footnote>
### Recalling the O-decisions:

<table><tr><td colspan="2">O has a choice and takes a decision when</td></tr><tr><td>O challenges a...</td><td>O defends a...</td></tr><tr><td>Conjunction<br/>Existential</td><td>Disjunction<br/>Implication</td></tr></table>

### Recalling left and right decisions:

We speak of a *left-decision* when:

* O defends the left side of a disjunction;

* O challenges the left side of a conjunction or existential;

* O counterattacks instead of defending an implication.

We speak of a *right decision* when:

* O defends the right side of a disjunction;

* O challenges the right side of a conjunction or existential;

* O defends an implication.

### Getting rid of infinite ramifications in a strategy:

When the Opponent has to choose a local reason for a previously unresolved instruction, it will be a member of some set which, unless otherwise specified, may be infinite. The Opponent can then choose among an infinite number of members when asked to replace the instruction with a local reason,<fnref n="91" /> though once she has chosen one she must keep it for the rest of the play (recall the statement-substitution rule).

Repetition ranks ensure that plays are finite (they fix an upper boundary to the number of challenges and defences each player can play in reaction to a move). But strategies take all the possible plays for a thesis into account, which easily yields infinite strategies. These are reduced down to a finite length (the core) by disregarding redundant variants.

### Local reasons and proof-objects:

Local reasons are not the dialogical counterparts of CTT proof-objects—strategic reasons are, which will be presented in section VII.7—, and thus are not enough to establish the connection between the dialogical and the CTT approaches.

The connection between our dialogical games and CTT is not to be found at the level of plays, but at the level of strategies where the CTT notion of proof and the dialogical notion of P-winning strategies come together. More precisely, demonstrations in Natural deduction in general, and in CTT in particular, correspond within the dialogical framework to P-winning strategies (see chapter IX for how this correspondence is built).

<footnote n="91">⁹¹ See (Clerbout, 2014a; 2014c): if there is a move by which the Opponent can force her victory, then nothing prevents her from playing it as soon as she has a chance to. Whether this move is a challenge or a defence, the repetition rank 1 is enough to allow her to play it in accordance with SR1i.</footnote>
## Disregarding formation rules for formal plays

The dialogical rules allow the players to enquire about the type of expressions used in a dialogue; in particular they allow to ask whether an expression is a proposition or not. This leads to plays that use formation rules (see VII.1.1).

The scope of the present study only covers the fragment of CTT involving logically valid propositions and formal plays (see chapter IX); so generally in the formal enquiries which we are dealing with here, we presuppose that the logical structure of the expressions whose validity must be demonstrated have been well typed. We will therefore set aside the formation rules in considering the strategic level for formal plays.

## Disregarding irrelevant variations in the order of O-moves.

A P-strategy must account for every possible way for O to play, and in particular it must deal with any order in which O might play her moves. Since we look for a winning P-strategy, we can select any particular order of O-moves without losing anything in terms of P's victory: the very definition of a winning strategy states that P must win in every play proceeding from an O-choice, so the order of O-moves does not influence the result.

Special care must nevertheless be taken, especially in an intuitionistic framework (because of the restrictions of SR1i ('last duty first'), O can only answer to P's last non-answered challenge): we do not want a play in which O loses because she played poorly. Since the extensive form of the strategy will contain all of the possible plays—the ones in which O played well and those in which she did not—, if we select some plays and discard the others we should take care not to retain one of those plays in which O did not play well. When extracting a particular order of O's moves in all the possible order of moves, we shall select a play such that every P-challenge is immediately followed by the O-defence, for it tends to be strategically safer for O to defend immediately (and be sure not to lose the chance of making that move later on) and delay possible moves involving counterattacks. By doing so we explicitly get rid of the cases in which O loses only because she poorly chose the order of her moves.

Once we have removed all the redundant information for developing a demonstration, what remains is the core C of the strategy.

**Example: obtaining the core for ($\forall x: D) Q(x) \supset Q(x)$**

From the play in section VII.3, one can build a graphic (tree) presentation of the core, provided infinite ramifications are reduced to a finite number, which can be carried out in two steps: getting rid of ramifications first from repetition ranks, then from choice of names.

### Step 1: getting rid of ramifications from repetition ranks

Here we present the core of the strategy where we delete all the branches where O chooses a repetition rank bigger than 1

<figure><img src="image_19.png" /></figure>
4. **P** *d*₂: *Q(p*₁) ⊃ *Q(p*₁)*[!, 3]

5. **O** L$^{ hood}$(d₂): Q(d₁)[?, 4]

6. **P** ? ... /L$^{hood}$(d₂) [?, 5]

4. **P** *d*₂: *Q(p*₁) ⊃ *Q(p*₁)*[!, 3]

5. **O** L$^{hood}$(d₂): Q(d₁)[?, 4]

6. ...

4. ...

<figure><img src="image_20.png" /></figure>

**Step 2: getting rid of choices of names**

Delete all but one of the branches of the previous tree triggered by **O**'s choices of a
local reason.

<figure><img src="image_21.png" /></figure>

Litterature on the link between CTT and the dialogical
framework:

Nicolas Clerbout (2014a; 2014b; 2014c) showed how to extract winning strategies for **P** out of the extensive form of strategies, and he developed the corresponding proof. Clerbout & Rahman (2015) extended the result to the CTT-demonstrations.

For other publications on the development of such algorithms see (Felscher, 1985), (Keiff, 2007), (Rahman & Tulenheimo, 2009), (Rahman, Clerbout, & Keiff, 2009) and (Cardascia, 2016). Laurent Keiff (2007) was the first to have developped this kind of method for standard dialogical logic.
## VII.6 Exercises and solutions<fnref n="92" />

Build a demonstration for the theses provided in section VII.4 using the heuristic procedure.

Provide also the graphic (tree) presentation for the theses marked with an asterisk *.

### Solutions

The exercises have been developed considering the following elements:

* the assumptions for the procedure of building a winning strategy (see sections V.2.1 and VII.5). We thus assume that O's repetition rank is 1.

* As much as possible, local reasons will follow the notation $d_1, d_{1,2}$, etc., in order to keep track of the complex local reason from which they originate.

For example $d_1$ indicates that the local reason is the first component of the complex local reason d. We will use this notation as long as it does not hinder the choices of the players.

* In order to shorten the length of the plays we will not deploy challenges of the form $? ... = A(b): type$.

* In order to implement more clearly the Intuitionistic Development rule SR1i (section VII.2.1) we present the negation in its implication form—instead of writing $p : \neg A$ we write $p: A \supset \bot$.

### VII.6.1 $B \lor A [c: A \lor B]$

<table><thead><tr><th></th><th>O</th><th></th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>P<sub>1</sub></td><td>0.1</td><td>c: A ∨ B</td><td></td><td>! B ∨ A [c: A ∨ B]</td><td>0</td></tr><tr><td></td><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td></td><td>3</td><td>?V</td><td>0</td><td>c<sub>1</sub>: A</td><td>8</td></tr><tr><td></td><td>5</td><td>L<sup>V</sup>(c): A [δ<sub>1</sub>, ...]</td><td></td><td>?V</td><td>4</td></tr><tr><td></td><td>7</td><td>c<sub>1</sub>: A</td><td></td><td>? .../L<sup>V</sup>(c)</td><td>6</td></tr><tr><td></td><td>9</td><td>? = c<sub>1</sub></td><td>8</td><td>L<sup>V</sup>(c) = c<sub>1</sub>: A</td><td>10</td></tr></tbody></table>

P wins

<table><thead><tr><th></th><th>O</th><th></th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>P<sub>2</sub></td><td>0.1</td><td>c: A ∨ B</td><td></td><td>! B ∨ A [c: A ∨ B]</td><td>0</td></tr><tr><td></td><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td></td><td>3</td><td>?V</td><td>0</td><td>c<sub>2</sub>: B</td><td>8</td></tr><tr><td></td><td>5</td><td>R<sup>V</sup>(c): A [δ<sub>1</sub>, δ<sub>2</sub>]</td><td></td><td>?V</td><td>4</td></tr><tr><td></td><td>7</td><td>c<sub>2</sub>: B</td><td></td><td>? .../R<sup>V</sup>(c)</td><td>6</td></tr><tr><td></td><td>9</td><td>? = c<sub>2</sub></td><td>8</td><td>R<sup>V</sup>(c) = c<sub>2</sub>: B</td><td></td></tr></tbody></table>

P wins

### VII.6.2 $((A \lor (A \supset \bot)) \supset \bot) \supset \bot$

<table><thead><tr><th></th><th>O</th><th></th><th>P</th></tr></thead></table>

<footnote n="92">⁹² This section has been developed by Stephen Eckoubili.</footnote>
<table><tr><td></td><td></td><td></td><td>!((A ∨ (A ⊃ ⊥)) ⊃ ⊥) ⊃ ⊥</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: (A ∨ (A ⊃ ⊥)) ⊃ ⊥</td><td>0</td><td>you<sub>gave up</sub>(7 [P<sub>1R</sub>]): ⊥</td><td>8 [P<sub>1R</sub>]</td></tr><tr><td></td><td>...</td><td></td><td>L<sup>⊤</sup>(d<sub>1</sub>): A ∨ (A ⊃ ⊥)</td><td>4</td></tr><tr><td>5</td><td>? .../L<sup>⊤</sup>(d<sub>1</sub>)</td><td>4</td><td>d<sub>1,1</sub>: A ∨ (A ⊃ ⊥)</td><td>6</td></tr></table>

<table><tr><td>P<sub>1L</sub></td><td>7</td><td>?<sup>ν</sup></td><td>6</td><td>R<sup>ν</sup>(d<sub>1,1</sub>): A ⊃ ⊥</td><td>8</td></tr><tr><td></td><td>9</td><td>? .../R<sup>ν</sup>(d<sub>1,1</sub>)</td><td>8</td><td>d<sub>1,1,2</sub>: A ⊃ ⊥</td><td>10</td></tr><tr><td></td><td>11</td><td>L<sup>⊤</sup>(d<sub>1,1,2</sub>): A</td><td>10</td><td></td><td></td></tr><tr><td></td><td>13</td><td>d<sub>1,1,2,1</sub>: A</td><td></td><td>11</td><td>? ... /L<sup>⊤</sup>(d<sub>1,1,2</sub>)</td><td>12</td></tr><tr><td></td><td>[7]</td><td>[?<sup>ν</sup>]</td><td>[6]</td><td>L<sup>ν</sup>(d<sub>1,1</sub>): A</td><td>14</td></tr><tr><td></td><td>15</td><td>? .../L<sup>ν</sup>(d<sub>1,1</sub>)</td><td>14</td><td>d<sub>1,1,2,1</sub>: A</td><td>16</td></tr><tr><td></td><td>17</td><td>? = d<sub>1,1,2,1</sub></td><td>16</td><td>L<sup>⊤</sup>(d<sub>1,1,2</sub>) = d<sub>1,1,2,1</sub>: A</td><td>18</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>7</td><td>R<sup>⊤</sup>(d<sub>1</sub>): ⊥</td><td></td><td>...</td><td></td></tr></table>

P wins

VII.6.3 $((A \wedge (A \supset \bot)) \supset \bot)$

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!((A ∧ (A ⊃ ⊥)) ⊃ ⊥)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: A ∧ (A ⊃ ⊥)</td><td>0</td><td>you<sub>gave up</sub>(15 [P<sub>1R</sub>]): ⊥</td><td>16 [P<sub>1R</sub>]</td></tr><tr><td>5</td><td>L<sup>∧</sup>(d<sub>1</sub>): A</td><td></td><td>3</td><td>? L<sup>∧</sup></td><td>4</td></tr><tr><td>7</td><td>d<sub>1,1</sub>: A</td><td></td><td>5</td><td>? .../L<sup>∧</sup>(d<sub>1</sub>)</td><td>6</td></tr><tr><td>9</td><td>R<sup>∧</sup>(d<sub>1</sub>): A ⊃ ⊥</td><td></td><td>3</td><td>? R<sup>∧</sup></td><td>8</td></tr><tr><td>11</td><td>d<sub>1,2</sub>: A ⊃ ⊥</td><td></td><td>7</td><td>? .../R<sup>∧</sup>(d<sub>1</sub>)</td><td>10</td></tr><tr><td></td><td>...</td><td></td><td>11</td><td>L<sup>⊤</sup>(d<sub>1,2</sub>): A</td><td>12</td></tr><tr><td>13</td><td>? .../L<sup>⊤</sup>(d<sub>1,2</sub>)</td><td>12</td><td></td><td>d<sub>1,1</sub>: A</td><td>14</td></tr></tbody></table>

<table><tr><td>P<sub>1L</sub></td><td>15</td><td>? = d<sub>1,1</sub></td><td>14</td><td>L<sup>∧</sup>(d<sub>1</sub>) = d<sub>1,1</sub>: A</td><td>16</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>15</td><td>R<sup>⊤</sup>(d<sub>1,2</sub>): ⊥</td><td></td><td>...</td><td></td></tr></table>

P wins

VII.6.4 $((A \supset B) \supset A) \supset A$

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!((A ⊃ B) ⊃ A) ⊃ A</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: (A ⊃ B) ⊃ A</td><td>0</td><td>d<sub>1,1,1</sub>: A</td><td>10 [P<sub>1L</sub>]</td></tr><tr><td></td><td></td><td></td><td>d<sub>1,2</sub>: A</td><td>10 [P<sub>1R</sub>]</td></tr></tbody></table>
<table><tr><td></td><td>...</td><td></td><td>L<sup>2</sup>(d<sub>1</sub>): A ⊃ B</td><td>4</td></tr><tr><td>5</td><td>? .../L<sup>2</sup>(d<sub>1</sub>)</td><td>4</td><td>d<sub>1,1</sub>: A ⊃ B</td><td>6</td></tr></table>

<table><tr><td>P<sub>1L</sub></td><td>7</td><td>L<sup>2</sup>(d<sub>1,1</sub>): A</td><td>6</td><td></td><td></td></tr><tr><td></td><td>9</td><td>d<sub>1,1,1</sub>: A</td><td></td><td>7</td><td>? .../L<sup>2</sup>(d<sub>1,1</sub>)</td><td>8</td></tr><tr><td></td><td>11</td><td>? = d<sub>1,1,1</sub></td><td>10</td><td></td><td>L<sup>2</sup>(d<sub>1,1</sub>) = d<sub>1,1,1</sub>: A</td><td>12</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>7</td><td>R<sup>2</sup>(d<sub>1</sub>): A</td><td></td><td></td><td>...</td><td></td></tr><tr><td></td><td>9</td><td>d<sub>1,2</sub>: A</td><td></td><td>7</td><td>? .../R<sup>2</sup>(d<sub>1</sub>)</td><td>8</td></tr><tr><td></td><td>11</td><td>? = d<sub>1,2</sub></td><td>10</td><td></td><td>R<sup>2</sup>(d<sub>1</sub>) = d<sub>1,2</sub>: A</td><td>12</td></tr></table>

P wins

### VII.6.5 $(A \wedge (B \supset \bot)) \supset ((A \supset B) \supset \bot)$

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>m := 1</td><td></td><td>!(A ∧ (B ⊃ ⊤)) ⊃ ((A ⊃ B) ⊃ ⊤)</td><td>0</td></tr><tr><td>3</td><td>d<sub>1</sub>: A ∧ (B ⊃ ⊤)</td><td>0</td><td>n := 2</td><td>2</td></tr><tr><td>5</td><td>L<sup>2</sup>(d<sub>2</sub>): A ⊃ B</td><td>4</td><td>d<sub>2</sub>: (A ⊃ B) ⊃ ⊤</td><td>4</td></tr><tr><td>7</td><td>d<sub>2,1</sub>: A ⊃ B</td><td></td><td>you<sub>gave up</sub>(21 [P<sub>1RR</sub>]): ⊤</td><td>22 [P<sub>1RR</sub>]</td></tr><tr><td>9</td><td>L<sup>1</sup>(d<sub>1</sub>): A</td><td></td><td>? .../L<sup>2</sup>(d<sub>2</sub>)</td><td>6</td></tr><tr><td>11</td><td>d<sub>1,1</sub>: A</td><td></td><td>? L<sup>1</sup></td><td>8</td></tr><tr><td>13</td><td>R<sup>1</sup>(d<sub>1</sub>): B ⊃ ⊤</td><td></td><td>? .../L<sup>1</sup>(d<sub>1</sub>)</td><td>10</td></tr><tr><td>15</td><td>d<sub>1,2</sub>: B ⊃ ⊤</td><td></td><td>? R<sup>1</sup></td><td>12</td></tr><tr><td></td><td>...</td><td></td><td>? .../R<sup>1</sup>(d<sub>1</sub>)</td><td>14</td></tr><tr><td></td><td>...</td><td></td><td>d<sub>1,1</sub>: A</td><td>16</td></tr></tbody></table>

<table><tr><td>P<sub>1L</sub></td><td>17</td><td>? = d<sub>1,1</sub></td><td>16</td><td></td><td>L<sup>1</sup>(d<sub>1</sub>) = d<sub>1,1</sub>: A</td><td>18</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>17</td><td>R<sup>2</sup>(d<sub>2,1</sub>): B</td><td></td><td></td><td>...</td><td></td></tr><tr><td></td><td>19</td><td>d<sub>2,1,2</sub>: B</td><td></td><td>17</td><td>? .../R<sup>2</sup>(d<sub>2,1</sub>)</td><td>18</td></tr><tr><td></td><td></td><td>...</td><td></td><td>15</td><td>d<sub>2,1,2</sub>: B</td><td>20</td></tr></table>

<table><tr><td>P<sub>1RL</sub></td><td>21</td><td>? = d<sub>2,1,2</sub></td><td>20</td><td></td><td>R<sup>2</sup>(d<sub>2,1</sub>) = d<sub>2,1,2</sub>: B</td><td>22</td></tr></table>

P wins

<table><tr><td>P<sub>1RR</sub></td><td>21</td><td>R<sup>2</sup>(d<sub>1,2</sub>): ⊤</td><td></td><td></td><td>...</td><td></td></tr></table>

P wins

### VII.6.6 $(A \wedge B) \wedge C [c: A \wedge (B \wedge C)]$

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>c: A ∧ (B ∧ C)</td><td></td><td>!(A ∧ B) ∧ C [c: A ∧ (B ∧ C)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr></tbody></table>
<table><tr><td>3</td><td>? L<sup>^</sup></td><td>0</td><td></td><td>d<sub>1</sub>: A ^ B</td><td>4</td></tr><tr><td>5</td><td>? L<sup>^</sup> [δ<sub>1</sub>, ...]</td><td>4</td><td></td><td>L<sup>^</sup>(d<sub>1</sub>): A</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>^</sup>(d<sub>1</sub>)</td><td></td><td></td><td>c<sub>1</sub>: A</td><td>12</td></tr><tr><td>9</td><td>L<sup>^</sup>(c): A</td><td></td><td>0.1</td><td>? L<sup>^</sup></td><td>8</td></tr><tr><td>11</td><td>c<sub>1</sub>: A</td><td></td><td>9</td><td>? .../L<sup>^</sup>(c)</td><td>10</td></tr><tr><td>13</td><td>? = c<sub>1</sub></td><td>12</td><td></td><td>L<sup>^</sup>(c) = c<sub>1</sub>: A</td><td>14</td></tr></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>c: A ^ (B ^ C)</td><td>! (A ^ B) ^ C [c: A ^ (B ^ C)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>^</sup> [δ<sub>2</sub>, ...]</td><td>d<sub>1</sub>: A ^ B</td><td>4</td></tr><tr><td>5</td><td>? R<sup>^</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>R<sup>^</sup>(d<sub>1</sub>): B</td><td>6</td></tr><tr><td>7</td><td>? .../R<sup>^</sup>(d<sub>1</sub>)</td><td>c<sub>2.1</sub>: B</td><td>16</td></tr><tr><td>9</td><td>R<sup>^</sup>(c): B ^ C</td><td>0.1</td><td>? R<sup>^</sup></td><td>8</td></tr><tr><td>11</td><td>c<sub>2</sub>: B ^ C</td><td>9</td><td>? .../R<sup>^</sup>(c)</td><td>10</td></tr><tr><td>13</td><td>L<sup>^</sup>(c<sub>2</sub>): B</td><td>11</td><td>? L<sup>^</sup></td><td>12</td></tr><tr><td>15</td><td>c<sub>2.1</sub>: B</td><td>13</td><td>? .../L<sup>^</sup>(c<sub>2</sub>)</td><td>14</td></tr><tr><td>17</td><td>? = c<sub>2.1</sub></td><td>16</td><td>L<sup>^</sup>(c<sub>2</sub>) = c<sub>2.1</sub>: B</td><td>18</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>c: A ^ (B ^ C)</td><td>! (A ^ B) ^ C [c: A ^ (B ^ C)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>^</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>c<sub>2.2</sub>: C</td><td>12</td></tr><tr><td>5</td><td>R<sup>^</sup>(c): B ^ C</td><td>0.1</td><td>? R<sup>^</sup></td><td>4</td></tr><tr><td>7</td><td>c<sub>2</sub>: B ^ C</td><td>5</td><td>? .../R<sup>^</sup>(c)</td><td>6</td></tr><tr><td>9</td><td>R<sup>^</sup>(c<sub>2</sub>): C</td><td>7</td><td>? R<sup>^</sup></td><td>8</td></tr><tr><td>11</td><td>c<sub>2.2</sub>: C</td><td>9</td><td>? .../R<sup>^</sup>(c<sub>2</sub>)</td><td>10</td></tr><tr><td>13</td><td>? = c<sub>2.2</sub></td><td>12</td><td>R<sup>^</sup>(c<sub>2</sub>) = c<sub>2.2</sub>: C</td><td>14</td></tr></tbody></table>

P wins

The core of the strategy can be found section VII.7.4.

$$ \text{VII.6.7} \quad *(B \wedge A) \supset C [c: (A \wedge B) \supset C] $$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>c: (A ^ B) ⊃ C</td><td>! (B ^ A) ⊃ C [c: (A ^ B) ⊃ C]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: B ^ A</td><td>c<sub>2</sub>: C</td><td>18 [P<sub>1R</sub>]</td></tr><tr><td>5</td><td>L<sup>^</sup>(d<sub>1</sub>): B</td><td>3</td><td>? L<sup>^</sup></td><td>4</td></tr><tr><td>7</td><td>d<sub>1.1</sub>: B</td><td>5</td><td>? .../L<sup>^</sup>(d<sub>1</sub>)</td><td>6</td></tr><tr><td>9</td><td>R<sup>^</sup>(d<sub>1</sub>): A</td><td>3</td><td>? R<sup>^</sup></td><td>8</td></tr><tr><td>11</td><td>d<sub>1.2</sub>: A</td><td>7</td><td>? .../R<sup>^</sup>(d<sub>1</sub>)</td><td>10</td></tr></tbody></table>
<table><tr><td></td><td>...</td><td>0.1</td><td>L<sup>2</sup>(c): A ∧ B</td><td>12</td></tr><tr><td>13</td><td>? .../L<sup>2</sup>(c)</td><td>12</td><td>c<sub>1</sub>: A ∧ B</td><td>14</td></tr></table>

<table><tr><td>P<sub>1L</sub></td><td>15</td><td>? L<sup>1</sup> [δ<sub>1</sub>, ...]</td><td>14</td><td>L<sup>1</sup>(c<sub>1</sub>): A</td><td>16</td></tr><tr><td></td><td>17</td><td>? .../L<sup>1</sup>(c<sub>1</sub>)</td><td>16</td><td>d<sub>1,2</sub>: A</td><td>18</td></tr><tr><td></td><td>19</td><td>? = d<sub>1,2</sub></td><td>18</td><td>R<sup>1</sup>(d<sub>1</sub>) = d<sub>1,2</sub>: A</td><td>20</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>15</td><td>R<sup>2</sup>(c): C</td><td></td><td>...</td><td></td></tr><tr><td></td><td>17</td><td>c<sub>2</sub>: C</td><td>15</td><td>? .../R<sup>2</sup>(c)</td><td>16</td></tr><tr><td></td><td>19</td><td>? = c<sub>2</sub></td><td>18</td><td>R<sup>2</sup>(c) = c<sub>2</sub>: C</td><td>20</td></tr></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>c: (A ∧ B) ⊃ C</td><td>! (B ∧ A) ⊃ C [c: (A ∧ B) ⊃ C]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: B ∧ A</td><td>c<sub>2</sub>: C</td><td>18 [P<sub>1R</sub>]</td></tr><tr><td>5</td><td>L<sup>1</sup>(d<sub>1</sub>): B</td><td>3</td><td>? L<sup>1</sup></td><td>4</td></tr><tr><td>7</td><td>d<sub>1,1</sub>: B</td><td>5</td><td>? .../L<sup>1</sup>(d<sub>1</sub>)</td><td>6</td></tr><tr><td>9</td><td>R<sup>1</sup>(d<sub>1</sub>): A</td><td>3</td><td>? R<sup>1</sup></td><td>8</td></tr><tr><td>11</td><td>d<sub>1,2</sub>: A</td><td>7</td><td>? .../R<sup>1</sup>(d<sub>1</sub>)</td><td>10</td></tr><tr><td></td><td>...</td><td>0.1</td><td>L<sup>2</sup>(c): A ∧ B</td><td>12</td></tr><tr><td>13</td><td>? .../L<sup>2</sup>(c)</td><td>12</td><td>c<sub>1</sub>: A ∧ B</td><td>14</td></tr></tbody></table>

<table><tr><td>P<sub>2L</sub></td><td>15</td><td>? R<sup>1</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>14</td><td>R<sup>1</sup>(c<sub>1</sub>): B</td><td>16</td></tr><tr><td></td><td>17</td><td>? .../R<sup>1</sup>(c<sub>1</sub>)</td><td>16</td><td>d<sub>1,1</sub>: B</td><td>18</td></tr><tr><td></td><td>19</td><td>? = d<sub>1,1</sub></td><td>18</td><td>L<sup>1</sup>(d<sub>1</sub>) = d<sub>1,1</sub>: B</td><td>20</td></tr></table>

P wins

<table><tr><td>P<sub>2R</sub></td><td>15</td><td>R<sup>2</sup>(c): C</td><td></td><td>...</td><td></td></tr><tr><td></td><td>17</td><td>c<sub>2</sub>: C</td><td>15</td><td>? .../R<sup>2</sup>(c)</td><td>16</td></tr><tr><td></td><td>19</td><td>? = c<sub>2</sub></td><td>18</td><td>R<sup>2</sup>(c) = c<sub>2</sub>: C</td><td>20</td></tr></table>

P wins

The core of the strategy can be found section VII.7.4.

$$ \text{VII.6.8} \quad ((\forall x: D)A(x)) \supset \bot [(\exists x: D)(A(x) \supset \bot)] $$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>!(∃x: D)(A(x) ⊃ ∨)</td><td>!((∀x: D)A(x)) ⊃ ∨<br/>[(∃x: D)(A(x) ⊃ ∨)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: (∀x: D)A(x)</td><td>you<sub>gave up</sub>(19 [P<sub>1R</sub>]): ⊕</td><td>20[P<sub>1R</sub>]</td></tr></tbody></table>
<table><tr><td>5</td><td>c<sub>1</sub>: d</td><td>0.1</td><td>? L<sup>3</sup></td><td>4</td></tr><tr><td>7</td><td>c<sub>2</sub>: A(c<sub>1</sub>) ⊃ ⊥</td><td>0.1</td><td>? R<sup>3</sup></td><td>6</td></tr><tr><td>13</td><td>R<sup>∀</sup>(d<sub>1</sub>): A(c<sub>1</sub>)</td><td>3</td><td>L<sup>∀</sup>(d<sub>1</sub>): D</td><td>8</td></tr><tr><td>9</td><td>? .../L<sup>∀</sup>(d<sub>1</sub>)</td><td>8</td><td>c<sub>1</sub>: D</td><td>10</td></tr><tr><td>11</td><td>? = c<sub>1</sub></td><td>10</td><td>c<sub>1</sub> = c<sub>1</sub>: D</td><td>12</td></tr><tr><td>15</td><td>d<sub>1.2</sub>: A(c<sub>1</sub>)</td><td>13</td><td>? .../R<sup>∀</sup>(d<sub>1</sub>)</td><td>14</td></tr><tr><td colspan="3">...</td><td>L<sup>∃</sup>(c<sub>2</sub>): A(c<sub>1</sub>)</td><td>16</td></tr><tr><td>17</td><td>? .../L<sup>∃</sup>(c<sub>2</sub>)</td><td>16</td><td>d<sub>1.2</sub>: A(c<sub>1</sub>)</td><td>18</td></tr></table>

<table><tr><td>P<sub>1L</sub></td><td>19</td><td>? = d<sub>1.2</sub></td><td>18</td><td>R<sup>∀</sup>(d<sub>1</sub>) = d<sub>1.2</sub>: A(c<sub>1</sub>)</td><td>20</td></tr></table>

P wins

<table><tr><td>P<sub>1R</sub></td><td>19</td><td>R<sup>∃</sup>(c<sub>2</sub>): ⊥</td><td>...</td></tr></table>

P wins

$$ \text{VII.6.9} \quad (\exists x: D)A(x) \wedge (\exists x: D)B(x) [(\exists x: D)(A(x) \wedge B(x))] $$

<table><thead><tr><th colspan="2">P<sub>1</sub></th><th>O</th><th>P</th></tr></thead><tbody><tr><td>0.1</td><td>! (∃x: D)(A(x) ∧ B(x))</td><td></td><td>! (∃x: D)A(x) ∧ (∃x: D)B(x) [(∃x: D)(A(x) ∧ B(x))]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∧</sup></td><td>0</td><td>d<sub>1</sub>: (∃x: D)A(x)</td><td>4</td></tr><tr><td>5</td><td>? L<sup>∃</sup> [δ<sub>1</sub>, ...]</td><td>4</td><td>L<sup>∃</sup>(d<sub>1</sub>): D</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>∃</sup>(d<sub>1</sub>)</td><td>6</td><td>c<sub>1</sub>: D</td><td>10</td></tr><tr><td>9</td><td>c<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>∃</sup></td><td>8</td></tr><tr><td>11</td><td>? = c<sub>1</sub></td><td>10</td><td>c<sub>1</sub> = c<sub>1</sub>: D</td><td>12</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">P<sub>2</sub></th><th>O</th><th>P</th></tr></thead><tbody><tr><td>0.1</td><td>! (∃x: D)(A(x) ∧ B(x))</td><td></td><td>! (∃x: D)A(x) ∧ (∃x: D)B(x) [(∃x: D)(A(x) ∧ B(x))]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∧</sup> [δ<sub>2</sub>, ...]</td><td>0</td><td>d<sub>1</sub>: (∃x: D)A(x)</td><td>4</td></tr><tr><td>5</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>4</td><td>R<sup>∃</sup>(d<sub>1</sub>): A(c<sub>1</sub>)</td><td>14</td></tr><tr><td>7</td><td>c<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>∃</sup></td><td>6</td></tr><tr><td>9</td><td>c<sub>2</sub>: A(c<sub>1</sub>) ∧ B(c<sub>1</sub>)</td><td>0.1</td><td>? R<sup>∃</sup></td><td>8</td></tr><tr><td>11</td><td>L<sup>∧</sup>(c<sub>2</sub>): A(c<sub>1</sub>)</td><td>9</td><td>? L<sup>∃</sup></td><td>10</td></tr><tr><td>13</td><td>c<sub>2.1</sub>: A(c<sub>1</sub>)</td><td>11</td><td>? .../L<sup>∧</sup>(c<sub>2</sub>)</td><td>12</td></tr><tr><td>15</td><td>? .../R<sup>∃</sup>(d<sub>1</sub>)</td><td>14</td><td>c<sub>2.1</sub>: A(c<sub>1</sub>)</td><td>16</td></tr><tr><td>17</td><td>? = c<sub>2.1</sub></td><td>16</td><td>L<sup>∧</sup>(c<sub>2</sub>) = c<sub>2.1</sub>: A(c<sub>1</sub>)</td><td>18</td></tr></tbody></table>

P wins

<table><tr><td>P<sub>3</sub></td><td>O</td><td>P</td></tr></table>
<table><tr><td>0.1</td><td>!(∃x: D)(A(x) ∧ B(x))</td><td></td><td>!(∃x: D)A(x) ∧ (∃x: D)B(x)<br/>[(∃x: D)(A(x) ∧ B(x))]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>^</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>0</td><td>d<sub>2</sub>: (∃x: D)B(x)</td><td>4</td></tr><tr><td>5</td><td>? L<sup>∃</sup> [δ<sub>3</sub>, ...]</td><td>4</td><td>L<sup>∃</sup>(d<sub>2</sub>): D</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>∃</sup>(d<sub>2</sub>)</td><td>6</td><td>c<sub>1</sub>: D</td><td>10</td></tr><tr><td>9</td><td>c<sub>1</sub>: D</td><td></td><td>? L<sup>∃</sup></td><td>8</td></tr><tr><td>11</td><td>? = c<sub>1</sub></td><td>10</td><td>c<sub>1</sub> = c<sub>1</sub>: D</td><td>12</td></tr></table>

P wins

<table><thead><tr><th>P<sub>4</sub></th><th>O</th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!(∃x: D)(A(x) ∧ B(x))</td><td>!(∃x: D)A(x) ∧ (∃x: D)B(x)<br/>[(∃x: D)(A(x) ∧ B(x))]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>^</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>d<sub>2</sub>: (∃x: D)B(x)</td><td>4</td></tr><tr><td>5</td><td>? L<sup>∃</sup> [δ<sub>3</sub>, δ<sub>4</sub>]</td><td>R<sup>∃</sup>(d<sub>2</sub>): B(c<sub>1</sub>)</td><td>14</td></tr><tr><td>8</td><td>c<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>∃</sup></td><td>6</td></tr><tr><td>9</td><td>c<sub>2</sub>: A(c<sub>1</sub>) ∧ B(c<sub>1</sub>)</td><td>0.1</td><td>? R<sup>∃</sup></td><td>8</td></tr><tr><td>11</td><td>R<sup>^</sup>(c<sub>2</sub>): B(c<sub>1</sub>)</td><td>9</td><td>? R<sup>∃</sup></td><td>10</td></tr><tr><td>13</td><td>c<sub>2.2</sub>: B(c<sub>1</sub>)</td><td>11</td><td>? .../R<sup>^</sup>(c<sub>2</sub>)</td><td>12</td></tr><tr><td>15</td><td>? .../R<sup>∃</sup>(d<sub>2</sub>)</td><td>14</td><td>c<sub>2.2</sub>: B(c<sub>1</sub>)</td><td>16</td></tr><tr><td>17</td><td>? = c<sub>2.2</sub></td><td>16</td><td>R<sup>^</sup>(c<sub>2</sub>) = c<sub>2.2</sub>: B(c<sub>1</sub>)</td><td>18</td></tr></tbody></table>

P wins

$$ \text{VII.6.10} \quad (\exists x: D)(\exists y: D)(A(x) \supset B(y))[A(a) \supset B(b); a: D; b: D] $$

<table><thead><tr><th>P<sub>1</sub></th><th>O</th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!A(a) ⊃ B(b)</td><td>!(∃x: D)(∃y: D)(A(x) ⊃ B(y))</td><td>0</td></tr><tr><td>0.2</td><td>a: D</td><td rowspan="2">[A(a) ⊃ B(b); a: D; b: D]</td><td rowspan="2"></td></tr><tr><td>0.3</td><td>b: D</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∃</sup> [δ<sub>1</sub>, ...]</td><td>a: D</td><td>4</td></tr><tr><td>5</td><td>? = a</td><td>a = a: D</td><td>6</td></tr></tbody></table>

P wins

<table><thead><tr><th>P<sub>2</sub></th><th>O</th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!A(a) ⊃ B(b)</td><td>!(∃x: D)(∃y: D)(A(x) ⊃ B(y))</td><td>0</td></tr><tr><td>0.2</td><td>a: D</td><td rowspan="2">[A(a) ⊃ B(b); a: D; b: D]</td><td rowspan="2"></td></tr><tr><td>0.3</td><td>b: D</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>d<sub>2</sub>: (∃x: D)(A(a) ⊃ B(y))</td><td>4</td></tr><tr><td>5</td><td>? L<sup>∃</sup> [δ<sub>2</sub>, ...]</td><td>b: D</td><td>6</td></tr><tr><td>7</td><td>? = b</td><td>b = b: D</td><td>8</td></tr></tbody></table>

P wins
<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!A(a) ⊃ B(b)</td><td></td><td>! (∃x: D)(∃y: D)(A(x) ⊃ B(y))</td><td>0</td></tr><tr><td>0.2</td><td>a: D</td><td></td><td rowspan="2">[A(a) ⊃ B(b); a: D ; b: D]</td><td></td></tr><tr><td>0.3</td><td>b: D</td><td></td><td></td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>0</td><td>d<sub>2</sub>: (∃y: D)(A(a) ⊃ B(y))</td><td>4</td></tr><tr><td>5</td><td>? R<sup>∃</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>4</td><td>R<sup>∃</sup>(d<sub>2</sub>): A(a) ⊃ B(b)</td><td>6</td></tr><tr><td>7</td><td>? .../R<sup>∃</sup>(d<sub>2</sub>)</td><td>6</td><td>d<sub>2.2</sub>: A(a) ⊃ B(b)</td><td>8</td></tr><tr><td>9</td><td>L<sup>∃</sup>(d<sub>2.2</sub>): A(a)</td><td>8</td><td>R<sup>∃</sup>(d<sub>2.2</sub>): B(b)</td><td>12</td></tr><tr><td>11</td><td>d<sub>2.2.1</sub>: A(a)</td><td></td><td>? .../L<sup>∃</sup>(d<sub>2.2</sub>)</td><td>10</td></tr><tr><td>13</td><td>? .../R<sup>∃</sup>(d<sub>2.2</sub>)</td><td>12</td><td>d<sub>2.2.2</sub>: B(b)</td><td>16 [P<sub>3R</sub>]</td></tr><tr><td></td><td>...</td><td></td><td>d<sub>2.2.1</sub>: A(a)</td><td>14</td></tr></tbody></table>

<table><tr><td>P<sub>3L</sub></td><td>15</td><td>? = d<sub>2.2.1</sub></td><td>14</td><td>L<sup>∃</sup>(d<sub>2.2</sub>) = d<sub>2.2.1</sub>: A(a)</td><td>16</td></tr></table>

P wins

<table><tr><td>P<sub>3R</sub></td><td>15</td><td>d<sub>2.2.2</sub>: B(b)</td><td>6</td><td>...</td><td></td></tr><tr><td></td><td>17</td><td>? = d<sub>2.2.2</sub>: B(b)</td><td>16</td><td>d<sub>2.2.2</sub> = d<sub>2.2.2</sub>: B(b)</td><td>18</td></tr></table>

P wins

VII.6.11 (∃x: D)B(x) ∧ (∃x: D)P(x)[B(a) ∧ P(b); a: D ; b: D]

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!B(a) ∧ P(b)</td><td></td><td>! (∃x: D)B(x) ∧ (∃x: D)P(x)</td><td>0</td></tr><tr><td>0.2</td><td>a: D</td><td></td><td rowspan="2">[B(a) ∧ P(b); a: D ; b: D]</td><td></td></tr><tr><td>0.3</td><td>b: D</td><td></td><td></td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∃</sup></td><td>0</td><td>d<sub>1</sub>: (∃x: D)B(x)</td><td>4</td></tr><tr><td>5</td><td>? L<sup>∃</sup> [δ<sub>1</sub>, ...]</td><td>4</td><td>L<sup>∃</sup>(d<sub>1</sub>): D</td><td>6</td></tr><tr><td>7</td><td>? .../L<sup>∃</sup>(d<sub>1</sub>)</td><td>6</td><td>a: D</td><td>8</td></tr><tr><td>9</td><td>? = a</td><td>8</td><td>a = a: D</td><td>10</td></tr></tbody></table>

P wins

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>!B(a) ∧ P(b)</td><td></td><td>! (∃x: D)B(x) ∧ (∃x: D)P(x)</td><td>0</td></tr><tr><td>0.2</td><td>a: D</td><td></td><td rowspan="2">[B(a) ∧ P(b); a: D ; b: D]</td><td></td></tr><tr><td>0.3</td><td>b: D</td><td></td><td></td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∃</sup> [δ<sub>2</sub>, ...]</td><td>0</td><td>d<sub>1</sub>: (∃x: D)B(x)</td><td>4</td></tr><tr><td>5</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>4</td><td>R<sup>∃</sup>(d<sub>1</sub>): B(a)</td><td>6</td></tr><tr><td>7</td><td>? .../R<sup>∃</sup>(d<sub>1</sub>)</td><td>6</td><td>c<sub>1</sub>: B(a)</td><td>10</td></tr><tr><td>9</td><td>c<sub>1</sub>: B(a)</td><td>0.1</td><td>? L<sup>∃</sup></td><td>8</td></tr><tr><td>11</td><td>? = c<sub>1</sub></td><td>10</td><td>c<sub>1</sub> = c<sub>1</sub>: B(a)</td><td>12</td></tr></tbody></table>

P wins
<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>!B(a) ∧ P(b)</td><td colspan="2">! (∃x: D)B(x) ∧ (∃x: D)P(x)</td></tr><tr><td>0.2</td><td>a: D</td><td colspan="2">[B(a) ∧ P(b); a: D ; b: D]</td></tr><tr><td>0.3</td><td>b: D</td><td colspan="2">0</td></tr><tr><td>1</td><td>m := 1</td><td colspan="2">n := 2</td></tr><tr><td>3</td><td>? L<sup>1</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td colspan="2">d<sub>2</sub>: (∃x: D)P(x)</td></tr><tr><td>5</td><td>? L<sup>3</sup> [δ<sub>3</sub>, ...]</td><td colspan="2">L<sup>3</sup>(d<sub>2</sub>): D</td></tr><tr><td>7</td><td>? .../L<sup>3</sup>(d<sub>2</sub>)</td><td colspan="2">b: D</td></tr><tr><td>9</td><td>? = b</td><td colspan="2">b = b: D</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>! B(a) ∧ P(b)</td><td colspan="2">! (∃x: D)B(x) ∧ (∃x: D)P(x)</td></tr><tr><td>0.2</td><td>a: D</td><td colspan="2">[B(a) ∧ P(b); a: D ; b: D]</td></tr><tr><td>0.3</td><td>b: D</td><td colspan="2">0</td></tr><tr><td>1</td><td>m := 1</td><td colspan="2">n := 2</td></tr><tr><td>3</td><td>? L<sup>1</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td colspan="2">d<sub>2</sub>: (∃x: D)P(x)</td></tr><tr><td>5</td><td>? R<sup>3</sup> [δ<sub>3</sub>, δ<sub>4</sub>]</td><td colspan="2">R<sup>3</sup>(d<sub>2</sub>): P(b)</td></tr><tr><td>7</td><td>? .../R<sup>3</sup>(d<sub>2</sub>)</td><td colspan="2">c<sub>2</sub>: P(b)</td></tr><tr><td>9</td><td>c<sub>2</sub>: P(b)</td><td>0.1</td><td>? R<sup>1</sup></td></tr><tr><td>11</td><td>? = c<sub>2</sub></td><td colspan="2">c<sub>2</sub> = c<sub>2</sub>: P(b)</td></tr></tbody></table>

P wins

$$ \text{VII.6.12} \quad (\exists x: D)(\exists y: D)A(x, y)[(\exists x: D)A(x, x)] $$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>! (∃x: D)A(x, x)</td><td colspan="2">! (∃x: D)(∃y: D)A(x, y)<br/>[(∃x: D)A(x, x)]</td></tr><tr><td>1</td><td>m := 1</td><td colspan="2">n := 2</td></tr><tr><td>3</td><td>? L<sup>3</sup> [δ<sub>1</sub>, ...]</td><td colspan="2">d<sub>1</sub>: D</td></tr><tr><td>5</td><td>d<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>3</sup></td></tr><tr><td>7</td><td>? = a</td><td colspan="2">d<sub>1</sub> = d<sub>1</sub>: D</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>! (∃x: D)A(x, x)</td><td colspan="2">! (∃x: D)(∃y: D)A(x, y)<br/>[(∃x: D)A(x, x)]</td></tr><tr><td>1</td><td>m := 1</td><td colspan="2">n := 2</td></tr><tr><td>3</td><td>? R<sup>3</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td colspan="2">d<sub>3</sub>: (∃y: D)A(d<sub>1</sub>, y)</td></tr><tr><td>5</td><td>d<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>3</sup></td></tr><tr><td>7</td><td>d<sub>2</sub>: A(d<sub>1</sub>, d<sub>1</sub>)</td><td>0.1</td><td>? R<sup>3</sup></td></tr><tr><td>9</td><td>? L<sup>3</sup> [δ<sub>2</sub>, ...]</td><td colspan="2">L<sup>3</sup>(d<sub>3</sub>): D</td></tr><tr><td>11</td><td>? .../L<sup>3</sup>(d<sub>3</sub>)</td><td colspan="2">d<sub>1</sub>: D</td></tr><tr><td>13</td><td>? = d<sub>1</sub></td><td colspan="2">d<sub>1</sub> = d<sub>1</sub>: D</td></tr></tbody></table>
P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>!(∃x: D)A(x, x)</td><td>!(∃x: D)(∃y: D)A(x, y)<br/>[(∃x: D)A(x, x)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>∃</sup>[δ<sub>1</sub>, δ<sub>2</sub>]</td><td>d<sub>3</sub>: (∃y: D)A(d<sub>1</sub>, y)</td><td>8</td></tr><tr><td>5</td><td>d<sub>1</sub>: D</td><td>0.1</td><td>? L<sup>∃</sup></td><td>4</td></tr><tr><td>7</td><td>d<sub>2</sub>: A(d<sub>1</sub>, d<sub>1</sub>)</td><td>0.1</td><td>? R<sup>∃</sup></td><td>6</td></tr><tr><td>9</td><td>? R<sup>∃</sup> [δ<sub>2</sub>, δ<sub>3</sub>]</td><td>R<sup>∃</sup>(d<sub>3</sub>): A(d<sub>1</sub>, d<sub>1</sub>)</td><td>10</td></tr><tr><td>11</td><td>? .../R<sup>∃</sup>(d<sub>3</sub>)</td><td>d<sub>2</sub>: A(d<sub>1</sub>, d<sub>1</sub>)</td><td>12</td></tr><tr><td>13</td><td>? = d<sub>2</sub></td><td>d<sub>2</sub> = d<sub>2</sub>: A(d<sub>1</sub>, d<sub>1</sub>)</td><td>14</td></tr></tbody></table>

P wins

$$ \text{VII.6.13} \quad (\forall x: D)(\forall y: D)(A(x, y) \wedge A(y, x))[(\forall x: D)(\forall y: D)A(x, y)] $$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>!(∀x: D)(∀y: D)A(x, y)</td><td>!(∀x: D)(∀y: D)(A(x, y) ∧ A(y, x))<br/>[(∀x: D)(∀y: D)A(x, y)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: D</td><td>d<sub>2</sub>: (∀y: D)(A(d<sub>1</sub>, y) ∧ A(y, d<sub>1</sub>))</td><td>4</td></tr><tr><td>5</td><td>L<sup>∀</sup>(d<sub>2</sub>): D</td><td>R<sup>∀</sup>(d<sub>2</sub>): A(d<sub>1</sub>, d<sub>2.1</sub>) ∧ A(d<sub>2.1</sub>, d<sub>1</sub>)</td><td>8</td></tr><tr><td>7</td><td>d<sub>2.1</sub>: D</td><td>5</td><td>? .../L<sup>∃</sup>(d<sub>2</sub>)</td><td>6</td></tr><tr><td>9</td><td>? .../R<sup>∀</sup>(d<sub>2</sub>)</td><td>d<sub>2.2</sub>: A(d<sub>1</sub>, d<sub>2.1</sub>) ∧ A(d<sub>2.1</sub>, d<sub>1</sub>)</td><td>10</td></tr><tr><td>11</td><td>? L<sup>∀</sup> [δ<sub>1</sub>, ...]</td><td>L<sup>∀</sup>(d<sub>2.2</sub>): A(d<sub>1</sub>, d<sub>2.1</sub>)</td><td>12</td></tr><tr><td>13</td><td>? .../L<sup>∀</sup>(d<sub>2.2</sub>)</td><td>c<sub>2.2</sub>: A(d<sub>1</sub>, d<sub>2.1</sub>)</td><td>26</td></tr><tr><td>17</td><td>c<sub>2</sub>: (∀y: D)A(d<sub>1</sub>, y)</td><td>0.1</td><td>d<sub>1</sub>: D</td><td>14</td></tr><tr><td>15</td><td>? = d<sub>1</sub></td><td>d<sub>1</sub> = d<sub>1</sub>: D</td><td>16</td></tr><tr><td>23</td><td>R<sup>∀</sup>(c<sub>2</sub>): A(d<sub>1</sub>, d<sub>2.1</sub>)</td><td>17</td><td>L<sup>∀</sup>(c<sub>2</sub>): D</td><td>18</td></tr><tr><td>19</td><td>? .../L<sup>∀</sup>(c<sub>2</sub>)</td><td>d<sub>2.1</sub>: D</td><td>20</td></tr><tr><td>21</td><td>? = d<sub>2.1</sub></td><td>L<sup>∀</sup>(d<sub>2</sub>) = d<sub>2.1</sub>: D</td><td>22</td></tr><tr><td>25</td><td>c<sub>2.2</sub>: A(d<sub>1</sub>, d<sub>2.1</sub>)</td><td>23</td><td>? .../R<sup>∀</sup>(c<sub>2</sub>)</td><td>24</td></tr><tr><td>27</td><td>? = c<sub>2.2</sub></td><td>R<sup>∀</sup>(c<sub>2</sub>) = c<sub>2.2</sub>: A(d<sub>1</sub>, d<sub>2.1</sub>)</td><td>28</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>!(∀x: D)(∀y: D)A(x, y)</td><td>!(∀x: D)(∀y: D)(A(x, y) ∧ A(y, x))<br/>[(∀x: D)(∀y: D)A(x, y)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>d<sub>1</sub>: D</td><td>d<sub>2</sub>: (∀y: D)(A(d<sub>1</sub>, y) ∧ A(y, d<sub>1</sub>))</td><td>4</td></tr><tr><td>5</td><td>L<sup>∀</sup>(d<sub>2</sub>): D</td><td>R<sup>∀</sup>(d<sub>2</sub>): A(d<sub>1</sub>, d<sub>2.1</sub>) ∧ A(d<sub>2.1</sub>, d<sub>1</sub>)</td><td>8</td></tr><tr><td>7</td><td>d<sub>2.1</sub>: D</td><td>5</td><td>? .../L<sup>∃</sup>(d<sub>2</sub>)</td><td>6</td></tr><tr><td>9</td><td>? .../R<sup>∀</sup>(d<sub>2</sub>)</td><td>d<sub>2.2</sub>: A(d<sub>1</sub>, d<sub>2.1</sub>) ∧ A(d<sub>2.1</sub>, d<sub>1</sub>)</td><td>10</td></tr><tr><td>11</td><td>? R<sup>∀</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>R<sup>∀</sup>(d<sub>2.2</sub>): A(d<sub>2.1</sub>, d<sub>1</sub>)</td><td>12</td></tr></tbody></table>
<table><tr><td>13</td><td>? .../R<sup>^</sup>(d<sub>2,2</sub>)</td><td>12</td><td>c<sub>2,2</sub>: A(d<sub>2,1</sub>, d<sub>1</sub>)</td><td>26</td></tr><tr><td>17</td><td>c<sub>2</sub>: (∀y: D)A(d<sub>2,1</sub>, y)</td><td>0.1</td><td>d<sub>2,1</sub>: D</td><td>14</td></tr><tr><td>15</td><td>? = d<sub>2,1</sub></td><td>14</td><td>L<sup>^</sup>(d<sub>2</sub>) = d<sub>2,1</sub>: D</td><td>16</td></tr><tr><td>23</td><td>R<sup>^</sup>(c<sub>2</sub>): A(d<sub>2,1</sub>, d<sub>1</sub>)</td><td>17</td><td>L<sup>^</sup>(c<sub>2</sub>): D</td><td>18</td></tr><tr><td>19</td><td>? .../L<sup>^</sup>(c<sub>2</sub>)</td><td>18</td><td>d<sub>1</sub>: D</td><td>20</td></tr><tr><td>21</td><td>? = d<sub>1</sub></td><td>20</td><td>d<sub>1</sub> = d<sub>1</sub>: D</td><td>22</td></tr><tr><td>25</td><td>c<sub>2,2</sub>: A(d<sub>2,1</sub>, d<sub>1</sub>)</td><td>23</td><td>? .../R<sup>^</sup>(c<sub>2</sub>)</td><td>24</td></tr><tr><td>27</td><td>? = c<sub>2,2</sub></td><td>26</td><td>R<sup>^</sup>(c<sub>2</sub>) = c<sub>2,2</sub>: A(d<sub>2,1</sub>, d<sub>1</sub>)</td><td>28</td></tr></table>

P wins

$$ \text{VII.6.14} \quad (\exists x: D)(A(x) \supset (\forall x: D)A(x)) \quad [((\exists x: D)(A(x) \supset \bot)) \lor ((\forall x: D)A(x)); a: D] $$

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1<br>0.2</td><td>!( (∃x: D)(A(x) ⊃ ⊥)) ∨ ((∀x: D)A(x))<br>a: D</td><td>!( (∃x: D)(A(x) ⊃ (�forall x: D)A(x))<br>[( (∃x: D)(A(x) ⊃ ⊥))<br>∨ ((∀x: D)A(x)); a: D]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? L<sup>∃</sup> [δ<sub>1</sub>, ...]</td><td>a: D</td><td>4</td></tr><tr><td>5</td><td>? = a</td><td>a = a: D</td><td>6</td></tr></tbody></table>

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1<br>0.2</td><td>!( (∃x: D)(A(x) ⊃ ⊥)) ∨ ((∀x: D)A(x))<br>a: D</td><td>!( (∃x: D)(A(x) ⊃ (�forall x: D)A(x))<br>[( (∃x: D)(A(x) ⊃ ⊥)) ∨ ((∀x: D)A(x))]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>d<sub>2</sub>: A(c<sub>1,1</sub>) ⊃ (�forall x: D)A(x)</td><td>14</td></tr><tr><td>5</td><td>c<sub>1</sub>: (∃x: D)(A(x) ⊃ ⊥) [δ<sub>2</sub>, ...]</td><td>0.1</td><td>? ∨</td></tr><tr><td>7</td><td>L<sup>∃</sup>(c<sub>1</sub>): D</td><td>5</td><td>? L<sup>∃</sup></td></tr><tr><td>9</td><td>c<sub>1,1</sub>: D</td><td>7</td><td>? .../L<sup>∃</sup>(c<sub>1</sub>)</td></tr><tr><td>11</td><td>R<sup>∃</sup>(c<sub>1</sub>): A(c<sub>1,1</sub>) ⊃ ⊥</td><td>5</td><td>? R<sup>∃</sup></td></tr><tr><td>13</td><td>c<sub>1,2</sub>: A(c<sub>1,1</sub>) ⊃ ⊥</td><td>11</td><td>? .../R<sup>∃</sup>(c<sub>1</sub>)</td></tr><tr><td>15</td><td>L<sup>∃</sup>(d<sub>2</sub>): A(c<sub>1,1</sub>)</td><td>14</td><td>you gave up (21 [P<sub>2R</sub>]): (�forall x: D)A(x) 22 [P<sub>2R</sub>]</td></tr><tr><td>17</td><td>d<sub>2,1</sub>: A(c<sub>1,1</sub>)</td><td>15</td><td>? .../L<sup>∃</sup>(d<sub>2</sub>)</td></tr><tr><td>...</td><td></td><td>13</td><td>L<sup>∃</sup>(c<sub>1,2</sub>): A(c<sub>1,1</sub>)</td></tr><tr><td>19</td><td>? .../L<sup>∃</sup>(c<sub>1,2</sub>)</td><td>18</td><td>d<sub>2,1</sub>: A(c<sub>1,1</sub>)</td></tr></tbody></table>

$$ \mathcal{P}_{2L} \quad \boxed{21} \quad ? = d_{1,2} \quad \boxed{20} \quad \boxed{L^2(d_2) = d_{2,1}: A(c_{1,1})} \quad \boxed{22} $$

P wins

$$ \mathcal{P}_{2R} \quad \boxed{21} \quad R^2(c_2): \bot \quad \boxed{...} $$

P wins

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody></tbody></table>
<table><tr><td>0.1<br>0.2</td><td>!(∃x: D)(A(x) ⊃ ∨)<br>a: D</td><td></td><td>!(∃x: D)(A(x) ⊃ (∀x: D)A(x))<br>[( (∃x: D)(A(x) ⊃ ∨))<br>∩ (∀x: D)A(x)]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td></td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>? R<sup>∃</sup> [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>0</td><td>d<sub>2</sub>: A(a) ⊃ (∀x: D)A(x)</td><td>6</td></tr><tr><td>5</td><td>c<sub>2</sub>: (∀x: D)A(x) [δ<sub>2</sub>, δ<sub>3</sub>]</td><td></td><td>0.1</td><td>4</td></tr><tr><td>7</td><td>L<sup>∃</sup>(d<sub>2</sub>): A(a)</td><td>6</td><td>R<sup>∃</sup>(d<sub>2</sub>): (∀x: D)A(x)</td><td>10</td></tr><tr><td>9</td><td>d<sub>2.1</sub>: A(a)</td><td></td><td>7</td><td>8</td></tr><tr><td>11</td><td>? .../R<sup>∃</sup>(d<sub>2</sub>)</td><td>10</td><td>d<sub>2.2</sub>: (∀x: D)A(x)</td><td>12</td></tr><tr><td>13</td><td>L<sup>∃</sup>(d<sub>2.2</sub>): D</td><td>12</td><td>R<sup>∃</sup>(d<sub>2.2</sub>): A(d<sub>2.2.1</sub>)</td><td>16</td></tr><tr><td>15</td><td>d<sub>2.2.1</sub>: D</td><td></td><td>13</td><td>14</td></tr><tr><td>17</td><td>? .../R<sup>∃</sup>(d<sub>2.2</sub>)</td><td>16</td><td>c<sub>2.1</sub>: A(d<sub>2.2.1</sub>)</td><td>26</td></tr><tr><td>23</td><td>R<sup>∀</sup>(c<sub>2</sub>): A(d<sub>2.2.1</sub>)</td><td></td><td>L<sup>∀</sup>(c<sub>2</sub>): D</td><td>18</td></tr><tr><td>19</td><td>? .../L<sup>∀</sup>(c<sub>2</sub>)</td><td>18</td><td>d<sub>2.2.1</sub>: D</td><td>20</td></tr><tr><td>21</td><td>? = d<sub>2.2.1</sub></td><td>20</td><td>L<sup>∃</sup>(d<sub>2.2</sub>) = d<sub>2.2.1</sub>: D</td><td>22</td></tr><tr><td>25</td><td>c<sub>2.1</sub>: A(d<sub>2.2.1</sub>)</td><td></td><td>23</td><td>24</td></tr><tr><td>27</td><td>? = c<sub>2.1</sub></td><td>26</td><td>R<sup>∀</sup>(c<sub>2</sub>) = c<sub>2.1</sub>: A(d<sub>2.2.1</sub>)</td><td>28</td></tr></table>

P wins

The graphic (tree) presentation of the core yields the following:

<figure><img src="image_22.png" /></figure>
21. $O? = d_{1.2}$ [?, 20]

22. $P L^{\supset}(d_2) = d_{2.1}: A(c_{1.1}) [!, 21]$ \\ $P$ wins

21. $O R^{\supset}(c_2): \perp [!, 20]$

22. $P you_{gave up}(21[P_{2R}]):$ \\
$(\forall x: D)A(x) [!, 15]$ \\ $P$ wins

22. $P L^{\supset}(d_{2.2}) = d_{2.2.1}: D[!, 21]$

23. $O R^{\supset}(c_2): A(d_{2.2.1})[!, 18]$

24. $P? .../R^{\supset}(c_2)[?, 23]$

25. $O c_{2.1}: A(d_{2.2.1}) [!, 24]$

26. $P c_{2.1}: A(d_{2.2.1})[!, 17]$

27. $O? = c_{2.1}$ [?, 26]

28. $P R^{\supset}(c_2) = c_{2.1}: A(d_{2.2.1})[!28]$ \\ $P$ wins

## VII.7 Strategic reasons in dialogues for immanent reasoning

The philosophical backbone on which rests the proof of admissibility provided in chapter IX,<fnref n="93" /> and which is one of the dialogical framework's greatest strengths, is probably the notion of strategic reason which allows to adopt a global view on all the possible plays that constitute a strategy; but this global view should not be identified with the perspective common in proof theory: strategic reasons are a kind of recapitulation of what can happen for a given thesis and show the entire history of the play by means of the instructions. Strategic reasons thus yield an overview of the possibilities enclosed in a thesis—what plays can be carried out from it—, but without ever being carried out in an actual play: they are only a perspective on all the possible variants of plays for a thesis and not an actual play. In this way the rules of synthesis and analysis of strategic reasons provided below are not of the same nature as the analysis and synthesis of local reasons, they are not produced through challenges and their defence, but are a recapitulation of the plays that can actually be carried out.

The notion of strategic reasons enables us to link dialogical strategies with CTT-demonstrations, since strategic reasons (and not local reasons) are the dialogical counterpart of CTT proof-objects; but it also shows clearly that the strategy level by itself—the only level that proof theory considers—is not enough: a deeper insight is gained when considering, together with the strategy level, the fundamental level of plays; strategic reasons thus bridge these two perspectives, the global view of strategies and the more in-depth and down-to-earth view of actual plays with all the possible variations in logic they allow,<fnref n="94" /> without sacrificing the one for the other.

This vindication of the play level is a key aspect of the dialogical framework and one of the purposes of the present study: other logical frameworks lack this dimension, which besides is not an extra dimension appended to the concern for demonstrations, but actually constitutes it, the heuristical procedure for building strategies out of plays showing the gapless link there is between the play level and the strategy level: strategies (and so demonstrations) stem from plays. Thus the dialogical framework can say at least as much as other logical frameworks, and, additionally, reveals limitations of other frameworks through this level of plays.

This final section presenting dialogues for immanent reasoning will be devoted first to a rather informal presentation of strategic reasons, stressing out the philosophical

<footnote n="93">⁹³ Chapter IX will focus on proving that dialogues for immanent reasoning is an admissible logical framework; it will therefore be rather technical and will address problems that mainly concern logicians, though we will here take care to outline the main philosophical aspects involved.</footnote>

<footnote n="94">⁹⁴ Among these variations can be counted cooperative games, non-monotony, the possibility of player errors or of limited knowledge or resources, to cite but a few options the play level offers, making the dialogical framework very well adapted for history and philosophy of logic.</footnote>