aspects underlying this key notion; then to the synthesis of strategic reasons and showing
the link with the introduction rules for CTT; and finally to the analysis of strategic
reasons. Once the rules have been provided, two examples will illustrate them and show
how to produce a strategic reason for the thesis out of the core of a strategy.

VII.7.1 Introducing strategic reasons

Strategic reasons belong to the strategy level, but are elements of the object-
language of the play level: they are the reasons brought forward by a player entitling him
to his statement. Strategic reasons are a perspective on plays that take into account all the
possible variations in the play for a given thesis; they are never actually carried out, since
any play is but the actualization of only one of all the possible plays for the thesis: each
individual play can be actualized but will be separate from the other individual plays that
can be carried out if other choices are made; strategic reasons allow to see together all
these possible plays that in fact are always separate. There will never be in any of the
plays the complex strategic reason for the thesis as a result of the application of the
particle rules, only the local reason for each of the subformulas involved; the strategic
reason will put all these separate reasons together as a recapitulation of what can be said
from the given thesis.

Consider for instance a conjunction: the Proponent claims to have a strategic reason
for this conjunction. This means that he claims that whatever the Opponent might play,
be it a challenge of the left or of the right conjunct, the Proponent will be able to win the
play. But in a single play with repetition rank 1 for the Opponent, there is no way to
check if a conjunction is justified, that is if both of the conjuncts can be defended, since a
play is precisely the carrying out of only one of the possible O-choices (challenging the
left or the right conjunct): to check both sides of a conjunction, two plays are required,
one in which the Opponent challenges the left side of the conjunction and another one for
the right side. So a strategic reason is never a single play, but refers to the strategy level
where all the possible outcomes are taken into account; the winning strategy can then be
displayed as a tree showing that both plays (respectively challenging and defending the
left conjunct and right conjunct) are won by the Proponent, thus justifying the
conjunction.

Let us now study what strategic reasons look like, how they are generated and how
they are analyzed.

A strategic perspective on a statement

In the standard framework of dialogues, where we do not explicitly have the
reasons for the statements in the object-language, the particle rules simply determine the
local meaning of the expressions. In dialogues for immanent reasoning, the reasons
entitling one to a statement are explicitely introduced; the particle rules (synthesis and
analysis of local reasons) govern both the local reasons and the local meaning of
expressions. But when building the core of a winning P-strategy, local reasons are also
linked to the justification of the statements—which is not the case if considering single
plays or non-winning strategies, for then only one aspect of the statement may be taken
into account during the play, the play providing thus only a partial justification.

Take again the example of a P-conjunction, say

$Pw : A \wedge B.$

In providing a strategic reason *w* for the conjunction *A* ∧ *B*, **P** is claiming to have a winning strategy for this conjunction, that is, he is claiming that the conjunction is absolutely justified, that he has a proper reason for asserting it and not simply a *local*
reason for stating it. Assuming that **O** has a repetition rank of 1 and has stated both **A** and **B** prior to move *i*, two different plays can be carried out from this point, which we provide without the strategic reason:

Play 12: introducing strategic reasons: stating a conjunction

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td>Concessions</td><td>Thesis</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td></tr><tr><td>...</td><td>...</td><td>! A ∧ B</td><td>i</td></tr></tbody></table>

Play 13: introducing strategic reasons: left decision option on conjunction

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td>Concessions</td><td>Thesis</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td></tr><tr><td>...</td><td>...</td><td>! A ∧ B</td><td>i</td></tr><tr><td>i + 1</td><td>? ∧<sub>1</sub></td><td>! A</td><td>i + 2</td></tr></tbody></table>

Play 14: introducing strategic reasons: right decision option on conjunction

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td>Concessions</td><td>Thesis</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td></tr><tr><td>...</td><td>...</td><td>! A ∧ B</td><td>i</td></tr><tr><td>i + 1</td><td>? ∧<sub>2</sub></td><td>! B</td><td>i + 2</td></tr></tbody></table>

So if **P** brings forward the strategic reason *w* to support his conjunction at move *i*, he is claiming to be able to win *both* Play 13 and Play 14, and yet the actual play will follow into only one of the two plays. Strategic reasons are thus a *strategic perspective* on a statement that is brought forward during actual plays.

## An anticipation of the play and a recapitulation of the strategy

Since a strategic reason (*w* for instance) is brought forward during a play (say at move *i*), it is clear that the play has not yet been carried out fully when the player claims to be able to defend his statement against whatever challenge his opponent might launch: bringing forward a strategic reason is thus an anticipation on the outcome of the play.

But strategic reasons are not a simple claim to have a winning strategy, they also have a complex internal structure: they can thus be considered as recapitulations of the plays of the winning strategy produced by the heuristic procedure, that is the winning strategy obtained only after running all the relevant plays; this strategy-building process specific to the dialogical framework is a richer process than the one yielding CTT demonstrations—or proof theory in general—, since the strategic reasons will contain traces of *choice dependences*, which constitute their complexity.
Choice dependences link possible moves of a player to the choices made by the other player: a player will play this move if his opponent used this decision-option, that move if the opponent used that decision-option. In the previous example, the Proponent will play move *i* + 2 depending on the Opponent's decision at move *i* + 1, so the strategic object *w* played at move *i* will contain these two possible scenarios with the *i* + 2 *P*-move depending on the *i* + 1 *O*-decision. The strategic reason *w* is thus a *recapitulation* of what would happen if each relevant play was carried out. When the strategic reason makes clearly explicit this choice-dependence of *P*'s moves on those of *O*, we say that it is in a *canonical argumentation form* and is a recapitulation of the statement.

The rules for strategic reasons do not provide the rules on how to play but rather
rules that indicate how a winning strategy has been achieved while applying the relevant
rules at the play level. Strategic reasons emerge as the result of considering the optimal
moves for a winning strategy: this is what a recapitulation is about.

The canonical argumentation form of strategic reasons is closely linked to the synthesis and analysis of local reasons: they provide the recapitulation of all the relevant local reasons that could be generated from a statement. In this respect following the rules for the synthesis and analysis of local reasons (see section VII.1.2), the rules for strategic reasons are divided into synthesis and analysis of strategic reasons, to which we will now turn.

In a nutshell, the synthesis of strategic reasons provides a guide for what **P** needs to be able to defend in order to justify his claim; the analysis of strategic reasons provides a guide for the local reasons **P** needs to make **O** state in order to copy these reasons and thus defend his statement.

## Assertions and statements

The difference between local reasons and strategic reasons should now be clear: while local reasons provide a local justification entitling one to his statement, strategic reasons provide an absolute justification of the statement, which thus becomes an *assertion*.

The equalities provided in each of the plays constituting a *P*-winning strategy, and found
in the analysis of strategic objects, convey the information required for *P* to play in the
best possible way by specifying those *O*-moves necessary for *P*'s victory. This
information however is not available at the very beginning of the first play, it is not made
explicit at the root of the tree containing all the plays relevant for the *P*-winning strategy:
the root of the tree will not explicitly display the information gathered while developing
the plays; this information will be available only once the whole strategy has been
developped, and each possible play considered. So when a play starts, the thesis is a
simple statement; it is only at the end of the construction process of the strategic reason
that *P* will be able to have the knowledge required to assert the thesis, and thus provide in
any new play a strategic reason for backing his thesis.

The *assertion* of the thesis, making explicit the strategic reason resulting from the
plays, is in this respect a *recapitulation* of the result achieved after running the relevant
plays, after *P*'s initial simple statement of that thesis. This is what the canonical
argumentation form of a strategic object is, and what renders the dialogical formulation
of a CTT canonical proof-object.

It is in this fashion that dialogical reasons correspond to CTT proof-objects:
introduction rules are usually characterized as the right to assert the conclusion from the
premises of the inference, that is, as defining what one needs in order to be entitled to
assert the conclusion; and the elimination rules are what can be inferred from a given statement. Thus, in the dialogical perspective of **P**-winning strategies, since we are looking at **P**'s entitlements and duties, what corresponds to proof-object introduction rules would define what **P** is required to justify in order to assert his statement, which is the synthesis of a **P**-strategic reason; and what corresponds to proof-object elimination rules would define what **P** is entitled to ask of **O** from her previous statements and thus say it himself by copying her statements, which is the analysis of **P**-strategic reasons. We will thus provide the rules for the synthesis and analysis of strategic reasons (always in the perspective of a **P**-winning strategy), followed by their corresponding CTT rule. We have in this regard a good justification of Sundholm's idea that inferences can be considered as involving an *implicit interlocutor*, but here at the strategy level.

### VII.7.2 Rules for the synthesis of P-strategic reasons: Strategic reasons as recapitulations of the local reasons required for a P-winning strategy

**P**-strategic reasons must be built (*synthesis* of **P**-strategic reasons); they constitute the justification of a statement by providing certain information—choice-dependences—that are essential to the relevant plays issuing from the statement: strategic reasons are a recapitulation of the building of a winning strategy, directly inserted into a play. Thus a strategic reason for a **P**-statement can have the form $p_2^P [[ p_1^O ]]$ and indicates that **P**'s choice of $p_2$ is dependent upon **O**'s choice of $p_1$. In this respect the synthesis of **P**-strategic reasons differ from the *analysis* of **P**-strategic reasons—dealt with in the following section (VII.7.3)—which provide a guide for all the local reasons **P** needs to ask **O** to provide in order for **P** to justify his statement through the equality rules.

Strategic reasons for **P** are the dialogical formulation of CTT proof-objects, and the canonical argumentation form of strategic reasons correspond to canonical proof-objects. Since in this chapter we are seeking a notion of winning strategy that corresponds to that of a CTT-demonstration, and since these strategies have being identified to be those where **P** wins, we will only provide the synthesis of strategic reasons for **P**.<fnref n="95" />

The rules for the synthesis of **P**-strategic reasons provide the strategic reasons in their *canonical argumentation form*, that is they make explicit the choice-dependences for **P**-moves based on **O**-decisions; the range of possibilities to take into account is dictated by the rules for the synthesis of local reasons, the synthesis of strategic reasons recapitulating what **P** needs to provide in order to have a winning strategy (or demonstration, that is, for his statement to be justified).

Thus for a conjunction, the rules for the synthesis of local reasons stipulates that **P** does not have the choice and must provide the local reason required by **O**. So in order to justify a conjunction, **P** must be able to provide a local reason for both of the conjuncts: the strategic reason for a conjunction will thus have the form $<p_1, p_2>$, where $p_1$ and $p_2$ are the local reasons for each conjunct.

The defence of a disjunction on the other hand gives the choice to **P**, so the strategic reason for a disjunction requires only one local reason.

The defence of an implication can use what **O** had to concede in order to challenge the implication, so the local reason $p_2$ for the consequent depends on the local reason $p_1$.

<footnote n="95">⁹⁵ The table which follows is in fact the dialogical analogue to the *introduction rules* in CTT: dialogically speaking, these rules display the *duties* required by **P**'s assertions—we will come back to this issue in section IX.1.</footnote>
for the antecedent provided by **O**; the strategic reason for the implication thus has the form $p_2^P[[p_1^O]]$.

<table><caption>**Table 24: Synthesis of strategic reasons for P:**</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Move</th><th colspan="2">Synthesis of local reasons</th><th rowspan="2">Synthesis of strategic reasons</th></tr><tr><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Conjunction</th><td>P! A ∧ B</td><td>O?L<sup>^</sup><br>or<br>O?R<sup>^</sup></td><td>P p<sub>1</sub>: A<br>(resp.)<br>P p<sub>2</sub>: B</td><td>P &lt; p<sub>1</sub>, p<sub>2</sub> &gt;: A ∧ B</td></tr><tr><th>Existential quantification</th><td>P!(∃x: A)B(x)</td><td>O?L<sup>∃</sup><br>or<br>O?R<sup>∃</sup></td><td>P p<sub>1</sub>: A<br>(resp.)<br>P p<sub>2</sub>: B(p<sub>1</sub>)</td><td>P &lt; p<sub>1</sub>, p<sub>2</sub> &gt;: (∃x: A)B(x)</td></tr><tr><th>Subset separation</th><td>P!{x: A | B(x)}</td><td>O?L<br>or<br>O?R</td><td>P p<sub>1</sub>: A<br>(resp.)<br>P p<sub>2</sub>: B(p<sub>1</sub>)</td><td>P &lt; p<sub>1</sub>, p<sub>2</sub> &gt;: {x: A | B(x)}</td></tr><tr><th>Disjunction</th><td>P! A ∨ B</td><td>O?<sup>V</sup></td><td>P p<sub>1</sub>: A<br>or<br>P p<sub>2</sub>: B</td><td>P p<sub>1</sub>: A ∨ B<br>or<br>P p<sub>2</sub>: A ∨ B</td></tr><tr><th>Implication</th><td>P! A ⊃ B</td><td>O p<sub>1</sub>: A</td><td>P p<sub>2</sub>: B</td><td>P p<sub>2</sub>P[[p<sub>1</sub><sup>O</sup>]]: A ⊃ B</td></tr><tr><th>Universal quantification</th><td>P!(∀x: A)B(x)</td><td>O p<sub>1</sub>: A</td><td>P p<sub>2</sub>: B(p<sub>1</sub>)</td><td>P p<sub>2</sub>P[[p<sub>1</sub><sup>O</sup>]]: (∀x: A)B(x)</td></tr></tbody></table>

For negation, we must bear in mind that we are considering **P**-strategies, that is, plays in which **P** wins, and we are not providing particle rules with a proper challenge and defence, but we are adopting a strategic perspective on the reason to provide backing a statement; thus the response to an **O**-challenge on a negation cannot be **P**!⊥, which would amount to **P** losing; this statement “$P n^O[[p_1^O]]$: ¬A” indicates that **P**'s strategic reason for the negation is based on **O**'s move *n* (where **O** is forced to state ⊥), move *n* which is dependent upon **O**'s choice $p_1$ as local reason for the antecedent of the negation. This yields the following rule for the synthesis of the strategic reason for negation:

<table><caption>**Table 25: synthesis of the strategic reason for negation**</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th><th>Strategic reason (synthesis)</th></tr></thead><tbody><tr><th>Negation</th><td>P! ¬A<br>Also<br>expressed<br>as<br>P! A ⊃ ⊥</td><td>O p<sub>1</sub>: A</td><td>O!⊥<br><br>P's successful defence of the negation amounts to a switch such that O must now state that she has a local reason for A. However this move leads her to give up by bringing forward ⊥ (*n*)</td><td>P n<sup>O</sup>[[p<sub>1</sub><sup>O</sup>]]: ¬A<br><br>The move O p<sub>1</sub>: A, allows P to force her to give up in move *n*, which leads to P's victory.</td></tr></tbody></table>
$P n^o [[p_1 o]]$: $\neg A$

$(\lambda x)p_2(x): \neg A$

## Dependences

In the case of material implication and universal quantification, a winning P-strategy literally displays the procedure by which the Proponent chooses the local reason for the consequent *depending* on the local reason chosen by the Opponent for the antecedent. What the canonical argumentation form of a strategic object does is to make explicit the relevant *choice-dependence* by means of a *recapitulation* of the plays stemming from the thesis.

This corresponds to the general description of proof-objects for material implications and universally quantified formulas in CTT: a method which, given a proof-object for the antecedent, yields a proof-object for the consequent.

## VII.7.3 Rules for the analysis of P-strategic reasons: Strategic reasons as recapitulations of procedures of analysis and record of instructions

The analysis of P-strategic reasons focuses on this other essential aspect of P's activity while playing: not determining *what* he needs in order to justify his statement—that aspect is dealt with by the synthesis of P-strategic reasons—but determining *how* he will be able to defend his statement through O's statement and through those alone; that is, the analysis of P-strategic reasons are a direct consequence of the Socratic rule: since P must defend his thesis using only the elements provided by O, P must be able to analyze O's statements and find the elements he needs for the justification of his own statements, so as to force O to bring these elements forward during the play.

In this regard, the analysis of strategic reasons constitute both the analogue of the *elimination rules* in CTT and the *equality rules* of a type, to which we now turn.

### Analysis of strategic reasons providing the equalities that will guide P's choices

As explained in chapter II, the *equality rules* for a type A determine the equalities between its elements which are introduced by the evaluation rules for the selector for A (the non-canonical operators that render the proof-objects of elimination rules for that type). Thus in the CTT-setting, the equality rules serve to justify the elimination rules by showing how the evaluation of the selectors (their computation) yield canonical elements of A.

In the dialogical framework, the analysis of strategic reasons renders the instructions (the analogue of selectors) and the equality rules for the resolutions of those instructions in such a way that in a winning strategy the result of the resolution of an instruction for an elementary A (challenged by the Opponent) is a local reason stated by the Opponent.

The strategic reason for the thesis then recapitulates not only the relevant processes of synthesis and analysis but it also includes a record of the resolution of the instructions manifesting how the process of analysis and synthesis intertwine. Accordingly, “recording resolutions” amounts to making explicit the equalities between instructions and the local reasons required by the justification of the thesis.

Since the winning strategies corresponding to CTT-demonstrations are P-winning strategies, the rules for the recapitulation of the procedures of analysis are fixed for O. From the dialogical point of view, the rules corresponding to CTT elimination rules display what P is entitled to state on the basis of O's statements: a P-winning strategy
includes all the **O**-statements brought forward while challenging the thesis. The procedures of analysis leading to a **P**-winning strategy thus prescribe how to analyze the **O**-statements into reasons that can be copied by **P** and that contribute to the justification of **P**'s thesis.

### The case of the strategic reason for disjunction

The most striking example for the analysis of **P**-strategic reasons is probably the case of a **P**-winning strategy based on a disjunction stated by **O**: let us take the case of a **P**-winning strategy for some thesis $\pi$ such that **O** has to defend at some point the disjunction $d: B \lor A$, and such that **P** needs **O** to defend this disjunction in order to win; in this context **P** has a winning strategy for his thesis because he is entitled to defend his own commitments—undertaken while stating the thesis—by analyzing precisely those statements that **O** is forced to concede while defending either side of $B \lor A$.

The rule for the analysis of local reasons for a disjunction states that the defender may choose which local reason to provide supporting the disjunct he chose. Thus if **O** states the disjunction $d: B \lor A$, and **P** challenges this disjunction, then **O** can choose to defend it by stating either $L^V(d)^O: B$ or $R^V(d)^O: A$. So when **P** analyzes **O**'s statement during the play, he must take **O**'s choice into account and track how **O** will resolve the instruction so that **P** can copy that resolution and not the corresponding instruction. The analysis of the **P**-strategic reason for a disjunction has thus the following form:

$$L^V(d)^O = d_1^{P,O} | R^V(d)^O = d_2^{P,O}$$

This strategic reason is constituted of two equalities, the left one being $L^V(d)^O = d_1^{P,O}$ and the right one being $R^V(d)^O = d_2^{P,O}$, separated by a bar $|$ which indicates that it is **O**, not **P**, who has the choice between the two instructions. The equalities state that the instruction used by **O** to defend her disjunction (left or right side) will be resolved into a local reason chosen by **O** ($d_1$ and $d_2$ respectively), local reason that will be copied by **P** in order to support a later claim—$C$ for instance—, the superscripts **P** and **O** indicating that the labelled player brings the local reason ($d_1^P$ for instance) or the instruction ($L^V(d)^O$ for instance) forward in the play. The strategic reason for the thesis will in this respect not only *display the instructions* resulting from the analysis of $d$, but it will also *record the resolution of those instructions* that yield the reasons for the elementary propositions that justify the thesis.

That is, statements of the form $P L^V(d)^O = d_1^{P,O} | R^V(d)^O = d_2^{P,O}: C$ indicate that the strategic reason for $C$ is the outcome of a disjunction stated by **O** such that whatever be the local reason she decides to defend her disjunction with, this reason will provide the strategic reason for **P** to state $C$: if the local reason adduced by **O** in defence of the disjunction is the one that is resolved by the left instruction, and if **O** uses $d_1$ to resolve the left instruction, then **P** will copy that local reason and use $d_1$ in order to defend $C$. The same holds for the right side, *mutatis mutandis*.

It is once again clear that a strategic reason is only a perspective on a statement which is not actually carried out in a play: both sides of the disjunction are taken into account without determining which one will be taken, thus allowing for the indetermination of **O**'s choice.

### The rules of analysis of strategic reasons

Here is the table providing the rules for the analysis of **P**-strategic reasons, in which we also recall the analysis rules for local reasons, so as to make the link between the two as clear as possible. Since the rules for the analysis of strategic reasons will display equalities, we assume that the instructions are resolved into its elementary constituents.
<table><caption>Table 27: analysis rules for P-strategic reasons</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Move</th><th colspan="2">Analysis of local reasons</th><th rowspan="2">Analysis of P-strategic reasons</th></tr><tr><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><td>Conjunction</td><td>O p: A ∧ B</td><td>P ? L<sup>∧</sup><br>or<br>P ? R<sup>∧</sup></td><td>O L<sup>∧</sup>(p)<sup>o</sup>: A<br>(resp.)<br>O R<sup>∧</sup>(p)<sup>o</sup>: B</td><td>P L<sup>∧</sup>(p)<sup>o</sup> = p<sub>1</sub><sup>P,o</sup>: A<br>(resp.)<br>P R<sup>∧</sup>(p)<sup>o</sup> = p<sub>2</sub><sup>P,o</sup>: B</td></tr><tr><td>Existential<br>quantification</td><td>O p: (∃x: A)B(x)</td><td>P ? L<sup>∃</sup><br>or<br>P ? R<sup>∃</sup></td><td>O L<sup>∃</sup>(p)<sup>o</sup>: A<br>(resp.)<br>O R<sup>∃</sup>(p)<sup>o</sup>: B(L<sup>∃</sup>(p)<sup>o</sup>)</td><td>P L<sup>∃</sup>(p)<sup>o</sup> = p<sub>1</sub><sup>P,o</sup>: A<br>(resp.)<br>P R<sup>∃</sup>(p)<sup>o</sup> = p<sub>2</sub><sup>P,o</sup>: B(p<sub>1</sub><sup>P,o</sup>)</td></tr><tr><td>Subset<br>separation</td><td>O p: {x : A | B(x)}</td><td>P ? L<br>or<br>P ? R</td><td>O L<sup>{...}</sup>(p)<sup>o</sup>: A<br>(resp.)<br>O R<sup>∧</sup>(p)<sup>o</sup>: B(L<sup>{...}</sup>(p)<sup>o</sup>)</td><td>P L<sup>{...}</sup>(p)<sup>o</sup> = p<sub>1</sub><sup>P,o</sup>: A<br>(resp.)<br>P R<sup>∧</sup>(p)<sup>o</sup> = p<sub>2</sub><sup>P,o</sup>: B(p<sub>1</sub><sup>P,o</sup>)</td></tr><tr><td>Disjunction</td><td>O p: A ∨ B</td><td>P ?<sup>ν</sup></td><td>O L<sup>ν</sup>(p)<sup>o</sup>: A<br>or<br>O R<sup>ν</sup>(p)<sup>o</sup>: B</td><td>P L<sup>ν</sup>(d)<sup>o</sup> = d<sub>1</sub><sup>P,o</sup>|R<sup>ν</sup>(d)<sup>o</sup> = d<sub>2</sub><sup>P,o</sup>: C</td></tr><tr><td>Implication</td><td>O p: A ⊃ B</td><td>P L<sup>⊂</sup>(p)<sup>P</sup>: A</td><td>O R<sup>⊂</sup>(p)<sup>o</sup>: B</td><td>P R<sup>⊂</sup>(p)<sup>o</sup> = p<sub>2</sub><sup>P,o</sup>[[L<sup>⊂</sup>(p)<sup>P</sup> = p<sub>1</sub><sup>P,o</sup>]]: B</td></tr><tr><td>Universal<br>quantification</td><td>O p: (∀x: A)B(x)</td><td>P L<sup>⊂</sup>(p)<sup>P</sup>: A</td><td>O R<sup>⊂</sup>(p)<sup>o</sup>: B(L<sup>⊂</sup>(p)<sup>P</sup>)</td><td>P R<sup>⊂</sup>(p)<sup>o</sup> = p<sub>2</sub><sup>P,o</sup>[[L<sup>⊂</sup>(p)<sup>P</sup> = p<sub>1</sub><sup>P,o</sup>]]: B(p<sub>1</sub><sup>P,o</sup>)</td></tr><tr><td>Negation</td><td>O p: ¬A<br>Also expressed as<br>O p: A ⊃ ⊥</td><td>P L<sup>¬</sup>(p)<sup>P</sup>: A<br><br>P L<sup>⊂</sup>(p)<sup>P</sup>: A</td><td>O R<sup>¬</sup>(p)<sup>o</sup>: ⊥<br><br>O R<sup>⊂</sup>(p)<sup>o</sup>: ⊥</td><td>P L<sup>¬</sup>(p)<sup>P</sup> = p<sub>1</sub><sup>P,o</sup>: A<br><br>P you<sub>gave up</sub>(n)[[L<sup>⊂</sup>(p)<sup>P</sup> = p<sub>1</sub><sup>P,o</sup>]]: C</td></tr></tbody></table>

Note that the analysis of strategic reasons for negation is divided into two presentations of negation, **O p**: ¬A and **O p**: A ⊃ ⊥, which, at the play level, are governed by SR7 (see p. 115). The first presentation yields **O** stating ⊥, that is giving up, and therefore the play ends with **P** winning without further ado. Thus the strategic reason is constituted by the resolution of the instruction for A with the means provided by **O** (L<sup>¬</sup>(p) = p<sub>1</sub><sup>o</sup>).

The second presentation on the other hand, allows **P** to back any proposition **C** with the local reason 'you<sub>gave up</sub>(n)' once **O** has stated ⊥ at move *n*. Thus the strategic reason for any proposition **C** is constituted by 'you<sub>gave up</sub>(n)', provided that **O** has provided **P** with the means for resolving the instruction L<sup>¬</sup>(p).

## Correspondence between the analysis of strategic reasons and CTT equality and elimination rules

We will not present here the table of correspondences since they can be reconstructed by the reader emulating the table of correspondence for procedures of synthesis. Let us only indicated that:

$$ \mathbf{P} \textit{you}_{gave\ up}(n) \llbracket L^{\neg}(p)^P = p_1^{P,o} \rrbracket : C $$

corresponds to the CTT-elimination-rule for absurdity, that is:

⊥ true
C true

interpreted as the fact that we shall never get an element of $⊥$, defined as the empty $N_0$. More precisely, if $c: N_0$, then the proof-object of $C$ is “$R_0$” understood as an “aborted programme”<fnref n="96" />

$$ \frac{c: N_0}{R_0(c): C(c)}. $$

In this respect the dialogical reading of the abort-operator is that a player gives up, and the reason for the other player to state $C$ is that the antagonist gave up.

## VII.7.4 Examples for building a strategic reason

**First example: $d: (A \land B) \land C$ [c: $A \land (B \land C)$]**

How to build the strategic reason for the thesis $(A \land B) \land C$ [c: $A \land (B \land C)$], that is for $(A \land B) \land C$ provided the initial concessions $c: A \land (B \land C)$?

**Building the strategic reason for the thesis:**

The thesis is a conjunction. In order to have a strategic reason for the thesis, **P** must have a winning strategy: in this case he must win whether the left conjunct or the right is requested when **O** challenges the thesis; in other words, **P** must be able to defend both: the form of the strategic reason will be an ordered pair $(... , ...)$ (see the synthesis of a strategic reason for a conjunction above).

We know **P** has a winning strategy (see the heuristic procedure section VII.6.6); the core can thus be represented in a tree:

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

<footnote n="96">⁹⁶ See (Martin-Löf, 1984, pp. 66-67).</footnote>
To build the strategic reason for the thesis, let us start with the right conjunct, C.
We must look at the end of a branch in the winning strategy where C is the last P-move:
this is move 14 at the outmost right branch; but move 14 defends against O's challenge in
move 13 on the local reason chosen by P for his elementary move 12, which synthesizes
the local reason for the right-hand side of the thesis (challenged move 3). P chose this
local reason because that is the one O herself chose (move 11); this choice dependence is
what the equality move 14 expresses. The strategic reason for the thesis can have this
form (leaving the left-hand side of the conjunction for later):

$$ \langle \dots, R^\wedge(c_2) = c_{2,2} \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

The explicit rendering of the embeddings encoded by $R^\wedge(c_2)$ yields:

$$ \langle \dots, R^\wedge(R^\wedge(c)) = c_{2,2} \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

Let us now explicit the left-hand side of the strategic reason for the conjunction:
since the left side of the thesis is also a conjunction $(A \wedge B)$, the argumentative canonical
form of the strategic reason will also be a pair:

$$ \langle \langle \dots, \dots \rangle, R^\wedge(R^\wedge(c)) = c_{2,2} \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

This pair will be made of the left and the right of $d_1$, the local reason synthesized by P
move 3 for the complex statement $A \wedge B$. Thus the strategic reason will be:

$$ \langle \langle L^\wedge(d_1), R^\wedge(d_1) \rangle, R^\wedge(R^\wedge(c)) = c_{2,2} \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

The outmost left branch of the tree tells us that

$$ L^\wedge(c) = c_1/L^\wedge(d_1) : A, $$

and the middle branch tells us that

$$ L^\wedge(c_2) = c_{2,1} / R^\wedge(d_1) : B $$

and the explicit rendering of the embeddings encoded by $L^\wedge(c_2)$ yields:

$$ L^\wedge(R^\wedge(c)) = c_{2,1} / R^\wedge(d_1) : B $$

So putting it now all together and implementing the substitution of $L^\wedge(d_1)$ and $R^\wedge(d_1)$ we
obtain:

$$ \langle \langle L^\wedge(c) = c_1, L^\wedge(R^\wedge(c)) = c_{2,1} \rangle, R^\wedge(R^\wedge(c)) = c_{2,2} \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

If we do not take into consideration the equalities we obtain the following strategic
reason for the thesis:

$$ \langle \langle L^\wedge(c), L^\wedge(R^\wedge(c)), R^\wedge(R^\wedge(c)) \rangle : (A \wedge B) \wedge C [c: A \wedge (B \wedge C)] $$

**Second example: $(B \wedge A) \supset C$ [$c: (A \wedge B) \supset C$]**

Develop a demonstration of $(B \wedge A) \supset C$, given the global assumption $c : (A \wedge B) \supset C$, out of the strategic core.

**Resolution:** first, we start by displaying the core in the tree presentation (see section VII.6.7 for the heuristical procedure):
<figure><img src="image_24.png" /></figure>

Recapitulation: building the strategic reason for the thesis. The thesis is an implication, so the form of the strategic reason will be

$$ \dots \mathbf{P} \llbracket \dots \mathbf{O} \rrbracket $$

The right-hand side of the strategic reason is what **O** brings forward to back her stating the antecedent of the implication: this is the synthesis of the local reason she has to carry out in order to challenge the thesis, move 3:

$$ \dots \mathbf{P} \llbracket d_1^0 \rrbracket $$

But the antecedent for the implication (the thesis) is a conjunction ($B \land A$), so $d_1$ is a reason for a conjunction, that is, $d_1$ is a pair:

$$ \langle L^{\wedge}(d_1), R^{\wedge}(d_1) \rangle: B \land A $$

With the equalities (moves 5-7 and 9-11) we obtain the analysis of a strategic reason for conjunction:

$$ \langle L^{\wedge}(d_1) = d_{1,1}, R^{\wedge}(d_1) = d_{1,2} \rangle: B \land A $$

This is therefore what **O** entitles **P** to state by challenging his implication (the thesis).

The left-hand side of the strategic reason for the thesis backs the consequent of the implication: **P** has here to play an elementary statement which therefore needs to be grounded in **O**-moves; this is the purpose of the equality move 20. So the form of the strategic reason will be:

$$ (R^{\supset}(c) = c_2)^{\mathbf{P}} \llbracket \langle L^{\wedge}(d_1) = d_{1,1}, R^{\wedge}(d_1) = d_{1,2} \rangle^{\mathbf{O}}: (B \land A) \supset C [c: (A \land B) \supset C] $$

But $R^{\supset}(c)$ depends on **P** stating $L^{\supset}(c): A \land B$ move 12, a conjunction; the strategic reason for it is a pair, and move 14 shows that $L^{\supset}(c) = c_1$ and the two left branches provide the internal structure of $c_1$:

$$ \langle L^{\wedge}(c_1), R^{\wedge}(c_1) \rangle: A \land B $$
The resolution of the instructions and the final equalities provide the structure of
$L^>(c) = c_1:$

$$
\langle L^>(L^>(c))^{\mathbf{P}} \rangle = R^>(d_1)^{\mathbf{P},\mathbf{o}}, R^>(L^>(c))^{\mathbf{P}} = L^>(d_1)^{\mathbf{P},\mathbf{o}} : A \wedge B
$$

So the analysis of the initial concession c: (A ∧ B) ⊃ C yields:

$$
(R^>(c) = c_2)^o \left[ \langle L^>(L^>(c))^{\mathbf{P}} \rangle = R^>(d_1)^{\mathbf{P},o}, R^>(L^>(c))^{\mathbf{P}} = L^>(d_1)^{\mathbf{P},o} \right]
$$

So the strategic reason for the thesis (B ∧ A) ⊃ C [c: (A ∧ B) ⊃ C] becomes:

$$
(R^>(c))^o \left[ \langle L^>(L^>(c)))^P \rangle = R^>(d_1)^{P,o}, R^>(L^>(c)))^P = L^>(d_1)^{P,o} \right] \rangle^P \left[ \langle L^>(d_1), R^>(d_1) \rangle \right]^o
$$
VIII. THE REMARKABLE CASE OF THE AXIOM OF CHOICE<sup>97</sup>

It is rightly said that the principle of set theory known as the *Axiom of Choice* is “probably the most interesting and in spite of its late appearance, the most discussed axiom of mathematics, second only to Euclid’s Axiom of Parallels which was introduced more than two thousand years ago” (Fraenkel, Bar-Hillel, & Levy, 1973).<sup>98</sup>

According to Ernst Zermelo's formulation of 1904, the Axiom of Choice amounts to the claim that, given any family A of non-empty sets, it is possible to select a single element from each member of A. The selection process is carried out by a function *f* with domain in *M*, such that for any non-empty set *M* in A, *f*(*M*) is an element of *M*. The axiom encountered resistance from its very beginnings, and has triggered heated foundational discussions concerning, among others, mathematical existence and the notion of mathematical objects, in particular of mathematical functions. With time however, the foundational and philosophical reluctancees faded and were replaced with a kind of praxis-driven view accepting the Axiom of Choice as a kind of postulate—rather than as an axiom whose truth is manifest—necessary for the practice and development of mathematics.

The foundational discussions around the Axiom of Choice (AC) found an unexpected revival around 1980 when Per Martin-Löf showed that in constructive logic—a logic that does not presuppose the Excluded Middle—the AC in its intensional version is logically valid, and that this logical truth follows naturally (almost trivially) from the constructive meaning of the quantifiers involved. More than being a simple postulate, this form of constructive “evidence” is what makes it a proper *axiom*. As for the extensional version, it can also be proved, though either the Excluded Middle or the unicity of the function must be assumed. Martin-Löf’s proof, for which he was awarded the prestigious Kolmogorov prize, showed that the old discussions were rooted in an even older conceptual problem: the tension there is between *intension* and *extension*.

Jaako Hintikka has in turn tackled the AC with a game-theoretical interpretation<sup>99</sup>—though he did not take Martin-Löf's proof into account, presumably because he was not in favour of the constructivist approaches. As opposed to Hintikka's game-theoretical approach, the *dialogical* take on the AC does not require an unaxiomatizable language such as the one underlying Independent Friendly logic (IF-logic). Hintikka is certainly right in stressing the aptness of the game-theoretical interpretation of the AC, yet we contend that he is mistaken in what concerns the theory of meaning such an interpretation requires. As pointed out by Jovanovic (2013), Hintikka's claim, that a game-theoretical perspective on Zermelo's AC in a first-order logic was perfectly acceptable for Constructivists, has found sound confirmation in the dialogical approach to Constructive Type Theory, albeit no underlying IF-semantics is required in this framework. Ironically, Hintikka's formulation of the AC, fully spelled out, yields Martin-Löf's own CTT-formulation, making it constructivist-friendly after all.

<footnote n="97">⁹⁷ This section is based on (Clerbout & Rahman, 2015) and (Rahman, Clerbout, & Jovanovic, 2015), where we developed a complete demonstation of AC but with a slighty different dialogical setting.</footnote>

<footnote n="98">⁹⁸ See also (Bell, 2009).</footnote>

<footnote n="99">⁹⁹ See for example (Hintikka, 1996b; 2001).</footnote>
By dealing with the case of the AC in dialogues for immanent reasoning, we intend to exhibit the expressive power of this constructivist game-theoretical framework based on equality in action.

Our point in bringing up this case study is thus to show two perks of our framework, dialogues for immanent reasoning:

* first, that it is possible, through the CTT approach, to distinguish at the object-language level the *intensional formulation* of the AC—demonstrable in CTT—and its *extensional formulation*—demonstrable only if it is assumed there is only one choice function. This will be expounded on in a first section (VIII.1).

* Second, that the dialogical formulation of the intensional version of the AC—also called the *Principle of Dependent Choices*—plainly shows how the evidence of its logical truth amounts to developing a winning strategy in which the consequent of the relevant main implication follows from an interactive take on the meaning of the antecedent. This will be in a following section (VIII.2).

The construction of this meaning is relevant to immanent reasoning or equality in action, since it is built out of the interaction of the two players generating dependences between moves according to the choices attached with the embedding of an existential quantifier—defender's choice—within a universal quantifier—challenger's choice. In such a perspective, the logical truth of the Principle of Dependent Choices is rooted in the equality between the reasons grounding the antecedent on the one hand and the reasons grounding the consequent on the other.

## VIII.1 The intensional and extensional versions of the Axiom of Choice

In order to show the expressive power of CTT, and in particular how it allows to exhibit quantifier interdependence at the object-language level, we will present the CTT proof of the Axiom of Choice.

### Zermelo's formulation

The Axiom of Choice (AC) was first introduced by Zermelo (1904) in order to prove Cantor's theorem: every set can be rendered in such a way as to be well ordered. Zermelo gave two formulations of this axiom: one in 1904, and a second one in 1908. The second formulation is relevant for our discussion, since it relates to both Martin-Löf's and the game-theoretical formalization, and is spelled out in the following fashion:

> A set *S* that can be decomposed into a set of disjoint parts *A*, *B*, *C*, ..., each containing at least one element, possesses at least one subset *S*₁ having exactly one element with each of the parts *A*, *B*, *C*, ..., considered.<fnref n="100" /> (Zermelo, 1908b)

The AC immediately attracted a lot of attention and both of its formulations were criticized by constructivists such as René-Louis Baire, Émile Borel, Henri-Léon Lebesgue and Luitzen Egbertus Jan Brouwer. The first objections were related to the non-predicative character of the axiom, for a certain choice function was supposed to exist

<footnote n="100">¹⁰⁰ Cited from the English translation (van Heijenoort, 1967, p. 186). The original is in (Zermelo, 1908a, p. 110)</footnote>
without constructively showing that it does. The axiom however found its way into the ZFC set theory and was finally accepted by the majority of mathematicians because of its usefulness in different branches of mathematics.

**Martin-Löf's proof: separating an extensional and an intensional version**

Martin-Löf's proof of the AC (provided below, p. 150) is produced in a constructive setting (CTT) and brings together two seemingly incompatible perspectives on this axiom, namely

1. Bishop's surprising observation from (1967): A choice function exists in *constructive mathematics*, because a choice is implied by the very meaning of existence; and

2. the proofs by Diaconescu (1975) and by Goodman and Myhill (1978) that the AC implies the Excluded Middle.

These two perspectives seem incompatible because Constructivists do not presuppose the Excluded Middle: Bishop's observation would thus seem to entail the Excluded Middle in a constructive setting if we also accept the second perspective. The solution resides in distinguishing two versions of the AC: an intensional and an extensional version.

In his (2006) paper, Martin-Löf thus shows that there are versions of the AC that are perfectly acceptable for Constructivists, namely those in which the choice function is defined *intensionally*. But in order to be able to formulate the intensional version of the AC, the axiom must be expressed within a CTT-framework. Such a setting allows the extensional and the intensional formulations of the axiom to be compared: we find that it is in fact the *extensional* version of the AC that implies the Excluded Middle, and that Bishop's remark is compatible with the intensional version of the AC.<fnref n="101" />

**Bishop and choice in the meaning of existence**

In harmony with Bishop's remark that the meaning of existence entails a choice, the truth of the AC follows rather naturally in CTT from the meaning of the quantifiers: take for instance the proposition ($\forall x : A) P(x$) where $P(x)$ is of the type proposition (**prop**), provided that $x$ is an element of the set $A$. If the proposition is true in a constructive setting, then there is a proof for it. Such a proof is a function that renders a proof of $P(x)$ for every element $x$ of $A$. Thus Bishop's remark should be understood as follows:

1. since in a constructive setting the truth of a universal quantification amounts to the existence of a proof, and

2. since this proof is a function,

3. then the truth of a universal quantification amounts in a constructive setting to the existence of such a function.

From this CTT characteristic the proof of the AC can be developed quite straightforwardly. If we recall that in the CTT-setting

* the existence of a function from $A$ to $B$ amounts to the existence of a proof-object for the universal *every* $A$ *is* $B$; and that

* the proof of the proposition $B(x)$, existentially quantified over the set $A$, amounts to a pair such that the first element of the pair is an element of $A$ and the second element of the pair is a proof of $B(x)$;

<footnote n="101">¹⁰¹ See for instance this observation of (Martin-Löf, 2006, p. 349): "[...] this is not visible within an extensional framework, like Zermelo-Fraenkel set theory, where all functions are by definition extensional."</footnote>
then a full-fledged formulation of the AC—more precisely, of the *Principle of Dependent Choices* (PDC)—follows, in which we explicit the set over which the existential quantifiers are defined:

**Figure 1: the intensional formulation of the Axiom of Choice:**

$$ (\forall x: A)(\exists y : B(x))C(x, y) \supset (\exists f : (\forall x : A)B(x))(\forall x : A)C(x, f(x)) $$

**Martin-Löf's proof of the intensional version of the Axiom of Choice:**<sup>102</sup>

The usual argument in intuitionistic mathematics, based on the intuitionistic interpretation of the logical constants, is roughly as follows: to prove $(\forall x)(\exists y)C(x, y) \supset (\exists f)(\forall x)C(x, f(x))$, assume that we have a proof of the antecedent. This means we have a method which, applied to an arbitrary $x$, yields a proof of $(\exists y)C(x, y)$. Let $f$ be the method which, to an arbitrarily given $x$, assigns the first component of this pair. Then $C(x, f(x))$ holds for an arbitrary $x$, and hence, so does the consequent. The same idea can be put into symbols getting a formal proof in intuitionistic type theory. Let $A$: set, $B(x)$: set $(x: A)$, $C(x, y)$: set $(x: A, y: B(x))$, and assume $z$: $(\Pi x: A)(\Sigma y: B(x))C(x, y)$. If $x$ is an arbitrary element of $A$, i.e. $x: A$, then by $\Pi$-elimination we obtain

$$ Ap(z, x): (\Sigma y: B(x))C(x, y) $$

We now apply left projection to obtain

$$ p(Ap(z, x)): B(x) $$

and right projection to obtain

$$ q(Ap(z, x)): C(x, p(Ap(z, x))). $$

By $\lambda$-abstraction on $x$ (or $\Pi$-introduction), discharging $x: A$, we have

$$ (\lambda x)p(Ap(z, x)): (\Pi x: A)B(x) $$

and by $\Pi$-equality

$$ Ap((\lambda x)p(Ap(z, x)), x) = p(Ap(z, x)): Bx $$

By substitution<sup>103</sup> we get

$$ C(x, Ap((\lambda x)p(Ap(z, x)), x)) = C(x, p(Ap(z, x)))^{104} $$

and hence by equality of sets

$$ q(Ap(z, x)): C(x, Ap((\lambda x)p(Ap(z, x)), x)) $$

where $(\lambda x)p(Ap(z, x))$ is independent of $x$. By abstraction on $x$

$$ (\lambda x)p(Ap(z, x)): (\Pi x: A)C(x, Ap((\lambda x)p(Ap(z, x)), x)) $$

We now use the rule of pairing (that is $\Sigma$-introduction) to get

$$ ((\lambda x)p(Ap(z, x)), (\lambda x)q(Ap(z, x))): (\Sigma f: (\Pi x: A)B(x))(\Pi x: A)C(x, Ap(f, x)) $$

(note that in the last step, the new variable $f$ is introduced and substituted for $(\lambda x)p(Ap(z, x))$ in the right member). Finally by abstraction on $z$, we obtain

<footnote n="102"><sup>102</sup> For the formal demonstration spelled out as a Natural deduction tree, see (Clerbout & Rahman, 2015, p. 78) and (Rahman, Clerbout, & Jovanovic, 2015, p. 204).</footnote>

<footnote n="103"><sup>103</sup> making use of $C(x, y): \text{set}(x: A, y: B(x))$.</footnote>

<footnote n="104"><sup>104</sup> That is, $C(x, Ap((\lambda x)p(Ap(z, x)), x)) = C(x, p(Ap(z, x))): \text{set}$.</footnote>
$$ (\lambda z) ((\lambda x)p(Ap(z, x)), (\lambda x)q(Ap(z, x))) : (\Pi x: A)(\Sigma y: B(x))C(x, y) \\ \supset (\Sigma f : (\Pi x: A)B(x))(\Pi x: A)C(x, Ap(f, x))^{105} $$

Martin-Löf (2006) further shows that—from a constructive point of view—what is wrong with the AC is the extensional formulation of it, formulation that Hintikka seems to assume and that can be expressed in the following way:

**Figure 2: the extensional version of the Axiom of Choice:**

$$ (\forall x: A)(\exists y : B(x))C(x, y) \supset (\exists f : (\forall x: A)B(x)) (Ext(f) \wedge (\forall x: A)C(x, f(x))) \\ \text{Where } Ext(f) \text{ is defined as } (\forall i, j: A)(i =_A j \rightarrow f(i) = f(j)). $$

Thus, from the constructive point of view, what is really wrong with the classical formulation of the AC is the assumption that from the truth that all of the As are Bs we can obtain a function that satisfies extensionality. In fact, as shown by Martin-Löf (2006), the classical version holds, even constructively, if we assume that there is only one such choice function in the set at stake:

**Figure 3: the constructive extensional formulation of the AC:**

$$ (\forall x: A)(\exists! y : B(x))C(x, y) \supset (\exists f : (\forall x: A)B(x))(\forall x: A)C(x, f(x)) $$

## Conclusion on the two formulations of the AC

Let us retain that if we take

$$ (\forall x : A) (\exists y : B(x) C(x, y) \supset (f : (\forall x : A) B(x)) (\forall x : A) C(x, f(x))) $$

to be the formalization of the AC, or more precisely of the PDC, then that axiom is not only unproblematic for Constructivists but it is also a theorem. In fact, it is the explicit language of CTT that allows a fine-grained distinction between the two formulations of the AC, equivalent only from the outside. This is due to the expressive power of CTT that allows expressing at the object-language level *quantifier interdependence*.

What is more, Hintikka's insight that the validity of the AC results from the fact that a winning strategy for the antecedent amounts to the existence of a suitable function, which seems to sum up the idea behind the demonstration of Martin-Löf<fnref n="106" />, is that what makes apparent the truth of the PDC is the game-theoretical approach to the meaning of the quantifiers. However, despite Hintikka's own developments, it is the dialogical approach to CTT that actually does the job. So now that the usefulness of CTT has been illustrated and the two versions of the AC defined, let us proceed to our second point: showing how the PDC in the framework of dialogues for immanent reasoning explicit the interdependency of the quantifiers through equality in action.

## VIII.2 The Principle of Dependent Choices within dialogues for immanent reasoning<fnref n="107" />

Since dialogues for immanent reasoning is a dialogical framework that incorporates the features of CTT, it is at least as expressive as CTT, and can thus also differentiate between an extensional version of the AC and an intensional version (the PDC). The

<footnote n="105">¹⁰⁵ (Martin-Löf, 1984, pp. 50-51)</footnote>

<footnote n="106">¹⁰⁶ See (Jovanovic, 2013).</footnote>

<footnote n="107">¹⁰⁷ The proof stems from (Clerbout & Rahman, 2015).</footnote>
particle rules provide the meaning of the logical constants; the existential and the universal quantifiers have their meaning determined notably by which player has the choice—the challenger for the universal quantification, the defender for the existential quantification. What is more, the whole structure of dialogues for immanent reasoning rests on this fundamental rule, SR4 or Socratic rule (see section VII.2.1, p. 113), that explicits the dynamics of the choices of the players in interaction: the Proponent will copy the Opponent's choices and reasons in order to provide local reasons for his own statements.

The PDC embeds existential quantification within universal quantification in the antecedent of the implication, and universal quantification within existential quantification in the consequent. In dialogues for immanent reasoning, just like in the standard dialogical framework, demonstrations are obtained by providing a P-strategy (see III.5 and in chapter V.1), that is P must be able to win whatever be O's choices.

<caption>**Figure 4: the thesis for the PDC in dialogues for immanent reasoning:**</caption>

$$ P! (\forall x: A)(\exists y : B(x))C(x, y) \supset (\exists f : (\forall x : A)B(x))(\forall x : A)C(x, f(x)) $$

Since the thesis is stated by **P** and is an implication, **O** will challenge it by stating the antecedent, **P** will be defending it by stating the consequent:

$$ O! (\forall x: A)(\exists y : B(x))C(x, y) $$

$$ P! (\exists f : (\forall x : A)B(x))(\forall x : A)C(x, f(x)) $$

In this fashion, **O** will have to defend the embedding of the existential within the universal, and **P** will have to defend the embedding of the universal within the existential.

In other words, **O** will have to defend the embedding of her choice (defence of the existential) within a **P**-choice (defence of a universal):

$$ O! (\forall x: A)^{\text{P choice}} (\exists y : B(x))^{\text{O choice}} C(x, y) $$

and **P** will have to defend the embedding of an **O**-choice (defence of a universal) within her choice (defence of an existential):

$$ P! (\exists f : (\forall x : A)^{\text{O choice}} B(x))^{\text{P choice}} (\forall x : A)C(x, f(x)) $$

Playing his moves in an optimal fashion will thus allow **P** to ask **O** to choose first and then copy her choices in order to build an equality through interaction and be able to win. The basic idea is that **P** can copy **O**'s choice for y in the antecedent for his defence of $f(x)$ in the consequent since both are equal objects of type $B(x)$, for any $x: A$. Thus a winning strategy for the implication follows simply from the meaning of the antecedent: this meaning is defined by the dependences generated by the interaction of choices involved in the embedding of an existential quantifier within a universal quantifier.

The following two dialogue tables display the relevant plays for building a winning strategy. These two plays are triggered by **O**'s decision-options concerning the existential in the consequent (stated by **P**): she can ask for the left or for the right (move 5), **P** must be able to win in both cases if he is to have a winning strategy.

Here is a reminder of some particle rules of dialogues for immanent reasoning:

<table><caption>**Table 28: recalling the synthesis of local reasons**</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Implication</th><td>X! A ⊃ B</td><td>Y p<sub>1</sub>: A</td><td>X p<sub>2</sub>: B</td></tr></tbody></table>
<table><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>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></table>

We assume by now that the reader is familiar enough with the dialogical framework and with this kind of table presentation; the comments will therefore be more to the point in explaining what is specific to the PDC. Are highlighted the moves where **P** defends his choice of a local reason by stating an equality, the crucial move defining immanent reasoning where **P** says “my reason is the same as yours”.

<table><caption>Play 15: the PDC (left decision-option)</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td>0.1</td><td>C(x, y) : set [x : A, y : B(x)]</td><td colspan="2">! (∀x : A) (∃y : B(x)) C(x,y)</td></tr><tr><td>0.2</td><td>B(x) : set [x : A]</td><td colspan="2">supset (∃f : (∀x : A) B(x)) (∀x : A)</td></tr><tr><td></td><td></td><td colspan="2">C(x, f(x))</td></tr><tr><td>1</td><td>m:= 1</td><td colspan="2">n:= 2</td></tr><tr><td>3</td><td>d<sub>1</sub> : (∀x : A) (∃y : B(x)) C(x, y)</td><td>0</td><td>d<sub>2</sub> : (∃f : (∀x : A) B(x)) (∀x : A)</td></tr><tr><td></td><td></td><td colspan="2">C(x, f(x))</td></tr><tr><td>5</td><td>?<sub>L</sub></td><td>4</td><td>L<sup>∃</sup>(d<sub>2</sub>) : (∀x : A) B(x)</td></tr><tr><td>7</td><td>? --- / L<sup>∃</sup>(d<sub>2</sub>)</td><td>6</td><td>g<sub>1</sub> : (∀x : A) B(x)</td></tr><tr><td>9</td><td>L<sup>∀</sup>(g<sub>1</sub>) : A</td><td>8</td><td>R<sup>∀</sup>(g<sub>1</sub>) : B(a)</td></tr><tr><td>11</td><td>a : A</td><td>13</td><td>? --- / L<sup>∀</sup>(g<sub>1</sub>)</td></tr><tr><td>17</td><td>R<sup>∀</sup>(d<sub>1</sub>) : (∃y : B(a)) C(a, y)</td><td>3</td><td>L<sup>∀</sup>(d<sub>1</sub>) : A</td></tr><tr><td>13</td><td>? --- / L<sup>∀</sup>(d<sub>1</sub>)</td><td>12</td><td>a : A</td></tr><tr><td>15</td><td>? = a</td><td>14</td><td>L<sup>∀</sup>(g<sub>1</sub>) = a : A</td></tr><tr><td>19</td><td>v : (∃y : B(a)) C(a, y)</td><td>17</td><td>? --- / R<sup>∀</sup>(d<sub>1</sub>)</td></tr><tr><td>21</td><td>L<sup>∃</sup>(v) : B(a)</td><td>19</td><td>?<sub>L</sub></td></tr><tr><td>23</td><td>v<sub>1</sub> : B(a)</td><td>21</td><td>? --- / L<sup>∃</sup>(v)</td></tr><tr><td>25</td><td>? --- / R<sup>∀</sup>(g<sub>1</sub>)</td><td>24</td><td>v<sub>1</sub> : B(a)</td></tr><tr><td>27</td><td>? = v<sub>1</sub></td><td>26</td><td>L<sup>∃</sup>(v) = v<sub>1</sub> : B(a)</td></tr><tr><td>29</td><td>? = a<sup>B(a)</sup></td><td>28</td><td>L<sup>∀</sup>(g<sub>1</sub>) = a : A</td></tr><tr><td>31</td><td>? = B(a)</td><td>30</td><td>! B(L<sup>∀</sup>(g<sub>1</sub>)) = B(a) : set</td></tr><tr><td>33</td><td>! B(a) : set</td><td>0.2<br>Subst-D</td><td>a : A</td></tr></tbody></table>

**Commentary:**

* **Move 3:** Once the thesis has been stated and the repetition ranks established, **O** challenges the material implication by stating the left component.

* **Move 4:** **P** states the right component of the material implication.

* **Moves 5 and 6:** **O** has here the choice between asking for the left or for the right component of the existential. The present play describes the development of the play triggered by the left choice.

* **Moves 7-13** follow from a straightforward application of the dialogical rules.

* **Move 15:** **O** asks for the local reason that corresponds to the instruction stated by **P** at move 14.
* **Move 16: P** answers by recalling that **O** used the same reason, namely *a*, in defence of the claim that **A** holds (that it is not empty). And indeed this is what **O** did when she resolved $L^\nabla(g_1)$ with *a*. This led **P** to implement the Socratic rule and state the equality $L^\nabla(g_1) = a : A$.

* **Moves 27-28 and 29-30:** deal with the same kind of situation.

* **Moves 30-31:** Once move 30 has established that *a*—occurring in $B(a)$—constitutes a local reason for holding **A**, according to the Socratic rule S4.1c, **O** can launch an attack requesting **P** to show that $B(a)$ and $B(L^\nabla(g_1))$ are equal propositions.

* **Moves 32-34:** **P** applies the rule for substitution within dependent statements (Subst-D) on the first concession, forcing **O** to state the condition that allows **P** to answer to the attack of move 31 and win the play by applying the Socratic rule to **O**'s move 25.

Notice that when **P** attacks **O**'s initial concession 0.2 he has to state *a : A* (move 32); according to the provisos of the Socratic rule however (see SR4.1, p. 114), **O** cannot attack this statement again: move 16 establishes **P**'s right to state this equality.

Let us now develop the second play, in which **O** went for the right decision-option at move 5.

<table><caption>**Play 16: the PDC (right decision-option)**</caption><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>0.1</td><td>C(x, y) : set [x : A, y : B(x)]</td><td></td><td>! (∀x : A) (∃y : B(x)) C(x, y) ⊃ (∃f : (∀x : A) B(x)) (∀x : A) C(x, f(x))</td><td>0</td></tr><tr><td>0.2</td><td>B(x) : set [x : A]</td><td></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>d<sub>1</sub> : (∀x : A) (∃y : B(x)) C(x, y)</td><td>0</td><td>d<sub>2</sub> : (∃f : (∀x : A) B(x)) (∀x : A) C(x, f(x))</td><td>4</td></tr><tr><td>5</td><td>?<sub>R</sub></td><td>4</td><td>R<sup>3</sup>(d<sub>2</sub>) : (∀x : A) C(x, L<sup>3</sup>(d<sub>2</sub>)(x))</td><td>6</td></tr><tr><td>7</td><td>? --- / R<sup>3</sup>(d<sub>2</sub>)</td><td>6</td><td>g<sub>2</sub> : (∀x : A) C(x, g<sub>1</sub>(x))</td><td>8</td></tr><tr><td>9</td><td>L<sup>3</sup>(g<sub>2</sub>) : A</td><td>8</td><td>R<sup>3</sup>(g<sub>2</sub>) : C(x, g<sub>1</sub>(a))</td><td>30</td></tr><tr><td>11</td><td>a : A</td><td>11</td><td>? --- / L<sup>3</sup>(g<sub>2</sub>)</td><td>10</td></tr><tr><td>17</td><td>R<sup>3</sup>(d<sub>1</sub>) : (∃y : B(a)) C(a, y)</td><td>3</td><td>L<sup>3</sup>(d<sub>1</sub>) : A</td><td>12</td></tr><tr><td>13</td><td>? --- / L<sup>3</sup>(d<sub>1</sub>)</td><td>12</td><td>a : A</td><td>14</td></tr><tr><td>15</td><td>? = a</td><td>16</td><td>! L<sup>3</sup>(g<sub>2</sub>) = a : A</td><td>16</td></tr><tr><td>19</td><td>v : (∃y : B(a)) C(a, y)</td><td>17</td><td>? --- / R<sup>3</sup>(d<sub>1</sub>)</td><td>18</td></tr><tr><td>21</td><td>L<sup>3</sup>(v) : B(a)</td><td>19</td><td>?<sub>L</sub></td><td>20</td></tr><tr><td>23</td><td>t<sub>1</sub> : B(a)</td><td>21</td><td>? --- / L<sup>3</sup>(v)</td><td>22</td></tr><tr><td>25</td><td>R<sup>3</sup>(v) : C(a, L<sup>3</sup>(v))</td><td>19</td><td>?<sub>R</sub></td><td>24</td></tr><tr><td>27</td><td>R<sup>3</sup>(v) : C(a, t<sub>1</sub>)</td><td>25</td><td>? t<sub>1</sub> / L<sup>3</sup>(v)</td><td>26</td></tr><tr><td>29</td><td>t<sub>2</sub> : C(a, t<sub>1</sub>)</td><td>27</td><td>? --- / R<sup>3</sup>(v<sub>2</sub>)</td><td>28</td></tr><tr><td>31</td><td>? --- / R<sup>3</sup>(g<sub>2</sub>)</td><td>30</td><td>t<sub>2</sub> : C(a, g<sub>1</sub>(a))</td><td>32</td></tr><tr><td>33</td><td>? --- / g<sub>1</sub>(a)</td><td>32</td><td>t<sub>2</sub> : C(a, t<sub>1</sub>)</td><td>34</td></tr><tr><td>35</td><td>? = t<sub>2</sub></td><td>34</td><td>R<sup>3</sup>(v) = t<sub>2</sub> : C(a, t<sub>1</sub>)</td><td>36</td></tr><tr><td>37</td><td>? = a<sup>C(a, t<sub>1</sub>)</sup></td><td>36</td><td>L<sup>3</sup>(v) = t<sub>1</sub> : B(a)</td><td>38</td></tr><tr><td>39</td><td>? = C(a, t<sub>1</sub>)</td><td>38</td><td>C(a, L<sup>3</sup>(v)) = C(a, t<sub>1</sub>) : set</td><td>44</td></tr><tr><td>41</td><td>C(a, y) : set [y : B(x)]</td><td>0.1<br>Subst-D</td><td>a : A</td><td>40</td></tr></tbody></table>
<table><tr><td>43</td><td>C(a, t<sub>1</sub>) : set</td><td>41<br/>Subst-D</td><td>42</td></tr></table>

**Remark:** This procedure differs from the one in the previous play only with moves 40 and 44: since $C(x, y)$ is a dyadic predicate, **P** must apply substitution twice before obtaining of **O** the right to state the winning equality at move 44.

Since **P** has a way of winning regardless of **O**'s choices, that is he can win in any case, **P** has a winning strategy for the PDC.

## Conclusion on the Axiom of Choice

From the constructive point of view, functions are rules of correspondence. Rules of correspondence only make sense if we know how the correspondences are to be carried out. From the dialogical (and more generally from the game theoretical) point of view a function is the result of a player choosing an object of the domain and the defender choosing the suitable match, which can be seen as carrying out a rule of correspondence. Intensional functions however cannot be directly produced from these interactions, though extensionality is also brought forward by interaction. Moreover, the dialogical take on constructivism is strongly linked to the view that in order to understand a play, and a winning strategy constituted by the relevant plays, it is not enough to know the rules of the game; it is not even enough to believe that there is a winning strategy behind the moves: what we need is to be able to describe the moves in such a way that it makes their contribution to the winning strategy understandable, that is, how the content involved in each move constitutes that strategy; in other words, a proof which would be beyond our description capacities would not produce knowledge at all. This is what Hintikka's use of Wittgenstein's notion of *human-playable games* amounts to in his (2001) work; it is what the dialogical demonstration of the PDC amounts to.<fnref n="108" />

Let us conclude by quoting some beautiful lines of Poincaré, his response to what he considered a purely "formalistic" approach to mathematics:

> Si vous assistez à un partie d'échecs, il ne vous suffira pas, pour comprendre la partie, de savoir les règles de la marche des pièces. Cela vous permettrait seulement de reconnaître que chaque coup a été joué conformément à ces règles et cet avantage aurait vraiment bien peu de prix. C'est pourtant ce que ferait le lecteur d'un livre de Mathématiques, s'il n'était que logicien. Comprendre la partie, c'est tout autre chose ; c'est savoir pourquoi le joueur avance telle pièce plutôt que telle autre qu'il aurait pu faire mouvoir sans violer les règles du jeu. C'est apercevoir la raison intime qui fait de cette série de coups successifs une sorte de tout organisé. À plus forte raison, cette faculté est-elle nécessaire au joueur lui-même, c'est-à-dire à l'inventeur. (Poincaré, La valeur de la science, 1905, p. 27).<fnref n="109" />

<footnote n="108">¹⁰⁸ See section XI.1 for further details on game definiteness and its crucial role in the dialogical framework.</footnote>

<footnote n="109">¹⁰⁹ "If you are present at a game of chess, it will not suffice, for the understanding of the game, to know the rules for moving the pieces. That will only enable you to recognize that each move has been made conformably to these rules, and this knowledge will truly have very little value. Yet this is what the reader of a book on mathematics would do if he were a logician only. To understand the game is wholly another matter; it is to know why the player moves this piece rather than that other which he could have moved without breaking the rules of the game. It is to perceive the inward reason which makes of this series of successive moves a sort of organized whole. This faculty is still more necessary for the player himself, that is, for the inventor." (Poincaré, 1907, p. 22).</footnote>
# IX. FROM DIALOGICAL STRATEGIES TO CTT-DEMONSTRATIONS AND BACK

## IX.1 General transformation principles between CTT and immanent reasoning

In a nutshell, we take from (Rahman, Clerbout, & Keiff, 2009) the following two correspondences within a P-winning strategy, provided some exceptions to be discussed below:

1. The result of applying a particle rule to a P-move corresponds to the application of an introduction rule of a CTT-demonstration rule (provided we read the P-moves “bottom-up”).

<table><caption>Table 29: correspondence between dialogical rules on P-moves and introduction rules</caption><thead><tr><td>APPLICATION OF A DIALOGICAL RULE TO A P-</td><td>CORRESPONDS IN CTT TO THE INTRODUCTION RULE FOR</td></tr></thead><tbody><tr><td>disjunction</td><td>disjunction</td></tr><tr><td>conjunction</td><td>conjunction</td></tr><tr><td>existential</td><td>existential</td></tr><tr><td>subset separation</td><td>subset separation</td></tr><tr><td>implication</td><td>implication</td></tr><tr><td>universal</td><td>universal</td></tr></tbody></table>

2. The result of applying a particle-rule to an O-move corresponds to the application of an elimination rule of a CTT-demonstration.

<table><caption>Table 30: correspondence between dialogical rules on O-moves and elimination rules</caption><thead><tr><td>APPLICATION OF A DIALOGICAL RULE TO AN O-</td><td>CORRESPONDS IN CTT TO THE ELIMINATION RULE FOR</td></tr></thead><tbody><tr><td>disjunction<br>(may be related to a case-dependent P-statement)</td><td>disjunction</td></tr><tr><td>conjunction</td><td>conjunction</td></tr><tr><td>existential</td><td>existential</td></tr><tr><td>subset separation</td><td>subset separation</td></tr><tr><td>implication</td><td>implication</td></tr><tr><td>universal</td><td>universal</td></tr></tbody></table>

Notice that from the perspective of a P-winning strategy, challenges and defences of P-statements on the one hand are *duties*, which can be understood as what P must bring forward in order to develop a dialogical demonstration for a given particle rule; but challenges and defences on O-statements, on the other hand, can be understood as what P is *entitled* to.<fnref n="110" /> If *duties* (or *commitments*) are understood as the normative force involved by the deployment of introduction rules of a CTT-framework, and *entitlements* as the normative force involved by the deployment of elimination rules of a CTT-

<footnote n="110">¹¹⁰ See the introduction, section I.2.3.</footnote>
framework, then the correspondence between CTT rules and dialogical rules follows naturally.

## Exceptions to the general correspondence

The exceptions to the general principle that **P**-statements correspond to introduction rules and **O**-statements to elimination rules are the following:

### **P**-statements depending upon **O** ⊥ moves correspond to ⊥-eliminations

When **P** makes a statement (elementary or not) adducing the local reason *you*<sub>*gave up*</sub>(*n*) after **O** has previously stated ⊥—the **P**-statement results of applying the elimination rule for ⊥.

### **P**-elementary statements defended with *I* = *p*<sub>*i*</sub>: *type* correspond to definitional equalities

If an elementary **P**-statement has been challenged and defended with a statement of the form *I* = *p*<sub>*i*</sub>: *type*—“*I*” standing for an instruction and “*p*<sub>*i*</sub>” for a local reason—the algorithm presented in this chapter which transforms dialogical strategies into CTT demonstrations (and reversewise), will first introduce in the demonstration tree this equality as the application of a definitional equality, and will remove the **P**-elementary statement that triggered the defence. So the algorithm first inserts the equality then eliminates it.

Dialogical plays use profusely definitional equalities. In fact, in the context of immanent reasoning every use of a move based on the Socratic rule is based on such form of equality. Yet, the natural deduction demonstrations that are not in normal form do not in general require coming back to the equality backing the coordination of introduction and elimination rules.

Within the standard Natural deduction setting Π- and Σ-equalities are made explicit when eliminations introduce non-canonical proof-objects. In the dialogical setting this corresponds to the cases in which **P** chooses a resolution of an instruction (or function) that mirrors the resolution of an *embedded* instruction (or function) occurring already either in the initial concession or in the main thesis.

Let us call the resulting equalities *anaphoric-based equalities* (for short *A-equalities*). Thus, we will only retain in the tree A-equalities. Strictly speaking, plays within the core are carried out in “normal form”.

### **P**-statements which are case-dependent of **O**-statements set the conditions that allow drawing the conclusion of a disjunction elimination rule

In fact, case-dependent **P**-statements correspond to either one of the disjunction eliminations achieved by introductions that follow from stating each of the components of the disjunction.<fnref n="111" />

### Applications of the Statement-Substitution rule

They correspond to substitutions on hypotheticals occurring as global assumptions (initial concessions by **O**).

<footnote n="111">¹¹¹ See section VII.7.3 on the argumentation form of a strategic object, in which we explicitly discuss the case of the disjunction (p. 141).</footnote>
**Transmission of Equality**

The transmission rules for definitional equality will be introduced unmodified in the demonstration tree with their direct CTT counterpart no matter whether they have been applied to **P**-moves or to **O**-moves.

**IX.2 Terminology**

Let recall some terminology from previous sections and introduce some new ones.

**Concessions**

A *concession* is either:

(a) a move that **O** conceded as conditioning the claim of the thesis. We call this also *initial concession*. It corresponds to the notion of *global assumption* of proof-theory including *epistemic assumptions* and premises.

(b) any other **O**-move brought forward during the development of a play, while challenging a **P**-implication or a **P**-universal, or while defending an **O**-disjunction or subset separation. We call this also *local concession*. It corresponds to the notion of *local assumption* of proof-theory.

**Nodes**

*Nodes descending from a statement:* for a statement $\pi$ occurring in the dialogical core C, the nodes *descending from* $\pi$ are all the nodes which are related to $\pi$ by a chain of applications of dialogical rules.

**Branches**

*Left and right branches:* when the dialogical core (or the demonstration) we are building splits, we speak of the *left* and *right branches of the core* (or demonstration). We may sometimes assign an order on the branches from left to right and speak of the first branch, second branch, etc.

**Dependent moves**

*Dependent moves:* a move *M* depends on the move *M'* if there is a chain of applications of game rules that leads from *M'* to *M*.

**Case-dependent move**

Let $\pi$ be some statement and $p$ some local reason. We say that in the core C the move $M_j \mathbf{P}! \pi$ is *case-dependent upon* move $M_{i<j} \mathbf{O}! p : \phi$ if $\phi$ is a disjunction and move $M_j$ depends upon move $M_{i<j}$.

More precisely the move $\mathbf{P}!\pi$ is *case-dependent upon O's* disjunction $\phi$ iff the local reason(s) that occur in the defence of $\mathbf{P}$'s move $\pi$ is definitionally equal to one of the instructions for $\phi$ or if $\mathbf{P}$ is dispensed to defend $\pi$ by $\mathbf{O}$'s move $\perp$ which results from the defence of $\phi$.

As we will discuss below, the point in distinguishing case-dependent moves is that these moves set—from the strategic point of view—the conditions for the conclusion of a disjunction elimination rule.

**A-equalities**

A-equalities are anaphoric-based equalities, which are built when **P** chooses a resolution of an instruction (or function) that mirrors the resolution of an *embedded*
instruction (or function) occurring already either in the initial concession or in the main thesis. See above, section IX.1.

# IX.3 Part 1: from strategies to CTT demonstrations

## IX.3.1 Extracting the core

We start by a method for extracting the parts of a winning strategy relevant for making it correspond to a demonstration in natural deduction; we call it the core of a winning strategy—or, simply, the core (see sections V.2 and VII.5).

In order to extract the core, we develop a method in order to

1. extract the finite part of a winning strategy;

2. disregard the formation rules involving the non-logical constants (since we are dealing with logical inferences);

3. disregard different orders of moves of the Opponent.

Once this has been achieved, we will describe the algorithm allowing us to transform the core into a CTT-demonstration. And finally we will prove the adequacy of the algorithm.

The rationale behind the operation of extracting the core is the following: because $S^*$ is the extensive form of a P-winning strategy, we know that P wins in every branch, so that to some extent which local reasons O chooses for the instructions does not matter.

Let us take as example the case of a universal quantification stated by P. Since we assume that P has a winning strategy, he has a method to successfully defend his statement no matter which local reason O chooses for $L^\nabla(p) : A$ (where A is a set). This yields a natural deduction description of the Introduction rule for universal quantification with an implicit interlocutor: whatever O brings forward as proof-object for the antecedent P has a method to transform it into a proof-object of the consequent. Hence, it is harmless to keep only one *representative* of the possible choices by O because the existence of a winning P-strategy ensures that there is indeed a successful method for every possible O-choice.

## IX.3.2 General procedure and EPI

The next step is to apply transformations to this core until we obtain a CTT demonstration.<fnref n="112" />

The transformation algorithm will *re-write* the tree that represents the core C of the strategy by means of a step-by-step procedure specified below. One important issue is that the re-writing procedure will ignore the following:

* The players' identities.

* The moves where the choices of the repetition ranks are made explicit.

* Questions. Strictly speaking, only statements will be incorporated in the demonstration resulting from the translation algorithm. Thus, questions will not be re-written as separate step; they however have an important role in the transformation-procedure, which will be described below.

<footnote n="112">¹¹² The section strongly relies on (Clerbout & Rahman, 2015), implementing in the CTT-framework the ideas developed in (Rahman, Clerbout, & Keiff, 2009) and (Clerbout, 2014a; 2014b) in the standard framework for FOL.</footnote>
Thus, important information will appear to be lost during the transformation procedure, though actually the procedure is only making it implicit : the other direction of the transformation (from CTT demonstrations to strategies) will show how to bring this information back, showing that dialogues for immanent reasoning make explicit what is implicit in a CTT demonstration.

**Remarks:**

1. We adopt here the natural deduction style of demonstrations used by Martin-Löf rather than the turnstile notation deployed in the introductory chapter on CTT.

2. The dialogical demonstrations will assume that if there are initial concessions, they have already been granted by the Opponent.

**EPI: Resolution and Substitution of Instructions (SR3-4)**

The operation we describe hereafter consists in replacing the challenged instruction with the local reason (chosen as response to the challenge) while placing move *n* in the demonstration under way, and ignoring those equalities that are not *A*-equalities.<fnref n="113" />

One of the cases for which it is important that the algorithm does not ignore the question mark ‘?’ is the application of the structural rules SR3-4 (see section VII.2.1) allowing the resolution and substitution of instructions by local reasons. The algorithm described below takes them into account through the following operation which we shall refer as *Endowing local reasons to Instructions* (EPI):

**EPI operation: Endowing local reasons to Instructions**

Assume that some instruction occurs in move number *n*.

1. Scan the core C: if move *n* is challenged by a question of the form “? --- /”, or “? - π-/” or “?I/p” for some instruction *I* and some local reason *p*, then scan C in search for the defence.

2. Write the replacement-process in the following way (only once): the instruction at the bottom and the resolution on the top, *without the request*.

3. Once such a replacement has been carried out it will be systematically implemented in every further stage of the construction of the demonstration.

The EPI operation ensures that equalities which stem from the resolution of non-embedded instructions will be taken into account during the procedure. Recall that the operation is not necessary for the so-called *A*-equalities—which correspond to resolutions of embedded instructions—because the algorithm already accounts for them as definitional equalities (as explained above, section IX.1, and described in details in step B.2.b of the algorithm).

**Remark**

The distinction between resolutions of non-embedded instructions and *A*-equalities is a technical by-product of the conceptual work on equalities and on immanent reasoning carried out in the present study, and which was not fully grasped in (Clerbout & Rahman, 2015); one consequence of this distinction is that the EPI operation will not, in general,

<footnote n="113">¹¹³ However, as specified below, the equalities that are not deployed in the demonstration tree are nevertheless useful at the strategic level in order to find out the justification of elementary P-statements.</footnote>
need to be applied as much as it was in (Clerbout & Rahman, 2015). Thus the present version of the algorithm is more precise when it comes to account for definitional equalities when building CTT demonstrations out of dialogical winning strategies.

### IX.3.3 The algorithm

The procedure we describe hereafter is a kind of rearrangement of (some of) the nodes in C which eventually produces a CTT demonstration. For convenience we assume that we have an unmodified “copy” of C to which we can refer to while the procedure goes on. The last stage (D) of the procedure requires some explanation: we provide it after the procedure.

#### Step A. Initial stage: placing the conclusion and premises.

Let $\pi$ be the thesis stated by P and $\gamma_1, \dots, \gamma_n$ be the initial concessions by O, if any. Place $\pi$ as the conclusion of the demonstration under construction and $\gamma_1, \dots, \gamma_n$ as its upmost premises:<fnref n="114" />

$$ \begin{array}{c} \gamma_1, \dots, \gamma_n \\ \vdots \\ \pi \end{array} $$

Then go to step B.

#### Step B.

Consider the lowest expression $\pi_i$ just added in the branch of the demonstration tree under construction (in the first stage it will be the thesis).

Find the move in the core C that responds to it (in the first stage of the procedure it will be a challenge of the thesis).

Scan C in order to identify the challenge and the defence resulting from the application of the particle rule relevant to this expression. Then:

##### B.0. EPI-operation

If applicable, implement the EPI-operation to the expressions present in what we have so far in the branch of the demonstration; that is, replace instructions by local reasons, place within the demonstration the equalities used either for statement-substitutions or substitutions involving instructions.<fnref n="115" /> Recall that the EPI does not need to be applied to A-equalities (these are dealt with in step B.2.b).

##### B.1. Moving to step C

If the relevant challenge and defence have already been accounted for in the branch being constructed, then go to C. Otherwise go to B.2.

##### B.2. Accounting for the relevant challenge and defence

If the defence is a P-elementary expression, apply stage B.2.a. Otherwise, implement step B.2.b.

<footnote n="114">¹¹⁴ According to the above Remark 2, we ignore the first steps of a dialogue where the initial assumptions (if any) of the thesis are written to the right of the thesis, and start the algorithm assuming straightaway that the initial concessions have already been settled and the thesis displays the local reason that resulted after O stated the initial concessions.</footnote>

<footnote n="115">¹¹⁵ Ramifications will be dealt with further on in the algorithm.</footnote>
### B.2.a. P-elementary expressions

The present step concerns occurrences of **P**-elementary expressions $\pi_i$ in the core that *are not* dependent upon an **O** $\perp$-move.

Place $\pi_i$ in the demonstration, draw an inference line above it and label it SR (short for the application of some form of the Socratic rule, as defined in rule SR5).

If the corresponding **O**-move (that allowed **P** to state $\pi_i$) has already been accounted for in the branch, then rearrange it so that it is placed as the premiss of the application of the rule. Find the **O**-move by searching for the relevant equality. All of the equalities in the core will indicate precisely the **O**-move relevant for the elementary expression at stake.

Go back to **B**.

### B.2.b. Other expressions

The present step concerns non **P**-elementary expressions $\pi_i$.

Draw an inference line above $\pi_i$ and label it with the relevant name of the rule.

Place the defence—and the challenge, if relevant<sup>116</sup>—as the premiss (or premisses) for the application of the rule, according to the following conventions:

1. In the cases of the Introduction rule for implication, negation, or universal quantification, the defence is the immediate premiss and the challenge is placed upwards as an assumption such that:

i. the defence depends on that assumption,

ii. the assumption is numbered and marked as discharged at the inference step, and

iii. the assumption is still in the scope of previously placed assumptions such as the premisses of the demonstration placed in stage **A**.

2. Here we apply the correspondences (given above) between player-moves and natural deduction steps in the following way:<sup>117</sup>

i. If $\pi_i$ is an **O**-implication move, we are facing an elimination rule: the premiss is constituted by that move and its challenge. The conclusion is the defence. Similarly for negations and universals.

ii. If $\pi_i$ is a **P**-conjunction or a **P**-existential move, we are dealing with an introduction rule: each premiss is constituted by one of the defences. The conclusion is the challenged conjunction or existential.

Dually, if $\pi_i$ is an **O**-conjunction or an **O**-existential move, we are in presence of an elimination-rule, so that $\pi_i$ is the premiss of each of the inferences with each of the defences as conclusion.

iii. If $\pi_i$ is a case-dependent **P**-statement, then rewrite each of the **O**-defences of the relevant disjunction as a local assumption upon which a copy of $\pi_i$ will be made dependent. Draw an inference line and copy below a third copy of the case-dependent statement $\pi_i$.

<footnote n="116"><sup>116</sup> That is, when the particle rule applied is a challenge to an implication, a negation, or a universal.</footnote>

<footnote n="117"><sup>117</sup> Recall that those moves in C have the form of defences and challenges established by the particle rules or structural rules.</footnote>
iv. If $\pi_i$ is an **O**-elementary statement, it is either initial concessions or the result of an elimination rule, in which case draw an inference line above $\pi_1$ and place the relevant move as premiss (see Table 29 and Table 30 above).

v. If $\pi_i$ is a **P**-statement (elementary or not) that does not need to be defended because **O** stated $\perp$ (allowing **P** to adduce the local reason $you_{gave up}(n)$ for $\pi_i$), then it corresponds to the application of an elimination rule for $\perp$. In such a case, scan for the move $\perp$, place it in the demonstration as a premiss of a $\perp$-elimination, draw an inference line and write $\pi_i$ below it. If $\pi_i$ is either an implication or a universal delete the **O**-challenge to it.

vi. If $\pi_i$ is a **P**-statement that displays an **A**-equality, place it in the demonstration as the conclusion of a $\Sigma$-($\Pi$-)equality-rule with the moves that lead to that equality as a premiss.<fnref n="118" />

vii. If $\pi_i$ is a substitution-move based on an **A**-equality, place that equality and the expression in which the substitution has been carried out as premiss of the application of a substitution rule. Similarly for statement-substitution moves.

viii. Apply the EPI operation to the newly added expressions (if applicable). Move to the first (starting from the left) newly opened branch if relevant and go back to **B**.

At this stage multiple premises can occur. Those premises are not dependent upon one another (with the exception of the premises of the elimination of a disjunction) and are placed on the same level: each one opening a new branch in the demonstration. In such cases all the premisses that were placed at some previous step in the translation must be copied and pasted for each newly opened branch.

**Step C.**

If the situation is the one of **B.1** and no new expression has been added to the branch under construction, then:

**C.1. Rearrangements**

Perform any rearrangement required to match the notational convention of natural deduction trees and go to **C.2**.

**C.2. Dealing with SR**

If the branch does not feature applications of SR then go to **C.3**. Otherwise for each application of SR in the branch, remove its conclusion and the associated inference line.<fnref n="119" /> Go to **C.3**.

<footnote n="118">¹¹⁸ Recall the remarks above (section IX.1, ‘Exceptions’) concerning **P**-elementary statements defended with $I = p_i : type$.</footnote>

<footnote n="119">¹¹⁹ SR-rules display two copies of the same elementary expression, one as premise and one as conclusion. In the standard presentation of natural deduction (used in the present text) this is not necessary, unless we make use of some other recent presentations of natural deductions that introduce explicitly axioms of the form $A \vdash A$.</footnote>
**C.3. Moving in the algorithm**

Move to the next branch to which stages C.1 and C.2 has not yet been applied and
go back to B.

If there are no such branches left, go to D.

**Step D. Inserting proof-objects and stopping the procedure.**

Going from top to bottom, replace in the demonstration at hand the dialogical local
reasons with CTT proof-objects in accordance with the CTT rules. The point is that once
the demonstration has been built we do not have local reasons any more but strategic
objects—the latter but not the former correspond to proof-objects.

Then stop the procedure.

**Checking method**

The table of correspondences between strategic objects and proof-objects
 subsection IX.1) can be used as checking method using the following steps:

Extract the strategic object of the thesis from the core. Use the correspondences of
the table and provide the proof-object for it. Compare with the result of the procedure.

**Remarks:**

We have designed the algorithm so that the branches in the demonstration under
construction are dealt with sequentially. However, it is possible to process them all at the
same time in parallel.

The concluding stage D is necessary because, as discussed all over our study (see
for instance section VII.5), dialogical local reasons differ from CTT proof-objects, which
correspond to strategic reasons.

**IX.3.4 Adequacy of the translation algorithm**

We must ensure that the algorithm is adequate: given the core of a winning P-
strategy it must always yield a CTT demonstration. Let us first describe the general idea
behind the demonstration, that in fact is an almost literal reproduction of the one
developed in (Clerbout & Rahman, 2015, pp. 49-52), with small changes due to the
present take on equalities.

The translation procedure ultimately consists in rearranging the nodes of the original
dialogical core C. We must ensure that the reordering results in a derivation which
complies with the CTT rules. We noticed that during this reordering, the procedure
introduces what we may call “gaps” which we have marked with vertical dots. Take for
example the first step of such a transformation procedure. In this step the thesis of the core
provides the conclusion of the demonstration and the concessions provide the
assumptions, though we still do not know at this point of the process what corresponds to
the steps between the assumptions and the conclusion. Accordingly, we start by simply
linking the assumptions and the conclusion with vertical dots. The idea behind the
adequacy of the algorithm is that all these gaps will eventually be filled and that it will be
done in a way which observes the CTT rules.

The last part of this statement is easily checked. Let us assume that all the gaps are
indeed removed. Then we can easily see that the resulting derivation is such that every rule
applied in it is a CTT rule. We have indeed associated every application of a dialogical rule
to a CTT rule, with the following exceptions: the rules involving elementary statements
by P (the SR-rules) and the rules for Resolution and Substitution for Instructions that do
not involve A-equalities. But applications of these three rules will also eventually be
removed. Indeed the last stage of the algorithm replaces local reasons with proof-objects,
so applications of the SR-rules regarding instructions will eventually be removed. Recall also that P-statements (elementary or not) that are dependent upon ⊥-eliminations correspond to those eliminations.

So far so good—though the critical task of checking that the CTT rules are properly applied still remains. This process must show the important fact that following the algorithm will eventually remove the gaps, as it was assumed above. In order to ground this assumption let us temporarily consider an extension of the CTT calculus which includes the rules SR-rules as well as a new rule called *Gap*. In relation to the the SR-rules, recall that in the so-called *full-presentation* of CTT, every leaf of a demonstration starts with an axiom of the form $A \vdash A$; thus, the introduction of SR is not at all foreign to the framework of a CTT-demonstration. In relation to *Gap*, it either allows to link (with the help of vertical dots) two nodes of the demonstration without a dialogical rule explaining such a link, or to introduce an expression as the last step of a sequence of vertical dots. We will show that when following the algorithm, each of the applications of the rule *Gap* will be replaced by applications of a suitable CTT rule or by applications of a SR-rule. We will then simply need to show that when no dialogical rule is applied to the corresponding node from C, the expression will not introduce additional gaps: the rearranging in the stage C.1 of the algorithm is harmless. Once we have reached this point, and after all the applications of a SR-rule have been removed, we are assured to have a proper CTT demonstration.

Accordingly, let us show first that the gaps introduced during the process of building the CTT demonstration are temporary and will be progressively removed bottom-up:

**Algorithm-Lemma (AL)**

For any stage of the translation procedure, there is a corresponding node in the original dialogical core C for every expression resulting from a gap.

**Proof**

This proof is a straightforward induction which also establishes that newly introduced gaps at a given stage of the translation have the “right shape”, so that they will be filled by a proper application of a rule later on.

The *base case* is trivial: the initial stage *A* of the algorithm stipulates that the first expression resulting from an application of the rule *Gap* is the thesis, which is obviously a node in *C* to which a dialogical rule is applied.

*Inductive Hypothesis.* Assume that AL holds for every application of the rule *Gap* up to this step in the translation procedure, say after *n* steps. We show that the Proposition holds for the gaps introduced at step *n* + 1 and that they have the correct “shape” in relation to the development of a CTT demonstration. This is done by cases, depending on the form of the last expression introduced at this point. For simplicity and brevity we only spell out two cases:

**Case 1:** The associated node in *C* is a P-disjunction *p* : *A* ∨ *B* which is not case-dependent, and the fragment of the derivation at stake at step *n* is:

$$ \vdots \\ p: A \lor B $$
Then, according to the algorithm, the result at step $n + 1$ is:

$$ \frac{\vdots \\ L^\vee(p): A \\ p: A \lor B}{\lor} IV $$

We next recall that we must have **O** challenging the disjunction at some place in the core: if there is a **P**-move in **C** which **O** does not challenge—though she could—then the core contains branches which do not represent terminal plays. However this is not possible since we have assumed **C** to be the core of a **P**-winning strategy. For the same reason, the core must feature the successful defence by **P** of one of the disjuncts, say **A**. Thus, the newly added expression filling up the dots introduced by *Gap* does indeed correspond to a node in **C**.

**Case 2:** The associated node in **C** is a **P**-conjunction $p: A \land B$ which is not case-dependent. After step $n$ we then have:

$$ \vdots \\ p: A \land B $$

so that according to the algorithm the result at step $n + 1$ is:

$$ \frac{\vdots \\ L(p): A \qquad R(p): B \qquad \vdots \\ p: A \land B}{\lor} I\land $$

Just like in the previous case, we must have **O** challenging the **P** conjunction at some place in the core—otherwise **C** would contain non-terminal plays and we would have a contradiction—resulting in a ramification in which each branch contains the statements by **P** of one of the conjuncts. The demonstration underway thus follows the CTT rule and the new expressions filling up the dots introduced by *Gap* correspond to these nodes in **C**.

The construction of the demonstration thus proceeds by progressively filling up the temporary gaps until it reaches a stage at which no further gap is introduced. Except for the initial assumptions of the demonstration, the cases in which no gaps are introduced are reduced to cases of atomic expressions. But these come either from an Elimination rule for $\perp$ or from the application of some *SR*-rule, that is, precisely the cases for which the premisses must already have been processed.

Summing up, the demonstration by induction of AL shows that the algorithm builds a derivation by introducing temporary gaps and then progressively filling them up until no further gap occurs. Moreover, this construction has been developed in such a way that the derivation complies with the proceedings of what we have called the extended CTT calculus (which includes the *SR*-rules).

Finally, as we have pointed out at the beginning of this section, the applications of the rules that do not strictly pertain to CTT are removed to guarantee that only CTT rules are applied in the resulting derivation. From all this together we have the following corollary:

**Algorithm-Corollary**

Let $C$ be the core of a winning $P$-strategy in the game for $p: \phi$ under initial concessions $\gamma_1, \dots, \gamma_n$. The result of applying the translation algorithm to $C$ is a CTT demonstration of $\phi$ under the hypotheses $\gamma_1, \dots, \gamma_n$.
This concludes the study of the process by the means of which dialogical strategies lead to CTT-demonstrations. For the demonstration of the equivalence between dialogical games and CTT, we need to consider the converse direction, namely from a CTT demonstration to a **P**-winning strategy. We tackle this issue in the next sections.

## IX.4 Part 2: from CTT demonstrations to strategies

In this chapter we will consider the other direction of the equivalence between the valid fragments of the CTT framework and the dialogical framework. That is, we will show that if there is a CTT demonstration for $\phi$, then there is a winning **P**-strategy in the dialogical game for $\phi$.

The demonstration, quite unsurprisingly, rests on developing a translation procedure which is the converse of the previous one. That is, we will present a procedure transforming a given CTT demonstration and we will show that the result is the core of a winning **P**-strategy—which is then expanded to a full-fledged winning strategy.

A core is expanded to a full strategy by adding branches accounting for variations in the order of the moves of the other player and in the local reasons he chooses. We will not give the specifics of that particular operation because it does not present any difficulty, and they have already been given in details in (Clerbout, 2014a; 2014c). We would rather focus on the way the initial CTT demonstration is transformed and on the proof that the result is the core of a winning **P**-strategy.

For the latter, we need to prove that the transformation results in a tree in which each branch represents a play won by **P**. In other words, we need to show that in the resulting tree each branch represents a legal sequence of moves ending with a **P**-move, or with **O** stating $\perp$. We also need to check that the tree has all the necessary information to be a core which can be expanded to a full strategy. That is to say, we must make sure that no possible play for **O** is ignored, excepting those varying in the order of the moves or the names of the local reasons.

The development of the next sections follows the proof by (Clerbout & Rahman, 2015) with the sole exception of the last step in which the equalities are introduced in the core for every **P**-move that is not a result of a SR4-rule (that is those elementary statements of **P** that do not involve resolution of instructions).

### IX.4.1 Transformation procedure

As in the first part, we first need here to design a transformation procedure. We will start with an informal description of the task and of the ideas underlying the procedure. Then we will provide the detailed algorithm.

#### Guidelines

In general there are two main obstacles such a procedure must overcome:

1. CTT is not an interactive-based framework. In particular the notions of players, challenges and defences are not present in CTT.

2. The progression of a CTT demonstration differs quite greatly from the progression of a dialogical core. Most notably, the production of ramifications on the one hand and the order of expressions on the other hand do not match in the two approaches.
These are just descriptions of the fundamental differences between a CTT demonstration and a dialogical core. There obviously are many other aspects which our translation method must take into account. Let us give further explanations on the topics on which the desired transformation procedure must operate.

## From CTT judgements to dialogical statements

To begin with we need to enrich the CTT demonstration with the players' identities. We need for that a way to figure out which expressions are stated by which player. In fact, there is a subtlety in this process because some steps in a CTT demonstration may be associated with either players, **P** or **O**; see below, “Identical statements by the two players”, for more details on this issue. But the general idea underlying the process is otherwise quite simple. The starting point is that the conclusion of the CTT demonstration is to be stated by **P** because it is the expression at stake: in a dialogue, that is the thesis. Moreover, the hypotheses of the demonstration, that is, the discharged assumptions that may occur at the leaves of the CTT demonstration, correspond to initial concessions made by **O**.

From there, it is quite straightforward to associate the other steps in the CTT demonstration with players by using the correspondences between the CTT and the dialogical rules used in the precedent sections. By means of illustration, suppose some step in the CTT demonstration has been associated to player **X** and suppose that the expression results from an application of the ⊃-Introduction rule. Then the assumption discharged by applying the Introduction rule is to be associated to player **Y** (it will occur in the core as the challenge by **Y**), and the expression immediately preceding the inference line is to be associated to player **X** (it will occur in the core as the defence by **X**).

## Identical statements by the two players

Because the CTT framework is not based on interaction, it does not distinguish between the two players. The point is that a CTT demonstration may very well feature expressions occurring only once, while two instances (or more) would be needed for a dialogical demonstration, that is, for the construction of a dialogical core. Elementary expressions associated to **P**, and which do not result from the application of the ⊥-Elimination rule, are one example. More generally, an expression may be used in a demonstration when applying the two kinds of rules: for example it can be used first when applying an Elimination rule and later on when applying an Introduction rule. In such cases, this expression is likely to occur as stated by the two players in a dialogical core (intuitively, this is because of the correspondence between Elimination rules and **O**-applications of rules on the one hand, and Introduction rules and **P**-applications of rules on the other hand). These consideration show the need of adding occurrences of expressions, but as stated by a different player.

## Dialogical instructions and local reasons

Next we need to account for the difference between CTT proof-objects on the one hand, and dialogical local reasons and instructions on the other hand. More precisely, we need to go from the CTT perspective on applications of rules to the dialogical perspective. In the CTT framework, applications of rules manifest themselves by specific operations defining the way proof-objects are obtained from other proof-objects. In the dialogical approach, meaning explanations are given in terms of local reasons and instructions at the other (prior) level of plays in which interaction prevails over the set-theoretic operations.
To perform this change of perspective, we start by substituting an arbitrary local reason *p* for the proof-object in the conclusion of the demonstration (and for that one only); in other words, we choose an arbitrary local reason for the thesis of the dialogical core we are building. Also, if relevant, we substitute local reasons for proof-objects in the expressions corresponding to initial concessions by O.

From there, it is a trivial matter to replace the other proof-objects occurring in the demonstration with the appropriate dialogical instructions. We simply look which analysis rule (section VII.1.2, Table 20) is applied to know which subscript must be associated to the letters *L* and *R* which will result in a proper dialogical instruction. For example, an instruction of the form *L*<sup>...</sup>—or *R*<sup>...</sup>—is substituted for the proof-object of the conclusion resulting from an application of the ∧-Elimination rule in the initial CTT demonstration.

Once we have a way to replace proof-objects with dialogical instructions, we are able to introduce local reasons as well. To do so we introduce the moves involving resolutions of instructions. We do so as we replace CTT proof-objects with dialogical instructions: every time we determine the dialogical instruction replacing the CTT proof-object, we also choose a local reason resolving the instruction. As a result, an expression “*α* : *φ*”, where *α* is a proof-object, will be replaced by an instruction of the form “*I* : *φ*” where *I* is an instruction. Immediately after that, another version of the same move is added in the structure, but with a local reason instead of the instruction *I*. By doing this immediately we can progressively replace proof-objects with simple instructions relative to local reasons, instead of having embedded instructions getting more and more (unnecessarily) complex.<fnref n="120" />

## Adding questions

At this point we have obtained a tree-like structure featuring a substantial number of expressions which differ only by the player identity, or maybe by the instruction and local reason.

Still, some aspects are missing to read the structure at hand in terms of interaction. To put it simply, the structure lacks challenges consisting in questions. For example, that two expressions **X** ! *I* : *φ* (for some instruction *I*) and **X** ! *p* : *φ* (for some local reason *p*) following each other in the structure does not make dialogical sense until the question **Y** *I*/? is placed between them; only then can we speak of an interaction in which **Y** asks **X** for the resolution of the instruction *I* and **X** chooses *p* for the resolution. Similarly with other questions such as ?_v_, ?_L_, ?_R_, etc., depending on the rule at stake.

The next step in the translation procedure is therefore to include questions in the relevant way so that one can accurately speak of interaction through the application of dialogical rules. However, the result still cannot be called a dialogical core. For that we need to overcome the difference in the production of ramifications between the CTT framework and dialogical strategies.

## Rearranging the branches and order of the moves

Recall that we are dealing with a tree-like structure written “upside-down”, that is, where the root of the tree (the conclusion of the demonstration we started with) is at the bottom and the leaves are at the top.

The most important transformation that remains is reorganising the tree at hand so that we obtain a good candidate for a core of a P-winning strategy. This means we aim

<footnote n="120">¹²⁰ Suppose for example that we have introduced an instruction *L*<sup>Y</sup>(*p*). If we do not immediately decide for a local reason, say *q*, resolving this instruction, then the next instruction will be of the form *I*(*L*<sup>Y</sup>(*p*)) instead of the simpler *I*(*q*)—for some *I*.</footnote>
for a tree in which branches are linear representations of plays in such a way that ramifications represent choices of **O** between different moves (since we are interested in **P**-strategies). The CTT framework distinguishes between rules applied to one or more expressions. In the latter case, a ramification is produced but not in the former case. But since there is no explicit notion of interaction and strategy (in the game-theoretical sense) in CTT, it is obvious that ramifications may not correspond to differences due to possible choices by a player, that are taken into account in a strategy for his adversary.

A typical example are the differences between the CTT Elimination rules for material implication and universal quantification on the one hand, and their dialogical counterpart on the other hand. In CTT these rules have (at least) two premisses: first, the complex expression, and, second, a judgement of the form $a : A$ when $A$ is the antecedent or the set which is quantified over. Each of these two premisses opens a branch in the demonstration. But in a dialogical game, one is the statement, the other is the challenge against it; consequently they occur in the same play and hence, in the same branch of a strategy. Notice that this will also happen with other rules including those equality assertions that in the CTT-demonstration result from the application of equality rules.

The goal in this step of the transformation is thus to reorganise the tree in order to overcome this discrepancy. We must also take some additional precautions (such as adding the choices of repetition ranks) so that the branches in the new tree do indeed represent plays.

Once this has been accomplished we reintroduce applications of the Socratic Rule (SR) to the **P**-elementary statements resulting from the resolution of some instruction. In other words, once all the previous steps have been carried out we reintroduce those equalities arising from **O**'s-choices while resolving instructions that have not been already implemented in the CTT demonstration. Recall that the standard CTT demonstrations deploy Σ- and Π-equalities only when the Elimination rules might produce a non-canonical proof-object.

We shall stop the general explanations here. All the details are given in the full description of the translation algorithm given below. Let us simply mention here that the procedure is meant to obtain the core of a **P**-winning strategy after all these modifications. This is something that must be proved, which we do afterwards.

## IX.4.2 The algorithm

Let us precise now the details of the procedure: we start with a CTT demonstration **D** of an expression **E** under a set **H** of global hypotheses or epistemic assumptions (that is, assertions that may include "given" proof-objects).

### Step A. From judgements to moves

First we enrich the initial demonstration with player identities and the sign !

### A1. Adding the players' identities

Rewrite the conclusion **E** as **P** ! **E**. Then, for every $h \in H$ occurring as a leaf of **D**, rewrite **h** as **O** ! **h**. Go to **A2**.
## A2. Using-up expressions

Scan *D* bottom-up. When there is no unused expression left, go to **A3**. Otherwise, let *E1* be the (left-most<sup>121</sup>) unused expression **X**! *E1*. Then,

(1) If **X** is **O** and *E1* results in *D* from applying an Introduction rule, then insert **P**! *E1* as the conclusion of the rule preceding **O**! *E1*. Consider the latter as used and go back to **A2**.

(2) If **X** is **P** and *E1* results in *D* from applying an Elimination rule other than for **V** or **Σ**, then insert **O**! *E1* as the conclusion of the rule preceding **P**! *E1*. Consider the latter as used and go back to **A2**.

(3) Otherwise use the correspondences between CTT and dialogical rules given in section IX.1 to rewrite the expressions allowing the application of the rule with the adequate player.<fnref n="122" />

In doing so, observe the following constraints:

1. an expression can be labelled as a **P**-move *and* an **O**-move,

* each player can be assigned at most once to an expression.

After this, consider the expression as used and go back to **A2**.

## A3. Corresponding O-moves

Scan the demonstration at hand. For each elementary statement by **P** which has no counterpart by **O** apply one of the following,

1. if it is the result of an application of the **⊥**-Elimination rule, then leave it as it is.

2. If there is no corresponding **O**-move, then insert one immediately below the **P**-move, and insert the expression **P** *Socratic Rule* at the leaf of the current branch.

Then go to **A4**.

## A4. Separating double labels

If there are leaves with the double label **O**! / **P**!, separate them into two expressions such that the **P**-move is placed as the leaf. Go to step **B**.

### Step B. Instructions and local reasons

Next we introduce local reasons in place of proof-objects. This is done in the following way.

## B1. Introducing arbitrary local reasons

In the conclusion **P**! *E*, replace the proof-object with an arbitrary local reason *p*. Then, for each initial concession **O**! *h* occurring at a leaf of the demonstration, substitute, if relevant, an arbitrary local reason for the proof-object. Consider these expressions as processed and go to **B2**.

The deployment of the procedure described by **A3** yields:

$$ \frac{\mathbf{O}! \alpha: (\Pi x: A) \quad \mathbf{P}! a: A}{\mathbf{O}! \dots \quad \mathbf{E} \Pi} $$

<footnote n="121">121 This accounts for the fact that *D* may have several branches.</footnote>

<footnote n="122">122 For example, given the situation
$$ \frac{\begin{array}{c} \alpha: (\Pi x: A) \\ \mathbf{O}! \dots \end{array}}{\begin{array}{c} a: A \\ \mathbf{E} \Pi \end{array}} $$</footnote>
## B2. Processing all the expressions

Scan the demonstration bottom-up. If there is no expression left unprocessed, go to C. Otherwise take the leftmost expression X!E2 with a local reason which has not been processed so far, and

* Use the correspondences between the CTT and the dialogical rules given in the previous sections to substitute the adequate instructions for the proof-object (or proof-objects) in the premiss (premisses) of the rule whose application results in X!E2.

* For each instruction introduced in that way, copy the expression at stake, replacing the instruction by an arbitrary local reason. Place the version with the local reason immediately above the expression with the instruction.

* Consider X!E2 as processed and go back to B2.

## Step C. Adding questions

Scan the demonstration and identify the applications of rules for which the dialogical counterpart features a question. For each expression understood as a defence according to such a rule, add the corresponding challenge performed by the adversary immediately below the expression.

Go to D.

## Step D. Moving the Opponent's initial concessions

Consider each leaf of the demonstration at hand which is an initial concession by O—that is, an undischarged assumption of the initial demonstration D which has been identified as an O-move. Remove it and place it below the conclusion P!E. In case of multiple occurrences, keep only one occurrence.

Go to E.

## Step E. Removing non-dialogical splits

Scan the demonstration top-down. Going from the left to the right, check each point where two different branches join. Depending on the case, apply one of the following,

1. If the ramification is such that the two branches are opened by two O-moves relevant for a rule dealing with a logical constant, then ignore them and proceed downwards.

2. Otherwise, “cut” one and “paste” it above the other one, according to the following convention:

* If both branches have a P-move as the leaf, or if both have an O-move as the leaf, then pick any one of the branch to be cut and pasted;

* Otherwise pick the one with a P-move at the leaf to be cut and pasted.

Go to F.

## Step F. Reordering the nodes.

Scan the tree structure at hand bottom-up. Starting from the thesis P!E, change the order of the expressions according to the following conditions,

* each O-move is a reaction—as specified by the dialogical rules—to the P-move placed immediately below;
* a question or a statement which is a challenge always occurs before (i.e. closer to the root) a defence reacting to it.

* Ramifications are preserved so that each branch is opened with an **O**-move as a reaction to a **P**-move which is immediately below.

Go to **G**.

**Step G. Introducing equalities by means of the Socratic rule**

Search for nodes labelled *SR* (*Socratic Rule*). Depending on the case, apply one of the following:

* If the **O**-expression copied by **P** is the result of applying a CTT equality rule, apply the relevant case defined in SR5.3.1: Non-reflexive cases of the Socratic rule (see section VII.2.1).

* If the **O**-expression copied by **P** is *not* the result of applying a CTT equality rule, apply the relevant case defined in SR5.3.2: Reflexive cases of the Socratic rule (section VII.2.1).

**Explanation**

The first case occurs when the **O**-expression is the result of a two step process in the CTT demonstration: the first step being an application of an elimination rule, and the second an application of an equality rule computing the proof-object to a given value. In the context of a dialogical play, this corresponds to **O** resolving or substituting an instruction. As explained in the description of the Socratic rule, this corresponds to a non reflexive case.

The second case occurs when the **O**-expression is an assumption, when a value for the proof-object is directly introduced without being computed by means of a CTT equality rule. In the context of a dialogical play, this corresponds to **O** conceding an elementary expression directly, without going through the resolution of substitution of an instruction. In this context, the Socratic rule specifies that **P** will apply the reflexive case of the rule.

Go to **H**.

**Step H. Adding ranks**

Insert an expression **O**n := 1 immediately above the thesis **P**!**E**. Then insert an expression **P**m := k above the one just inserted. Choose k to be the highest number of times a given rule is applied by **P** to the same expression in the tree.

The procedure stops.

IX.4.3 Adequacy of the algorithm

We have developed the algorithm transforming a CTT demonstration into a winning strategy. It remains to show that the algorithm indeed does so, in other words that applying the algorithm to a given a CTT demonstration results in the core of a **P**-winning strategy.

To be more specific, the point is to show that the result of applying the algorithm to a CTT demonstration is a tree in which,

1. each branch represents a play: the sequence of moves in each branch complies with the game rules,

2. each play in the tree is won by **P**,
3. the tree describes all the relevant alternatives for a core. In other words: there is no significantly different course of action for **O** that would be disregarded in the resulting tree.<fnref n="123" />

**Proposition 1**

*Each branch in the resulting tree represents a play.*

We need to show that in each branch the sequence of moves complies with the rules of dialogical games.

**Proof**

Because the translation observes a correspondence between CTT rules and dialogical particle rules (recall that step C of the algorithm is used to insert questions), we simply need to check that the dialogical structural rules are observed. We leave the Winning Rule aside for now since it is the topic we address in the next Proposition.

So for the Starting Rule SR0, steps D and H of the algorithm ensure that every sequence of moves in the tree starts with the initial concessions of **O**, which are followed by the thesis stated by **P**, and then by the choices of repetition ranks.

As for the Intuitionistic Development Rule, step F of the algorithm guarantees that each move following the repetition ranks in a sequence is played in reaction to a previous move. The condition in step F according to which **O**-moves immediately follow the **P**-move to which they react ensures that the intuitionistic restriction of the *Last Duty First* is observed.<fnref n="124" /> Moreover the choice of the repetition ranks prescribed by step H ensures that the players do not perform unauthorised repetitions.

As for the Socratic rule, no challenge against an elementary **O**-statement is added when applying the algorithm. Moreover, in the case of elementary statements made by **P**, step A3 and G of the procedure ensure that, if needed, a corresponding move by **O** and the adequate challenges and defences are added.

As for the rules related to the Resolution of Instructions, step B of the algorithm (in combination with step C introducing questions) guarantees that instructions are resolved according to the structural rules SR3 and SR4—recall that we ignore the formation dialogues since we are focusing on that fragment of CTT in which verifying the well formation is assumed successful.

Now that we have established that the branches represent plays because they comply with the dialogical rules, we must assess the situation in relation to victory and show that:

**Proposition 2**

*Each branch of the resulting tree represents a play won by **P**.*

<footnote n="123">123 By significantly different we mean other than relative to the order of **O**'s moves, or the choice of local reasons to replace instructions.</footnote>

<footnote n="124">124 This is known since (Felscher, 1985). See also more details in (Clerbout, 2014c).</footnote>
**Proof**

We must check that the leaf of each branch is either:

1. an elementary statement by **P** preceded by a **O**-statement of $\perp$,

2. an elementary statement by **P** (different to the previous case),

3. a **P**-equality that results from applying the Socratic Rule.

But all this is guaranteed by steps A3, E, F and G of the algorithm.

Finally, it remains to show that the tree describes all the relevant courses of actions for the Opponent underlying the core of a **P**-strategy:

**Proposition 3**

*There is no **P**-move in the tree remaining unanswered by **O** and there is no rule that would allow leaving such a **P**-move without a response.*

**Proof**

We know from the initial demonstration *D* and steps A1-A4 of the algorithm that every statement made by **P** in the resulting tree occurs as the result of an Introduction rule, of the Elimination rule for the $\Sigma$ operator or of the Elimination rule for disjunction. In the case of complex statements, the correspondence with dialogical particle rules, together with the addition of questions via step C of the algorithm, ensure that they are challenged and that when they are themselves played as challenges they are answered. In the case of elementary statements, we know from the proof of the preceding Proposition (2) that they are challenged if **O** may challenge them.

Moreover, all the possible challenges allowed by the particle rules are covered by the CTT rules they correspond to. For this reason, the only remaining possible variations left to **O** are the order of her moves and the choice of local reasons for the Resolution of Instructions. But these variations are the ones which are not relevant to build the *core* of a **P**-strategy. In other words the correspondence between CTT rules and the particle rules ensure that the starting demonstration *D* already contains the variations which are relevant to the core of a **P**-strategy.

The adequacy of our translation procedure, which amounts to the second direction of the equivalence between CTT demonstrations and dialogical strategies, is then a direct consequence of these three Propositions.

**Corollary**

*The result of applying the algorithm that transcribes a CTT demonstration into a tree of P-terminal plays constitutes the core of a winning P-strategy.*

## IX.5 Exercices

Transform the core of the winning strategy for the following theses into a natural-deduction demonstrations by deploying the procedure described in the preceding sections.

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

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

**Solution to exercise 1: demonstration of $(A \land B) \land C$ [c: $A \land (B \land C)$]**

Recall from section VII.7.4 the core of the winning strategy for the thesis.
<figure><img src="image_25.png" /><figcaption>Figure 5: Exercise 1 - the core</figcaption></figure>

Let us now launch the procedure for transforming the tree for the winning strategy into a natural deduction tree.

Steps A-B on the thesis

We place the thesis as conclusion and the initial concession as global assumption. Since in the tree the initial concessions occur before a branching, we need to introduce two branches in the demonstration starting both by the same initial concession:

<figure><img src="image_26.png" /><figcaption>Figure 6: Exercise 1 - Step A</figcaption></figure>

We now scan for the lowest expression in the demonstration tree—at this time it is the thesis—and find in the core the responses to it—the responses here are the challenges on the conjunctions; in order to help the reading of the process, we highlight in bold the last challenge-defence pair:

<figure><img src="image_27.png" /><figcaption>Figure 7: Exercise 1 - Step B on the thesis<fnref n="125" /></figcaption></figure>

<footnote n="125">¹²⁵ To help the reader we add this step with the challenges in request form on the conjunction, though the algorithm does not include the questions in the demonstration tree. We will not put them further on.</footnote>
<figure><img src="image_28.png" /></figure>

Whereas the left of the two expressions added in this step is a conjunction, the right is an elementary expression: steps **B.2.b** and **B.2.a** apply respectively. Let us start with the latter, and therefore begin with the right branch.

**Building the right branch: steps B-C**

Since $c_{2,2}: C$ is a **P**-elementary expression we know that it must be the result of Socratic rule (here noted SR).

<figure><img src="image_29.png" /><figcaption>Figure 8: Exercise 1 - Step B.2.a</figcaption></figure>

We now look in the core for the **O**-move that allowed **P** to state $c_{2,2}: C$. In order to do so, we search for the equality move that defended the challenge upon $c_{2,2}: C$—it is the equality move 14, and it provides the information that this statement uses move 11.

<figure><img src="image_30.png" /><figcaption>Figure 9: Exercise 1 - Step B.2.a</figcaption></figure>

We know that **O**'s elementary moves are either initial concessions or the result of an elimination rule: here move 11 is an answer to **P**'s challenge on the conjunction $B \land C$ stated move 7; so **O**'s move $c_{2,2}: C$ is the result of an elimination rule on the conjunction.

<figure><img src="image_31.png" /><figcaption>Figure 10: Exercise 1 – Step B.2.b (iv)</figcaption></figure>
The move $c_2: B \land C$ is the lowest of the expressions just added, so we apply once more **step B** and search in the core for the moves that triggered it: a defence to **P**'s challenge on the initial concession $c: A \land (B \land C)$—a conjunction again: the rule allowing for the statement $c_2: B \land C$ is therefore a conjunction elimination rule (we skip here the instructions and replace them straight).

<figure><img src="image_32.png" /><figcaption>Figure 11: Exercise 1 - Step B.2.b</figcaption></figure>

Step C to the right branch. The premiss for inferring $c_2: B \land C$ being already in the tree, we move to step C for this branch: we now delete the SR and leave only one copy of the elementary expression.

<figure><img src="image_33.png" /><figcaption>Figure 12: Exercise 1 - Step C to the right</figcaption></figure>

## Building the left branches: steps B-C

We now turn our attention to the left branch and take the lowest expression last added in the branch of the demonstration: it is a conjunction stated by **P**, so it is the result of a conjunction introduction rule. Since it is an introduction rule, the premisses must be constituted by the members of the conjunction stated by **P**, which opens two different branches, one for each side of the conjunction:

<figure><img src="image_34.png" /><figcaption>Figure 13: Exercise 1 - step B to the left</figcaption></figure>

With the resolution of the instructions we obtain:

<figure><img src="image_35.png" /><figcaption>Figure 14: Exercise 1 - step B to the left with instructions</figcaption></figure>
<figure><img src="image_36.png" /><figcaption>**Figure 18: Exercise 1 - Step C to the left**</figcaption></figure>

**Step D: inserting proof-objects**

We've reached the final step, and now replace the local reasons with proof-objects and obtain the CTT-demonstration in the style of natural deduction tree.

<figure><img src="image_37.png" /><figcaption>**Figure 19: Exercise 1 - step D**</figcaption></figure>

Recall from section VII.7.4 that the *strategic reason* for the thesis $d: (A \land B) \land C$ [c: $A \land (B \land C)$] is $\langle\langle L^\wedge(R^\wedge(c), L^\wedge(c)), R^\wedge(R^\wedge(c)) \rangle\rangle: (A \land B) \land C$, which is the dialogical counterpart to the proof-object in the demonstration tree.

**Solution to exercise 2: ($B \land A \supset C$ [$c: (A \land B) \supset C$]**

We start by displaying the core. As in section VII.7.4 we repeated move 16:

<figure><img src="image_38.png" /><figcaption>**Figure 20: Exercise 2 - the core**</figcaption></figure>
$$19. \mathbf{O} ? = d_{1,2} [?, 18]$$

$$20. \mathbf{P} R^{\wedge}(d_1) = d_{1,2}: \mathbf{A} [!, 19]$$

P wins

$$19. \mathbf{O} ? = d_{1,1} [?, 18]$$

$$20. \mathbf{P} L^{\wedge}(d_1) = d_{1,1}: \mathbf{B} [!, 19]$$

P wins

$$19. \mathbf{O} ? = c_2 [?, 18]$$

$$20. \mathbf{P} R^{\neg}(c) = c_2: \mathbf{C} [!, 19]$$

P wins

### Step A-B on the thesis

Step A. We place the thesis $(B \wedge A) \supset C$ as conclusion and the initial concession $c: (A \wedge B) \supset C$ as global assumption:

<caption>Figure 21: Exercise 2 - Step A</caption>

$$\frac{c: (A \wedge B) \supset C \quad \vdots \quad (B \wedge A) \supset C}{\phantom{c: (A \wedge B) \supset C}}$$

Step B. We scan now for the lowest expression in demonstration tree—the thesis at this stage—and find in the core the response to it—a challenge on the implication. The challenge on the **P**-implication is the local assumption $d_1: B \wedge A$ (after resolution of instructions), which is one of the premisses of the implication introduction rule; the second premiss is the **P**-move $c_2: C$ occurring move 18 on the outmost right branch of the core.

<caption>Figure 22: Exercise 2 - step B on the thesis</caption>

$$\frac{c: (A \wedge B) \supset C \quad \vdots \quad \frac{d_1: B \wedge A \quad \vdots \quad c_2: C}{(B \wedge A) \supset C} \quad I \supset}{\phantom{c: (A \wedge B) \supset C}}$$

### Step B: building the branches

Since the defence $c_2: C$ of the implication is a **P**-elementary expression, it must be a copy of a move made by **O**; move 18 is a copy of move 17, as recorded by the equality of move 20. This yields the following **SR** indication:

<caption>Figure 23: Exercise 2 - step B.2.a</caption>

$$\frac{c: (A \wedge B) \supset C \quad \vdots \quad \frac{d_1: B \wedge A \quad \vdots \quad \frac{c_2: C}{c_2: C} \quad SR}{(B \wedge A) \supset C} \quad I \supset}{\phantom{c: (A \wedge B) \supset C}}$$

Now, the core informs us move 17 results from the resolution of the right part of the initial concession $c: (A \wedge B) \supset C$, an implication: it thus results from the implication elimination applied to the concession; since the concession is an implication, **P** must state the antecedent in order to challenge it, which yields the **P**-move 14 $c_1: A \wedge B$.

<caption>Figure 24: Exercise 2 - Step B.2.b</caption>

$$\frac{d_1: B \wedge A \quad \vdots \quad \frac{c_1: A \wedge B}{c: (A \wedge B) \supset C} \quad E \supset}{\phantom{d_1: B \wedge A}}$$
<figure><img src="image_39.png" /></figure>

We know that **O** has two options to respond to a challenge on an implication, namely, stating the consequent, or launching a counterattack on the challenge. The defensive move has been implemented in the previous step, so we must now deal with the counterattack. Since the **P**-challenge is a conjunction, there are two possible challenges, namely, left, or right, each of them opening a new branch. The branches of the core trigger two branches in the demonstration tree by applying twice the conjunction introduction rule, corresponding to move 18 in the outmost left branch and move 18 in the middle branch respectively.

<figure><img src="image_40.png" /><figcaption>Figure 25: Exercise 2 - step B.2.b</figcaption></figure>

Since **P**-moves $d_{1.2}:A$ and $d_{1.1}:B$ are elementary, they are the result of the application of the Socratic Rule.

<figure><img src="image_41.png" /><figcaption>Figure 26: Exercise 2 - step B.2.a</figcaption></figure>

In the core, move 5 **O**! $L^\wedge(d_1):B$ and move 9 **O**! $R^\wedge(d_1):A$ convey the information that the **O**-moves result from applying the conjunction elimination rule to the local assumption $d_1: B \land A$.

<figure><img src="image_42.png" /><figcaption>Figure 27: Exercise 2 - final step B</figcaption></figure>
corresponding proof-objects, or, analogously, proof-objects are a kind of linear, interaction-free reading of the corresponding strategic reasons.

In the case in point, the general structure of the strategic reason shows the (strategic) dependence of **P**'s reason for the consequent upon **O**'s reason for the antecedent in a way similar to how the proof-object of the conclusion shows how the proof-object for the consequent results from applying a certain function to the proof-object for the antecedent. Notice how the interactive aspects in the strategic reason are accounted for by means of the players' identities and the equalities.

More precisely on the concrete example at hand, the most obvious connection between the strategic reason for the thesis and the proof-object for the conclusion lies between the dialogical instructions $L^>(d_1)$ and $R^>(d_1)$ in the strategic reason, and **fst**(d_1) and **snd**(d_1) in the proof-object.

Once we have noticed this, it is straightforward to read the *left-hand part* of the strategic reason

$$ (R^>(c))^0 \llbracket (L^>(L^>(c)))^P = R^>(d_1)^{P,o}, R^>(L^>(c))^P = L^>(d_1)^{P,o} \rrbracket^P $$

as saying that the reason $R^>(c)$ for $C$ is obtained from the pair $\langle R^>(d_1), L^>(d_1) \rangle$ (read as $\langle \mathbf{snd}(d_1), \mathbf{fst}(d_1) \rangle$) given **O**'s reason $\langle L^>(d_1), R^>(d_1) \rangle$ in the right-hand part, read as $\langle \mathbf{fst}(d_1), \mathbf{snd}(d_1) \rangle$.

The strategic dependence of **P**'s reason upon **O**'s reason is then to be read from the CTT point of view as the existence of a function between the two parts, that is, as a lambda abstraction, which gives us the proof-object $\lambda d_1. [\mathbf{ap}(c, \langle \mathbf{snd}(d_1), \mathbf{fst}(d_1) \rangle)]$ for the CTT conclusion.
# X. MATERIAL DIALOGUES

As pointed out by Krabbe (1985, p. 297), material dialogues—that is, dialogues in which propositions have content—receive in the writings of Paul Lorenzen and Kuno Lorenz priority over formal dialogues: material dialogues constitute the *locus* where the logical constants are introduced. However in the standard dialogical framework, since both material and formal dialogues marshal a purely syntactic notion of the formal rule—through which logical validity is defined—, this contentual feature is bypassed,<fnref n="126" /> with this consequence that Krabbe and others after him considered that, after all, *formal* dialogues had priority over material ones.

As can be gathered from the above discussion, we believe that this conclusion stems from shortcomings of the standard framework, in which local reasons are not expressed at the object-language level. We thus explicitly introduced these local reasons in order to undercut this apparent precedence of a formalistic approach that makes away with the contentual origins of the dialogical project.

And yet the Socratic Rule, as defined in the main chapters of our study (VI-IX), entirely leaves the introduction of local reasons to the Opponent (the Proponent only being allowed to copy what the Opponent introduced). This rule applying to *any* proposition (or set), it can be considered as a formal rule; so if we are to specify the rules for *material* reasoning—to use Peregrin’s (2014, p. 228) apt terminology—, the rules specifying the elementary propositions involved in a dialogue must also be defined: whereas in the structural rules for formal dialogues of immanent reasoning (see section VII.2), only the Socratic rules dealt with elementary statements, and without providing any specification on that statement beside the simple fact that it must be the Opponent who introduces them in the dialogue, the structural rules for material dialogues of immanent reasoning will have Socratic rules that are player dependent rules for elementary statements specific to that very statement, but the global rules (player independent) also include rules for elementary statements, specific to those statements (thus providing the material level). These Global rules establish how to synthesize and analyze local reasons during the development of play, once the role of the players have been fixed; they are thus at the structural level and not at the local level, though we still speak of *local* reasons (and *not* of global reasons).

Thus, as mentioned in section VI.2, a local reason prefigures a material dialogue displaying the content of the proposition stated. This aspect makes up the ground level of the normative approach to meaning of the dialogical framework, in which *use*—or dialogical interaction—is to be understood as *use prescribed by a rule*; such a use is what Peregrin (2014, pp. 2-3) calls the *role of a linguistic expression*. Dialogical interaction is this *use*, entirely determined by rules that give it meaning: the linguistic expression of every statement determines this statement by the role it plays, that is by the way it is used, and this use is governed by rules of interaction. The meaning of elementary propositions in dialogical interaction thus amounts to their *role* in the kind of interaction that is governed by the Socratic and Global rules for material dialogues, that is by the specific formulations of the Socratic and Global rules for precisely those very propositions.

It follows that material dialogues are important not only for the general issue on the normativity of logic but also for rendering a language with *content*.

<footnote n="126">¹²⁶ (Krabbe, 1985, p. 297)</footnote>
A thorough study on material dialogues is still work in progress and it seems to be
related to recent researches by Piecha & Schröder-Heister (2011) and Piecha (2012) on
dialogues with definitions. A study devoted to material dialogues as applied to natural
language will require a text of a similar length as the one of the present book; however
we can already sketch the main features of material dialogues that include sets of natural
numbers and the set **Bool**. The latter allows for expressing classical truth-functions
within the dialogical framework, and it has an important role in the CTT-approach to
empirical propositions.<fnref n="127" /> Accordingly, this chapter is structured as follows:

(1) A first section (X.1) will introduce material dialogues through one of its cases, **Bool**, which is central for material dialogues as it provides the means for dealing with empirical quantities (the canonical elements of **Bool** being the answers to yes or no questions); this will also enable us to provide the truth-functional operators within a dialogical framework.

(2) We will then (section X.2) provide further rules on material dialogues, dealing more generally with identity and equality, and provide an application of these rules by demonstrating *within* the system—that is, without presupposing a metalanguage—that every element of the set **Bool** is equal to *yes* or *to no*, which has many consequences in the foundations of mathematics, discussed in the following section.

(3) A further section (X.3) will deal more precisely with issues concerning mathematics and logic, where we will introduce natural numbers and broaden the perspective on **Bool**. We will then test the approach by discussing some case-studies in the domains of the foundations of mathematics and non-classical truth-functional operators.

a. Developing the consequences of the demonstration of section X.2.3 on **Bool**, we shall first demonstrate that the two canonical elements **yes**, **no** of the set **Bool** are different; we shall then approach the fourth axiom of Peano's arithmetic ("0 is identical to no successor of a natural number": $(\forall x : \mathbb{N}) \neg \mathrm{Id}(\mathbb{N}, 0, s(x))$). Moreover, such a demonstration gives us the chance to delve into the notion of a universe $\mathcal{U}$ constituted by sets dependent upon the Boolean set $\{\mathbf{yes}, \mathbf{no}\}$. In other words, while $\mathcal{U}$ is constituted by codes of sets, there is no code for $\mathcal{U}$ itself. Universes constitute the constructivist formulation of the mathematical notion of *sets of sets*.

b. In relation to the introduction of non-classical truth-functional operators, we will generalize Boolean operators to operators within finite sets and we will put this dialogical framework into work by integrating logics tolerant to some contradictions.

(4) Empirical quantities will then (section X.4) be inserted within material dialogues. Empirical content can thus be inserted within the framework of immanent reasoning: it comes from using “empirical quantities” as the outcome of procedures triggered by questions pertaining specifically to that quantity.

(5) The final section (X.5) will make explicit the epistemological background underlying the dialogical framework, by stressing the notion of

<footnote n="127">¹²⁷ See (Martin-Löf, 2014)</footnote>
internalization.<fnref n="128" /> In this respect, the dialogical framework can be considered as a formal approach to reasoning rooted in the dialogical constitution and "internalization" of content—including empirical content—rather than in the syntactic manipulation of un-interpreted signs. This discussion on material dialogues will provide a new perspective on Willfried Sellars' (1991, pp. 129-194) notion of *Space of Reasons*: the dialogical framework of immanent reasoning enriched with the material level should show how to integrate world-directed thoughts (displaying empirical content) into an inferentialist approach, thereby suggesting that immanent reasoning can integrate within the same epistemological framework the two conflicting readings of the Space of Reasons brought forward by John McDowell (2009, pp. 221-238) on the one hand, who insists in distinguishing world-direct thought and knowledge gathered by inference, and Robert Brandom (1997) on the other hand, who interprets Sellars’ work in a more radical anti-empiricist manner. The point is not only that we can deploy the CTT-distinction between *reason* as a premise and *reason* as a piece of evidence justifying a proposition, but also that the dialogical framework allows for distinguishing between the objective justification level targeted by Brandom (1997, p. 129) and the subjective justification level stressed by McDowell. According to our approach the subjective feature corresponds to the play level, where a concrete player brings forward the statement *It looks red to me*, rather than *It is red*. The general epistemological upshot from these initial reflections is that, on our view, many of the worries on the interpretation of the Space of Reasons and on the shortcomings of the standard dialogical approach to meaning (beyond the one of logical constants) have their origin in the neglect of the play level.<fnref n="129" />

## X.1 Material dialogues for Bool

Most of the literature differentiating the philosophical perspective underlying the work of Boole and the one of Frege focused on discussing either the different ways both authors understood the relation between logic and psychology or the links between mathematics and logic, or both. According to these studies, Boole's framework has been mainly conceived as a kind of psychologism and a programme for the mathematization of logic, contrasting as well with Frege's radical anti-psychologism as with his logicist project for the foundations of mathematics. These comparative studies have also been combined with the contrast between model-theoretical approaches to meaning, with their associated notion of *varying domains of discourse*, versus inferentialist approaches to meaning, with a *fixed universe of discourse*. It might be argued that while the first approach could be more naturally understood as an offspring of the algebraic tradition of Boole-Schröder, the second approach could be seen as influenced by Frege's *Begriffsschrift*.<fnref n="130" />

<footnote n="128">¹²⁸ By "internalization" we mean that the relevant content is made part of the setting of the game of giving and asking for reasons: any relevant content is the content displayed during the interaction. For a discussion on this conception of internalization see (Peregrin, 2014, pp. 36-42).</footnote>

<footnote n="129">¹²⁹ For some recent literature on those kind of objections to the approach to meaning of the dialogical conception of logic of (Lorenzen & Lorenz, 1978) see (Duthil Novaes, 2015) and (Trafford, 2017), chapter 4, section 2. Our concluding chapter (XI) will deal with this neglect of the play level at length.</footnote>

<footnote n="130">¹³⁰ Recall the distinction of language as the universal medium and as a calculus (van Heijenoort, 1967).</footnote>
However, from the point of view of contemporary classical logic, and after the meta-mathematical perspective of Gödel, Bernays, and Tarski, both Boole's and Frege's view on semantics are subsumed under the same formalization, according to which classical semantics amount to a function of interpretation between the sentences **S** of a given language **L** and the set of truth values {0, 1}—let us call such a set the set **Bool**. This function assumes that the well-formed formulae of **S** are made dependent upon a domain—either a *local domain of discourse* (in the case of Tarski's-style approach to Boolean-algebra), or a *universal domain* (in the case of Frege). More precisely, this functional approach is based on a separation of cases that simply assumes that the quantifiers and connectives take propositional functions into classical propositions—for a lucid insight on this perspective's limitations see (Sundholm, 2006). In fact, the integration of both views within the same formal semantic closes a gap in Boole's framework, which was already pointed out by Frege: the links between the semantics of propositional and first-order logic.<sup>131</sup>

*Constructive Type Theory* includes a third (epistemic) paradigm in the framework allowing for a new way of dividing the waters between Boolean operators and logical connectives, and, at the same time, integrating them in a common inferential system in which each of them has a specific role to play. The overall paradigm at stake is the Brouwer–Heyting–Kolmogorov conception of propositions as sets of proofs embedded in the framework in which, thanks to the insight brought forward by the Curry–Howard isomorphism (Howard, 1980), propositions are read as sets and as types.

In a nutshell: the CTT framework takes judgements, not propositions, to yield the minimal unity of knowledge and meaning—as the old philosophical tradition did before the spreading of the metalogical view of Gödel, Tarski and Bernays; see (Sundholm, 1997; 1998; 2001; 2009) (2012; 2013b; 2013a). Within CTT the simplest form of a judgement (the categorical) is an expression of the form

$a : B$

where "B" is a proposition and "a" a proof-object on the grounds of which the proposition B is asserted to be true, standing as shorthand for

"a provides evidence for B".

In other words, the expression "a : B", is the formal notation of the categorical judgment

"The proposition B is true",

which is shorthand for

"There is evidence for B".

According to this view, a proposition is a set of elements, called proof-objects, that make the proposition *B* true. Furthermore, we distinguish between *canonical proof-objects* on the one hand, those entities providing a *direct evidence* for the truth the proposition *B*, and on the other hand *non-canonical proof-objects*, the entities providing indirect pieces of evidence for *B*.

<footnote n="131"><sup>131</sup> Frege points out that within Boole's approach there is no organic link between propositional and first-order logic : “In *Boole the two parts run alongside one another* ; so that *one is like the mirror image of the other, but for that very reason stands in no organic relation to it*” (Frege G. , Boole's Logical Calculus and the Concept Script [1880/81], 1979).</footnote>
This generalization also allows another third reading: a proposition is a *type* and its elements are instances of this type. If we follow this reading proof-objects are conceived as instantiations of the type. This type-reading naturally leads to Brouwer–Heyting–Kolmogorov's constructivism mentioned above: if a proposition is understood as the set of its proofs, it might be the case that we do not have any proof for that proposition at our disposal, but that we neither have a proof for its negation (thus, in such a framework, *third excluded fails*). Notice that the constructivist interpretation requires the intensional rather than the extensional constitution of sets—recall the Aristotelian view that no "form" ("type") can be conceived independently of its instances and reversewise.

Moreover CTT provides a novel way to render the meaning of the set {0, 1} as the type **Bool**. More precisely, the type **Bool** is characterized as the set of the canonical elements 0 and 1. Thus, each non-canonical element is equal to one of them. But what kind of entities are those (non-canonical) elements that might be equal to 1 or 0? Since in such a setting 1, 0 and those equal to them are elements, they are not considered to be of the type proposition; they are rather providers of truth or falsity of a proposition (or a set, according to the Curry–Howard isomorphism between propositions, sets, and types): they are proof-objects that provide evidence for the assertion **Bool true**.

In order to illustrate our point here and to explicit the link with material dialogues, let us take an example outside of mathematics, for instance this *sentence*:

*Bachir Diagne is from Senegal.*

This sentence differs from the *proposition*, that is, what Frege called the *sense* or *thought* expressed by that sentence, which would be

*that *Bachir Diagne is from Senegal***

So if we take the sentence as expressing the proposition, then we might be able to bring forward some proof-object—some piece of evidence *a*, his passport or his birth certificate for instance—that renders the proposition *that *Bachir Diagne is from Senegal*** true. In such a case we have the assertion that the proposition is true on the grounds of the piece of evidence *a* (the passport), which we can write:

*passport : *Bachir Diagne is from Senegal*

or, in a more general assertion:

*That *Bachir Diagne is from Senegal*** **true**
*(there is some piece of evidence that *Bachir Diagne is from Senegal*)*

In this fashion, if we take the sentence *Bachir Diagne is from Senegal* as related to a *Boolean object*, then this sentence triggers a procedure yielding a non-canonical element, say **X** (the proposition), of the set **Bool**. In such a case the sentence would not *express* a proposition, but it could be understood as an *answer* to the question:

*Is *Bachir Diagne from Senegal*?*

the answer being:
yes, Bachir Diagne is from Senegal

which would thus yield the outcome **1**. In other words, determining to which of the canonical elements, **1** or **0**, the non-canonical element **X** is equal, would require answering to the question *Is Bachir Diagne from Senegal?* Thus, in our case, we take it to be equal to **1**.<fnref n="132" /> The procedure would amount to the following steps:

*Is Bachir Diagne from Senegal?*

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

yes, Bachir Diagne is from Senegal

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

**X = 1 : Bool**

The arrows indicate that determining to which of the elements **X** is equal actually is the result of an enquiry (in this case an empirical one).

This is not only different from:

*passport : Bachir Diagne is from Senegal*

but it is also different from:

**Bool true**

Indeed, while **X = 1 : Bool** expresses one of the possible outcomes the non-canonical element **X** can take in **Bool**, **Bool true** expresses the fact that at least one element of the set **Bool** can be brought forward.

Thus, a distinction is drawn between the Boolean object **1** (one of the canonical elements of **Bool**) and the predicate **true** that applies to **Bool**.

Moreover, operations between elements of **Bool** would then not be the logical connectives introduced by natural deduction rules at the right hand side of the colon, but they would be operations between objects occurring at the left hand side of the colon. For example the disjunction `+` at left of the colon in

$$A + B = 1 : \mathbf{Bool} \ (\mathit{given} \ A = 1 : \mathbf{Bool})$$

stands for an operation between the non-canonical **Boolean** objects A and B; whereas the disjunction occurring at right of the colon in the assertion

$$b : A \lor B \ (\mathit{given} \ b : A)$$

expresses the familiar logical connective of disjunction, that is here true since a piece of evidence for one of the disjuncts is provided: the piece of evidence b for A.

<footnote n="132">¹³² For the interpretation of empirical propositions see (Martin-Löf, 2014).</footnote>
Since **Bool** is a type, and since according to the Curry-Howard isomorphism, it is itself a proposition, we can certainly have both, propositional connectives as sets of proof-objects, and have them combined with Boolean operations. This allows us, for example, to demonstrate that each canonical element in **Bool** is identical either to **1** or **0**:

$$ (\forall x: \mathbf{Bool}) \mathbf{Id}(\mathbf{Bool}, x, 1) \lor \mathbf{Id}(\mathbf{Bool}, x, 0) \text{ true} $$

This will however require first a presentation of the dialogical rules for **Bool** and the Boolean operators, which will enable us to introduce dialogical rules for material meaning (Specific Socratic rules) through the case of **Bool**, before providing the general notions of material dialogues with the rules for identity and equality (section X.2). We will then have all the elements for dealing with the demonstration of the above proposition, which we shall carry out (see section X.2.3) in the dialogical framework of immanent reasoning.

## Dialogical Rules for Boolean Operators

In the dialogical framework, the elements of **Bool** are responses to yes-no questions, so that each element of **Bool** is equal to **yes** or **no**. Responses such as **b = yes** or **b = no** make explicit one of the possible origins of the answer **yes** (or **no**), namely whether **b** is or not the case. Here are the Global (player independent) rules for synthesis, analysis, and equalities of the Boolean operators.

<table><caption>Table 31: Global rules for **Bool** and Boolean operators in immanent reasoning</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Synthesis</th><td><b>X</b> ! <b>Bool</b></td><td><b>Y</b> ? <sub><b>Bool</b></sub></td><td><b>X</b> <i>yes</i> : <b>Bool</b><br><b>X</b> <i>no</i> : <b>Bool</b></td></tr><tr><th>Analysis</th><td><b>X</b> <i>p</i> : <i>C</i>(<i>c</i>)[<i>c</i>: <b>Bool</b>]</td><td><b>Y</b> ? = <i>c</i><sup><b>Bool</b></sup></td><td><b>X</b> <i>c</i> = <b>yes</b> : <b>Bool</b><br><b>X</b> <i>c</i> = <b>no</b> : <b>Bool</b></td></tr><tr><th>Equalities</th><td><b>X</b> <i>c</i> = <b>yes</b> : <b>Bool</b><br>...<br><b>X</b> <i>p</i> : <i>C</i>(<i>c</i>)[<i>c</i>: <b>Bool</b>]<br><b>X</b> <i>c</i> = <b>no</b> : <b>Bool</b><br>...<br><b>X</b> <i>p</i> : <i>C</i>(<i>c</i>)[<i>c</i>: <b>Bool</b>]</td><td><b>Y</b> ? =<sub><i>reason</i> <b>yes</b></sub></td><td><b>X</b> <i>p</i><sub>1</sub>: <i>C</i>(<b>yes</b>)<br><b>Y</b> ? =<sub><i>reason</i> <b>no</b></sub></td></tr></tbody></table>

**Note:**

In a play, given the statements **P**<i>p</i><sub>1</sub>: <i>C</i>(**yes***) or **P**<i>p</i><sub>2</sub>: <i>C</i>(**no***) (**P**-defences in the equality rules), the play would continue with **O** challenging the elementary statement according to the attack prescribed by the general Socratic rule (see SR5: Socratic rule and definitional equality in section VII.2.1).

## Specific Socratic rule for **Bool** and Boolean operators

When **O** states **a**: **Bool**, she is stating that **a** is an element of **Bool**, that is, she is committing to **a** being either **yes** or **no**; **P** may challenge this **O**-statement by requesting that she makes her commitment explicit and provides the equality **a = yes : Bool** or **a = no : Bool**. The following table provides the dialogical rule for this interaction; this
rule is part of the Socratic rules because it is player dependent,<fnref n="133" /> but it is a rule specific to **Bool** and the Boolean operators thus providing their specific meaning: this specific Socratic rule for **Bool** and the Boolean operators provides their material meaning.

<table><caption>Table 32: Specific Socratic rule for **Bool**</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="2">Specific Socratic rule<br>for Bool</th><td rowspan="2">O a: Bool</td><td rowspan="2">P ? = a<sup>Bool</sup></td><td>O a = yes: Bool</td></tr><tr><td>O a = no: Bool</td></tr></tbody></table>

We can now introduce quite smoothly the rules for the classical truth-functional connectives as operations between elements of **Bool** (left-hand side of the colon), which are distinct from the usual propositional connectives (right-hand side of the colon). We leave the description for quantifiers to the diligence of the reader, whereby the universal quantifier is understood as a finite sequence of products, and, dually, the existential as a finite sequence of additions.

The dialogical interpretation of the rules below is very close to the usual one: it amounts to the commitments and entitlements specified by the rules of the dialogue: if for instance the response is **yes** to a (left-hand side) product, then the speaker is also committed to answer **yes** to further questions on both of the components of that product. Here again, the meaning of the connectives is provided by interaction, where *choice* is a fundamental feature.

<table><caption>Table 33: Global rules for classical truth-functional operators</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Move</th><th colspan="2">Synthesis of local reasons</th><th rowspan="2">Synthesis of<br>strategic reasons</th></tr><tr><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Product</th><td>X a × b: Bool</td><td>Y ? = a × b</td><td>X (a × b) = yes: Bool<br>X (a × b) = no: Bool</td><td>P yes [[a = yes, b = yes]]<sup>0</sup><br>: Bool<br>P no [[a = no | b = no]]<sup>0</sup>: Bool</td></tr><tr><th>Yes-equality<br>(product)</th><td>X (a × b) = yes: Bool</td><td>Y ? L<sup>x</sup> yes<br>Y ? R<sup>x</sup> yes</td><td>X a = yes: Bool<br>X b = yes: Bool</td><td></td></tr><tr><th>No-equality<br>(product)</th><td>X (a × b) = no: Bool</td><td>Y ?<sup>x</sup> no</td><td>X a = no: Bool<br>X b = no: Bool</td><td></td></tr><tr><th rowspan="2">Addition</th><td rowspan="2">X a + b: Bool</td><td rowspan="2">Y ? = a + b</td><td>X a = yes: Bool<br>X b = yes: Bool</td><td>P yes [[a = yes | b = yes]]<sup>0</sup>: Bool<br>P no [[a = no, b = no]]<sup>0</sup>: Bool</td></tr><tr><td></td><td></td></tr></tbody></table>

<footnote n="133">¹³³ For a discussion on player dependence and the way this feature divides the Structural rules and the Particle rules, see section XI.3.</footnote>
<table><tbody><tr><td rowspan="2">Yes-equality (addition)</td><td rowspan="2">X (a + b) = yes: Bool</td><td>Y<sup>+</sup> yes</td><td>X a = yes: Bool</td><td rowspan="2"></td></tr><tr><td></td><td>X b = yes: Bool</td></tr><tr><td rowspan="2">No-equality (addition)</td><td rowspan="2">X (a + b) = no: Bool</td><td>Y<sup>?</sup> L<sup>+</sup>no</td><td>X a = no: Bool</td><td rowspan="2"></td></tr><tr><td>Y<sup>?</sup> R<sup>+</sup>no</td><td>X b = no: Bool</td></tr><tr><td rowspan="2">Implication</td><td rowspan="2">X a → b: Bool</td><td>Y<sup>?</sup> = a → b</td><td>X(a → b) = yes: Bool</td><td>P yes [[<a = yes, b = yes> | <b = no, a = no>]]<sup>0</sup>: Bool</td></tr><tr><td></td><td>X(a → b) = no: Bool</td><td>P no [[<a = yes, b = no>]]<sup>0</sup>: Bool</td></tr><tr><td rowspan="2">Yes-equality (implication)</td><td rowspan="2">X (a → b) = yes: Bool</td><td>Y a = yes: Bool</td><td>X b = yes: Bool</td><td rowspan="2"></td></tr><tr><td>Y b = no: Bool</td><td>X a = no: Bool</td></tr><tr><td rowspan="2">No-equality (implication)</td><td rowspan="2">X (a → b) = no: Bool</td><td>Y<sup>?</sup> L<sup>→</sup>no</td><td>X a = yes: Bool</td><td rowspan="2"></td></tr><tr><td>Y<sup>?</sup> R<sup>→</sup>no</td><td>X b = no: Bool</td></tr><tr><td rowspan="2">Negation</td><td rowspan="2">X<sup>~a</sup>: Bool</td><td>Y<sup>?</sup>~a</td><td>X<sup>~a</sup> = yes: Bool</td><td>P yes [[a = no]]<sup>0</sup>: Bool</td></tr><tr><td></td><td>X<sup>~a</sup> = no: Bool</td><td>P no [[a = yes]]<sup>0</sup>: Bool</td></tr><tr><td>Yes-equality (negation)</td><td>X<sup>~a</sup> = yes: Bool</td><td>Y<sup>?</sup>~ yes</td><td>X a = no: Bool</td><td></td></tr><tr><td>No-equality (negation)</td><td>X<sup>~a</sup> = no: Bool</td><td>Y<sup>?</sup>~ no</td><td>X a = yes: Bool</td><td></td></tr></tbody></table>

Reading the strategic reason for the product:

If both of the components of the product are affirmative (yes answer), that is if O has at some point stated both, then the recapitulation answer is yes: Bool, provided these O statements—[[<a = yes, b = yes>]]<sup>0</sup>. If at least one of the two components is a denial, that is if O has at some point stated one or the other, then the recapitulation answer is no: Bool, provided one of these O statements—[[a = no | b = no]]<sup>0</sup>.

## X.2 Material dialogues through identity and equality

From the CTT perspective, the identity predicate *Id* should be differentiated from

1. definitional equality, which does not express a proposition but introduces real definitions and establishes equivalence relations between pieces of evidence (proof-objects),

2. nominal definitions, which produces linguistic abbreviations, and

3. equality (or Identity) as a relation building up a proposition, that is, the relation we know from first-order logic, and which constitutes a proposition.
We therefore distinguish between

1. the real definition or judgemental equality $a = b: A$;

2. the nominal definition, for example "1" stands for successor of "s(0)";

3. the propositional identity $c: a =_A b$, or better $c: \mathbf{Id}(A, a, b)$.

In a dialogical setting,

* real definitions express at the object-language level **P**'s right to state **b**, **O** having already stated both, **a** and that **a** defines **b**. So **P**'s move $a = b: A$, responding to **O**'s request of justification for **b**: **A**, can be read as "you just conceded **a**: **A**, and furthermore you conceded that **a** defines **b**".

* Nominal definitions allows **P** to deploy the abbreviations established in such kinds of definition.

* **P** is allowed to state the Identity $\mathbf{Id}(A, a, b)$ only if he can state that $c$ is equal to the local (reflexivity) reason $\mathbf{refl}(A, a)$ —that is if he can state $\mathbf{refl}(B, a) = c: \mathbf{Id}(A, a, b)$—, and if he can show that the equality $a = b: B$ presupposed by the formation of $\mathbf{Id}(A, a, b)$ has been fulfilled.

### X.2.1 The generation of Id

The identity predicate $\mathbf{Id}(x, y, z)$, where $x$ is a **set**—or a **prop**—and $y$ and $z$ are local reasons for $x$, can be read as “$y$ is identical to $z$ within $x$.” The dialogical meaning explanation of this identity predicate is provided below through the different rules governing its use (formation rule and Specifi Socratic rule for **Id**), but can be grasped through this fact that **X**'s entitlement to state $\mathbf{Id}(A, a, b)$—“**a** is identical to **b** within **A**”—for instance, presupposes that **a**: **A** and that **b**: **A**, which is precisely its formation rule:

<table><caption>Table 34: Formation rule for **Id**</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="3">Formation of the identity predicate</th><td rowspan="3">X Id(A, a<sub>i</sub>, a<sub>j</sub>) : prop</td><td>Y<sub>?F1</sub> Id</td><td>X A : set</td></tr><tr><td>Y<sub>?F2</sub> Id</td><td>X a<sub>i</sub> : A</td></tr><tr><td>Y<sub>?F3</sub> Id</td><td>X a<sub>j</sub> : A</td></tr></tbody></table>

The three available challenges for the statement that $\mathbf{Id}(A, a_i, a_j) : prop$ correspond to the three presuppositions for this statement, namely that the first argument is a **set**, and that the second and third arguments are members of the first argument.

Since the basic cases of **Id**-statements involve elementary propositions, the rules prescribing the dialogical interaction for this kind of statements must be handled by a Socratic rule specific to that predicate (thus providing material meaning). In the case of **Id**, **O**'s identity statements can only be challenged by two means: either the rule of Global analysis, or the Leibniz-substitution rule. We will now provide these Specific Socratic rules for **Id**.

#### X.2.1.1 SR-Id.1 Specific Socratic rules for $\mathbf{Id}(A, a, a)$

If **P** states $\mathbf{Id}(A, a, a)$, then he must bring forward the definitional equality that conditions statements of propositional intensional identity. Furthermore, the statement
P ! *Id*(*A*, *a*, *a*) commits the Proponent to make explicit the local reason behind his statement, namely, the local reason *refl*(*A*, *a*) specific to *Id*-statements, whose internal structure only depends on *a*.

Thus, the dialogical meaning of the instruction *refl*(*A*, *a*) amounts to prescribing the definitional equality *a* = *refl*(*A*, *a*) : *A* as defence to the challenge *O* ? = *refl*(*A*, *a*) . The following table displays the global rules that implement those prescriptions.

<table><caption>Table 35: Specific Socratic rule for the global synthesis of the local reason for P!Id(A, a, a) and the rules of equality</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Identity predicate (for reflexivity)</th><td>P ! Id(A, a, a)</td><td>O ?<sub>reason</sub> Id</td><td>P refl(A, a) : Id(A, a, a)</td></tr><tr><th rowspan="2">Rules of equality</th><td>P refl(A, a) : Id(A, a, a)</td><td>O ? = refl(A, a)</td><td>P a = refl(A, a) : A</td></tr><tr><td>P a = refl(A, a) : A</td><td>O ? = a</td><td>P a = a : A</td></tr></tbody></table>

**Note:**

This rule presupposes that the well-formation of *Id*(*A*, *a*, *a*) has been established. What is more, notice that the two lines for the rules of equality follow each other: the defence that P must bring forward to answer the first challenge is the object of the second challenge. For an application of these rules, see below, section X.2.3.

The last line is just applying the general Socratic rule for local reasons to the specific case of *refl*(*A*, *a*), and shows that the local reason *refl*(*A*, *a*) is in fact equal to *a* (see section VII.2.1).

### Challenging O-elementary statements

Since in dialogues for immanent reasoning it is *O* who is given the authority to set the local reasons for the relevant sets, P can always trigger from *O* the identity statement *O* p : *Id*(*A*, *a*, *a*) for any statement *O* a : *A* brought forward during a play. This leads to the next table that constitutes one of the exceptions to the interdiction on challenges of *O*'s elementary statements.

<table><caption>Table 36: Specific Socratic rule for triggering the reflexivity move O!Id(A, a, a)</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>O-elementary statements I</th><td>O a : A</td><td>P ? Id</td><td>O refl(A, a) : Id(A, a, a)</td></tr></tbody></table>

**Remark**

Notice that it looks as if P would not need to use this rule since according to the rule for the synthesis of the local reason for a P-identity statement, he can always state *Id*(*A*, *a*, *a*), provided *O* stated *a* : *A*. However, in some cases such as when carrying out a substitution based on identity, P might need *O* to make an explicit statement of identity suitable for applying a substitution rule.
The next rule (global analysis of **O** *p*: **Id**(A, a, a)), also allows **P** to challenge an **O**-elementary statement by prescribing how to analyse a local reason *p* brought forward by **O** in order to support the statement **Id**(A, a, a).

<table><caption>Table 37: Analysis I: The Global Analysis of **O** *p*: **Id**(A, a, a)</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Analysis of<br>**O**-elementary<br>statements</th><td><strong>O</strong> *p*: **Id**(A, a, a)</td><td><strong>P</strong> ? = *p</td><td><strong>O</strong> *p* = <strong>refl</strong>(A, a): **Id**(A, a, a)</td></tr></tbody></table>

The second rule for analysis involves statements of the form **Id**(A, a, b), so we need general rules for statements that are not restricted to reflexivity. In fact the rules for **Id**(A, a, b) can be obtained by re-writing the previous rules—with the exception of the rule that triggers statements of reflexivity by **O**.

We will not spell out the rules for **Id**(A, a, b), but let us stress two important points:

(1) the unicity of the local reason **refl**(A, a);

(2) the non-inversibly of the intensional predicate of identity in relation to judgmental equality.

In relation to the first remark, the unicity of the local reason **refl**(A, a), the point is that the local reason produced by a process of synthesis for any identity statement is always **refl**(A, a). In other words, the local reason prescribed by the procedures of synthesis involving the statement ! **Id**(A, a, a) and the statement **Id**(A, a, a), is the *same one*, namely **refl**(A, a).

In relation to the second point, the non-inversibly of the intensional predicate of identity in relation to judgmental equality, it is important to remember that the *global synthesis* rule refers to the commitments undertaken by **P** when he affirms the identity between *a* and *b*. Such commitment amounts to i) providing a local reason for such an identity, and ii) stating *a* = *b*: *A*.

On the contrary, the rule of *global analysis of an O-identity statement* prescribes what **P** may require from **O**'s statement. In that case, **P** cannot force **O** to state *a* = *b*: *A* on the sole basis of her having stated **Id**(A, a, b): this would only be possible with the so-called extensional version of propositional identity—see section X.2.4, or (Nordström, Petersson, & Smith, 1990, pp. 57-61) for a thorough discussion.

The dialogical view of non-reversibility here is that the *rule of synthesis sets the conditions P must fulfil* when he states and identity, not *what follows from his statement of identity*.

## X.2.2 Global Analysis II: Leibniz's substitution rule for **Id**

Assume that **O** has stated the propositional identity of *a* and *b*, that is, **O**! **Id**(A, a, b), as well as *d*: **B**(a); **P** can then force her to further state **B**(b), by requesting a substitution of indistinguishables. The following table displays the dialogical take on Leibniz-substitution-rule in the context of **Id**-statements.

<table><caption>Table 38: Leibniz-substitution for **Id**</caption><thead><tr><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead></table>
<table><tr><td>Leibniz-substitution for <b>Id</b></td><td><b>O</b> c: <b>Id</b>(A, a, b)<br/>...<br/><b>O</b> d: B(a)<br/>The rule assumes<br/>a: A, b: A, and<br/>B(x): prop [x: A]</td><td><b>P</b>?<sub>Lbz-Id</sub> b/a<br/>Apply<br/>substitution!</td><td><b>O</b> Lbz-<b>Id</b>-subst(c, d): B(d)<br/>Application of substitution</td></tr></table>

The substitution rule allows the development of a play where **P** brings forward *Lbz-Id-subst(c, d)* in order to defend his statement *B(a)*. Such kind of plays do not stop (like in the case of formal dialogues) with the affirmation of a definitional reflexivity of the form *Lbz-Id-subst(c, d) = Lbz-Id-subst(c, d): B(a)*; the aim of the play is rather to make it explicit, by means of a series of equalities, that the local reason *Lbz-Id-subst(c, d)* for *B(b)*, is ultimately equal to the one for *B(a)*, since **O** stated that *a* and *b* are indistinguishable local reasons in *A*.

More precisely, the structure of the play should make it patent that the local reason for *B(b)*, if based on an application of the Leibniz substitution rule for **Id**, is *Lbz-Id-subst(c, d) = d(a): B(b)*, and that the latter is constituted by the definitional equalities *refl(A, a) = c [O c: Id(A, a, b): A]* and *d = d(a/x): B(a/x) [a/x: A]*.

The table below displays the full-version of the sequence of moves that leads to such a definitional equality. The table starts with a statement of the form **P! B(b)**, and the challenge **O?_reason B(b)**, but is *mutatis mutandis* similarly applicable if the starting statement is **P I: B(b)** and the challenge is **O? = I**—where **I** stands for some instruction.

In practice, we might display a shortened version so that when **P** brings forward *Lbz-Id-subst(c, d)* in order to defend his statement *B(a)*, the response to the challenge **O? = Lbz-Id-subst(c, d): B(b)** is the non-reflexive definitional equality *Lbz-Id-subst(c, d) = d(a): B(b)* and then we stop.

<table><caption>Table 39: *Lbz-Id-subst* and *Definitional Equality*</caption><thead><tr><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><td><b>P</b>! B(b)</td><td><b>O</b>?<sub>reason</sub> B(b)</td><td><b>P</b> Lbz-<b>Id</b>-subst(c, d): B(b)</td></tr><tr><td><b>P</b> Lbz-<b>Id</b>-subst(c, d): B(b)</td><td><b>O</b>?<br/>= Lbz-<b>Id</b>-subst(c, d): B(b)</td><td><b>P</b> Lbz-<b>Id</b>-subst(c, d)<br/>= Lbz-<b>Id</b>-subst(c, d): B(b)<br/>Provided that<br/><b>O</b> Lbz-<b>Id</b>-subst(c, d): B(b)</td></tr><tr><td><b>P</b> Lbz-<b>Id</b>-subst(c, d)<br/>= Lbz-<b>Id</b>-subst(c, d): B(b)</td><td><b>O</b>? = c</td><td><b>P</b> refl(A, a) = c : A<br/>Provided that<br/><b>O</b> c: <b>Id</b>(A, a, b)</td></tr><tr><td><b>P</b> Lbz-<b>Id</b>-subst(c, d): B(b)<br/>...<br/><b>P</b> refl(A, a) = c : A<br/>[<b>O</b> c: <b>Id</b>(A, a, b)]</td><td><b>O</b>? refl(A, a) / c</td><td><b>P</b> Lbz-<b>Id</b>-subst(refl(A, a), d)<br/>: B(b)</td></tr><tr><td><b>P</b> Lbz-<b>Id</b>-subst(refl(A, a), d)<br/>: B(b)</td><td><b>O</b>? = d</td><td><b>P</b> d = d(a/x): B(a/x)<br/>[a/x: A]</td></tr></tbody></table>
P Lbz-Id-subst(refl(A, a), d)
: B(b)

...

P d = d(a/x): B(a/x)
[a/x : A]

O?

Lbz-Id-subst

(refl(A, a), d) : B(b)

P d(a) = Lbz-Id-subst
(refl(A, a), d) : B(b)

Provided that

O! Id(A, a, b)

**Note**

The statements on lines two and four share a common statement (lines five and six as well). It must however be not only noted that the challenges differ, but also that the object of each of the challenges are different. It is important to realize that these rules do not concern *local meaning* but *global meaning*, which is determined by the evolution of the play. Thus, those challenges targeting pairs of statements such that one member of the pair is different to the other, *do not involve using twice the repetition ranks for challenging the common statement: they are different attacks to different statements*.

The Leibniz-elimination rule can be inferred from a more general rule provided by (Nordström, Petersson, & Smith, 1990, p. 58). This general rule includes cases of applying substitution to judgements of the form *B(c)* that expresses that some property holds of some non-canonical proof-object *c* for an identity judgement. Thus, the importance of this form of judgments is that it makes it possible to justify that some property applies to proof-objects of identities. We will however not develop it here.

### X.2.3 Application to Bool: the third (canonical element) excluded

A natural way to combine Boolean operations and elements with propositional connectives is to make use of the identity predicate **Id**.

Let us see how real definitions and identity interact when establishing the validity of the proposition *every element of the set Bool is equal to yes or to no*. That is, let us build the winning strategy for

$$ (\forall x: \mathbf{Bool}) \mathit{Id}(\mathbf{Bool}, x, \mathit{yes}) \lor \mathit{Id}(\mathbf{Bool}, x, \mathit{no}) \mathit{true} $$

Notice that this proposition can be interpreted as the classical third-excluded, this proposition indeed saying that there is no third canonical element in **Bool**beside **yes** and **no**: any element of **Bool** can thus be reduced to either one of them.

We shall proceed as usual by running the plays constituting a **P**-winning strategy (see section VII.5).

While on the one hand winning strategies concern the process of bringing forward the piece of evidence that justifies the proposition involved in the judgement, here *that every element of the set Bool is equal to yes or to no*, on the other hand the commitments engaged in asserting that something is one of the pieces of evidence for **Bool**, say, $a + \sim a : \mathbf{Bool}$, amounts to answering the question, Which of the canonical elements of **Bool** is this piece of evidence equal to? In our case, $a + \sim a = \mathbf{yes} : \mathbf{Bool}$.

Notice that since the set **Bool** contains only two elements, universal quantification over **Bool** can be tested by considering each of the elements of the set, each of them triggering a new play.
Play 17: first play for **Bool** third-excluded

<table><thead><tr><th></th><th colspan="2">O</th><th colspan="2">P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!(∀x : Bool)(Id(Bool, x, yes) ∨ Id(Bool, x, no))</td><td>0</td><td rowspan="2">Thesis</td></tr><tr><td></td><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>Synthesis of local reason for universal quantification (Table 19)</td><td>3</td><td>yes: Bool [δ<sub>1</sub>, ...]</td><td>0</td><td>yes: (Id(Bool, yes, yes) ∨ Id(Bool, yes, no))</td><td>4</td></tr><tr><td>Analysis of local reason for disjunction (Table 20)</td><td>5</td><td>?<sup>V</sup></td><td>4</td><td>L<sup>V</sup>(yes): Id(Bool, yes, yes)</td><td>6</td></tr><tr><td>Resolution of the instruction</td><td>7</td><td>? .../L<sup>V</sup>(yes)</td><td>6</td><td>refl(Bool, yes): Id(Bool, yes, yes)</td><td>8</td><td rowspan="3">Table 35<br>local reason<br>Id(A, a, a)</td></tr><tr><td>Rule of equality (Table 35)</td><td>9</td><td>? = refl(Bool, yes)</td><td>8</td><td>yes = refl(Bool, yes) : Bool</td><td>10</td></tr><tr><td>Rule of equality (Table 35)</td><td>11</td><td>? = yes</td><td>8</td><td>yes = yes: Bool</td><td>12</td></tr></tbody><tfoot><tr><td colspan="6">P wins.</td></tr></tfoot></table>

Play 18: second play for **Bool** third-excluded

<table><thead><tr><th></th><th colspan="2">O</th><th colspan="2">P</th><th></th></tr></thead><tbody><tr><td></td><td></td><td></td><td>!(∀x : Bool)(Id(Bool, x, yes) ∨ Id(Bool, x, no))</td><td>0</td><td></td></tr><tr><td></td><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td><td></td></tr><tr><td></td><td>3</td><td>no: Bool [δ<sub>1</sub>, δ<sub>2</sub>]</td><td>0</td><td>no: (Id(Bool, no, yes) ∨ Id(Bool, no, no))</td><td>4</td></tr><tr><td></td><td>5</td><td>?<sup>V</sup></td><td>4</td><td>R<sup>V</sup>(no): Id(Bool, no, no)</td><td>6</td></tr><tr><td></td><td>7</td><td>? .../L<sup>V</sup>(no)</td><td>6</td><td>refl(Bool, no): Id(Bool, no, no)</td><td>8</td></tr><tr><td></td><td>9</td><td>? = refl(Bool, no)</td><td>8</td><td>no = refl(Bool, no): Bool</td><td>10</td></tr><tr><td></td><td>11</td><td>? = no</td><td>8</td><td>no = no: Bool</td><td>12</td></tr></tbody><tfoot><tr><td colspan="6">P wins</td></tr></tfoot></table>

Since every **O**-decision option has been considered with plays $\mathcal{P}_1$ and $\mathcal{P}_2$, which are both **P**-terminal, **P** has a winning strategy for $(\forall x : \mathbf{Bool})(\mathbf{Id}(\mathbf{Bool}, x, \mathbf{yes}) \lor \mathbf{Id}(\mathbf{Bool}, x, \mathbf{no}))$, which is thus demonstrated (see chapter IX).

Notice that, in this framework, though it is trivial to show

$$P a + \sim a = \mathbf{yes} : \mathbf{Bool}$$

we cannot build a winning strategy for:

$$!(\forall x : \mathbf{Bool})(\mathbf{Id}(\mathbf{Bool}, x, \mathbf{yes}) \lor \neg \mathbf{Id}(\mathbf{Bool}, x, \mathbf{yes}))$$

unless we presuppose $\neg \mathbf{Id}(\mathbf{Bool}, \mathbf{no}, \mathbf{yes})$. This will be discussed in the next section.

### X.2.4 The extensional propositional identity Eq

The dialogical rules that prescribe the extensional propositional identity Eq are simpler than the other forms of equality. Once **O** stated an extensional propositional identity, **P** is allowed to ask him to state a definitional equality involving the terms of the
relation **Eq.** Thus, the rules that prescribe statements of the form **Eq(A, a, b)** are the same for **P** and **O**. However, the local reason for the resulting proposition, namely the local reason **eq** for **Eq(A, a, b)**; yet the analysis of **eq** does not render the local reasons involved in the definitional equality **a** = **b** : **A** on the basis of which the predicate **Eq** has been stated: **eq** is thus a kind of analogue of ontological equality. Moreover, every local reason **c** for **Eq(A, a, b)** is definitionally equal to **eq**.

<table><caption>Table 40: Formation rules for Eq</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="3">Eq-formation</th><td rowspan="3">X Eq(A, a<sub>i</sub>, a<sub>j</sub>) : prop</td><td>Y<sub>?F1</sub> Eq</td><td>X A: set</td></tr><tr><td>Y<sub>?F2</sub> Eq</td><td>X a<sub>i</sub>: A</td></tr><tr><td>Y<sub>?F3</sub> Eq</td><td>X a<sub>j</sub>: A</td></tr></tbody></table>

Since we are dealing with formation plays, these challenges can all be carried out without requiring the use of repetition ranks.

<table><caption>Table 41: Specific Socratic rule for the Global Synthesis of the local reason for X! Eq(A, a, a)</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="2">Socratic rule</th><td>X! Eq(A, a<sub>i</sub>, a<sub>j</sub>)</td><td>Y<sub>?reason</sub> Eq</td><td>X eq : Eq(A, a<sub>i</sub>, a<sub>j</sub>)</td></tr><tr><td>P eq : Id(A, a, a)</td><td>O? = eq</td><td>P eq = eq : A</td></tr></tbody></table>

Notice that the crucial difference between the **Id** and **Eq** is that the rules of synthesis are formulated as player-independent. In the context of an **Id**-statement, **P** cannot force **O** to bring forward **a** = **b** : **A** after **O eq: Eq(A, a, b)**, whereas in the context of **Eq**, **P** can. Moreover, the definitional equality of **eq** is **eq**, which is responsible for the "extensionality" of **Eq** and leads to the undecidability of assertions of the form **a** = **b** : **A**—see chapter II.

The rest of the rules follow from adapting the tables for **Id** to **Eq** and **eq**

## X.3 Mathematics and logic

### X.3.1 Material dialogues for $\mathbb{N}$

Let us display the main specifications yielding material dialogues for the natural numbers. Since we are in the presence of material dialogues, we need to "harmonize" the rules of synthesis and analysis with equality rules specific to $\mathbb{N}$. Moreover, the development of a play that includes statements of the form $Pn: \mathbb{N}[0: \mathbb{N}]$ might presuppose some particular nominal definitions that must be described by the structural rules. In the following sections we display the corresponding tables for synthesis, analysis, and equality, and the set of structural rules for the development of a play based on nominal definitions for 1, 2, ... : $\mathbb{N}$.
### Synthesis of N

If $X$ states that $n$ is a natural number, he is committed to the further statement that its successor is also a natural number.

<table><caption>Table 42: Synthesis of N</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Synthesis of N</th><td><b>X</b> n: N</td><td><b>Y</b> ? <i>s</i>(n)</td><td><b>X</b> <i>s</i>(n): N</td></tr></tbody></table>

### Analysis of N

If $X$ states that the property $C$ applies to any natural number $n$, then $X$ must also state

1. that it applies to 0 and

2. that it also applies to $C(s(m))$, for any $m$ chosen by $Y$.

Thus, the local reason $p$ is constituted by a *left component* locally grounding the statement $C(0)$, and a *right component*. Thus, two analysis rules are due, the first prescribing the moves yielding the left component of $p$, and the second those for the right component. The analysis for the right component requires analyzing this right component of $p$ into two further components, namely,

1. the left component of the right component of $p$, which provides the local reason for $Y$'s statement that the property $C$ applied to $m$; and

2. the right component of the right component of $p$, which provides a local reason for $X$'s statement that $C$ also applies to the successor of $m$.

<table><caption>Table 43: Analysis rules of N</caption><thead><tr><th></th><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="2">Analysis of N</th><th>Left</th><td><b>X</b> p: <i>C</i><sup>N</sup>(n)<br>For arbitrary n: N,<br>given <i>C</i>(z): <b>set</b> [z: N]</td><td><b>Y</b> ? <i>L</i><sup>N</sup><sub>df</sub> <i>C</i></td><td><b>X</b> <i>L</i><sup>N</sup>(p)<sup>X</sup>: <i>C</i>(0)</td></tr><tr><th>Right</th><td><b>X</b> p: <i>C</i><sup>N</sup>(n)<br>...<br><b>X</b> <i>L</i><sup>N</sup>(p)<sup>X</sup>: <i>C</i>(0)<br>For arbitrary n: N, and<br>given <i>C</i>(z): <b>set</b> [z: N]</td><td><b>Y</b> <i>L</i> (<i>R</i><sup>N</sup>(p))<sup>Y</sup>: <i>C</i>(m<sup>Y</sup>)<br>For arbitrary m: N,<br>chosen by <b>Y</b></td><td><b>X</b> <i>R</i> (<i>R</i><sup>N</sup>(p))<sup>X</sup>: <i>C</i>(<b>s</b>(m<sup>Y</sup>))</td></tr></tbody></table>

### Specific Socratic rules for N

The rules for definitional equality assume that $O$ brought forward $p_1$ and $p_2$ as local reasons for $C(0)$ and $C(s(m))$ respectively.

<table><caption>Table 44: Specific Socratic rules for N</caption><thead><tr><th></th><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Socratic rules</th><th>Definitional equality I</th><td><b>P</b> p<sub>1</sub>: <i>C</i>(0)</td><td><b>O</b> ? = p<sub>1</sub></td><td><b>P</b> p<sub>1</sub><sup>O</sup> = <i>L</i><sup>N</sup>(p): <i>C</i>(0)</td></tr></tbody></table>
<table><tr><td>for N</td><td>Definitional equality II</td><td>P p<sub>2</sub> : C(s(m))</td><td>O ? = p<sub>2</sub></td><td>P p<sub>2</sub><sup>o</sup> = R(R<sup>N</sup>(p)) : C(s(m))</td></tr></table>

**Rules specific to C**

Y's challenge upon $C(n)$ is specifically defined for $C$. Thus, if $C$ is the predicate “$x$ is an odd number”, the rule establishes that the challenge upon, say, $C(s(0))$ is choose an $x$ such that $\mathbf{Id}(\mathbb{N}, (s(0), 2 \cdot x^x + 1))^{134}$

That is, the precise form of the challenge in our case a challenge would be the challenge of the existential:

$$ \mathbf{X}!(\exists x: \mathbb{N}) \mathbf{Id}(\mathbb{N}, (s(0), 2 \cdot x^x + 1)) $$

The response would assume that $n$ stands for $s(0)$, and that $C(n)$ stands for “$s(0)$ is an odd number”. This response would thus be the answer to the challenge on the right side of the above existential, the response to the left side being:

$$ \mathbf{X}! 0 : \mathbb{N} $$

Hence, in this example

$$ \mathbf{X} p : C(n) $$

would stand for

$$ \mathbf{X} p: (\exists x: \mathbb{N}) \mathbf{Id}(\mathbb{N}, (s(0), 2 \cdot x^x + 1)) $$

which presupposes

$$ \mathbf{Odd}(s(0)) = (\exists x: \mathbb{N}) \mathbf{Id}(\mathbb{N}, s(0), 2 \cdot x + 1) : \mathbf{prop}[s(0): \mathbb{N}] $$

which presupposes the definition:

$$ \mathbf{Odd}(y) = (\exists x: \mathbb{N}) \mathbf{Id}(\mathbb{N}, y, 2 \cdot x + 1) : \mathbf{prop}[y: \mathbb{N}] $$

**Structural rules for statements of the form P 1 : N [0 : N], P 2 : N [0 : N], ...**

Given a statement of the form $P n: N [0: N]$, where $n$ stands for 1, or 2, or ..., $^{135}$O can challenge it by means of the attack $? n$. If $P$'s initial statement is $1: N [0: N]$, then $P$ can respond to the challenge $? 1$ with $s(0) \equiv_{df} 1: N$ only if $O$ stated $s(0): N$; similarly for 2, and so on. In other words:

$$ \mathbf{P} 1 : \mathbb{N} $$

$$ \mathbf{O} ? 1 $$

$$ \mathbf{O} s(0): \mathbb{N} $$

$$ \mathbf{P} 1 \equiv_{df} s(0): \mathbb{N} $$

$$ \mathbf{P} n : \mathbb{N} $$

$$ \mathbf{O} ? n \qquad \mathbf{O} s(...(s(s(0)))) : \mathbb{N} $$

$$ \mathbf{P} n \equiv_{df} s(...(s(s(0)))) : \mathbb{N} $$

(The answer cannot be challenged.)

**Example**

Let us sketch briefly as an example the play relevant for constituting a winning strategy for the thesis $3: N [0: N]$:

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>3: N [0: N]</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr></tbody></table>

<footnote>$^{134}$ The rule assumes that multiplication and addition have been defined already.</footnote>

<footnote>$^{135}$ This kind of statement can for instance result from defending the left side of an existential such as as $(\exists x: \mathbb{N}) \mathbf{Id}(\mathbb{N}, (s(0), 2 \cdot x^x + 1))$.</footnote>
<table><tr><td>3</td><td>0 : N</td><td></td><td>3 : N</td><td>4</td></tr><tr><td>5</td><td>? 3</td><td>4</td><td>s(s(s(0))) ≡<sub>df</sub> 3 : N</td><td>12</td></tr><tr><td>7</td><td>s(0) : N</td><td></td><td>3</td><td>? s(0)</td></tr><tr><td>9</td><td>s(s(0)) : N</td><td></td><td>7</td><td>? s(s(0))</td></tr><tr><td>11</td><td>s(s(s(0))) : N</td><td></td><td>9</td><td>? s(s(s(0)))</td></tr></table>

P wins.

**Description:**

* **Moves 0-5:** establish the thesis 3 : N, the concession 0 : N, and the challenge ? 3 on the thesis.

* **Moves 6-7:** P applies the rule of synthesis to the concession 0 : N. O responds to it.

* **Moves 8-11:** P applies the rule of synthesis to moves 7 and 9. O responds to them.

* **Move 12:** P applies the nominal definition of "3" established by the Socratic rule and wins responding to the challenge on 5.

### X.3.2 Beyond Bool: Finite Sets and Large Sets of Answers.

Let us now come back to the case of **Bool**. A natural extension of the framework is to have a larger set of answers than just the **yes-no** responses of **Bool**. The interpretation scope offered by the generalization we propose here is quite broad, as it can be interpreted as the different degrees of certainty an answer to a question can take; it can also be understood as encoding different possible answers to a question, so that **0** is the answer **a**, **1** is the answer **b**, and so on (we will discuss some examples in the next section).

Since the formation rule for a finite set $N^n$ of $n$ canonical elements (such that $n$ stands for some natural number) has no premisses in the CTT setting, the dialogical formation rule for it amounts to the following:

<table><caption>Table 45: Formation rule of $N^n$</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Formation of N<sup>n</sup></th><td>X ! N<sup>n</sup></td><td>Y ?<sub>F</sub> N<sup>n</sup></td><td>X N<sup>n</sup> : set</td></tr></tbody></table>

The rules of synthesis and analysis are a straightforward generalization of the set **Bool** (that is the set $N^2$).

<table><caption>Table 46: rules for $N^n$</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Synthesis for N<sup>n</sup></th><td>X ! N<sup>n</sup></td><td>Y ? N<sup>n</sup></td><td>X m<sub>1</sub>: N<sup>n</sup><br>...<br>X m<sub>n</sub>: N<sup>n</sup></td></tr><tr><th>Analysis for N<sup>n</sup><br>and equalities</th><td>X p : C(c) [c : N<sup>n</sup>]</td><td>Y ? = c<sup>N<sup>n</sup></sup></td><td>X c = m<sub>1</sub>: N<sup>n</sup><br>...<br>X c = m<sub>n</sub>: N<sup>n</sup></td></tr></tbody></table>
<table><tr><td>$$ \begin{array}{l} \mathbf{X} c = m_1: \mathbb{N}^n \\ \dots \\ \mathbf{X} c = m_n: \mathbb{N}^n \\ \dots \\ \mathbf{X} p: C(c)[c: \mathbb{N}^n] \end{array} $$</td><td>$$ \begin{array}{l} \mathbf{Y} c: \mathbb{N}^n \\ \dots \\ \mathbf{Y} ?_{\text{reason}} C(c) \end{array} $$</td><td>$$ \begin{array}{l} \mathbf{X} p_1: C(m_1) \\ \dots \\ \mathbf{X} p_n: C(m_n) \end{array} $$</td></tr><tr><td colspan="3">Then the play continues with <b>O</b> challenging the elementary statement according to the attack prescribed by the general Socratic Rule. This procedure yields the remaining equalities.</td></tr></table>

### The case of $\mathbb{N}^0$ and $\mathbb{N}^1$

$\mathbb{N}^0$: following our main interpretation, a statement such as $X! \mathbb{N}^0$ should be understood as stating that there is no local reason that can be adduced for the empty set. From a more dialogical point of view, we can coconsider $\mathbb{N}^0$ as the empty set of possible answers to an enquiry: the player thus states that there is no possible answer or solution to the enquiry at stake. Analogously to the Kolmogorov interpretation of a proposition as a problem associated with all that can count as a solution to it, the natural reading in a dialogical setting would be to understand a proposition as a solution to a problem or enquiry.

Accordingly, the dialogical rule for $\mathbb{N}^0$ is the same as the one for $\perp$, that is the rule for giving up:

* The player who states $\mathbb{N}^0$ (or $p: \mathbb{N}^0$) at move $n$ loses the current play. If it is $\mathbf{O}$ who states it, $\mathbf{P}$ can adduce the local reason $\mathbf{O}$-gives up($n$) in support for any statement that he has not defended before $\mathbf{O}$ stated $\mathbb{N}^0$ at move $n$.

$\mathbb{N}^1$: if $\mathbb{N}^0$ is in fact the empty set $\perp$, then the unary set is $\mathcal{T}$, inhabited by only one local reason, namely *yesyes*: $\mathcal{T}$:

* The player who states $\mathbb{N}^1$, can always adduce *yesyes* as its local reason.

### X.3.3 The set $\mathbf{Bool}$ and some applications to mathematics and logic

#### Universes and codes of sets

The main motivation of introducing *universes* is to have a device for dealing with contexts in which the use of sets of sets is required, though we cannot have the set of all sets, since we cannot describe all the possible ways of constituting a set. However, since sets of sets are particularly useful in the foundations of mathematics, Martin-Löf (1984, pp. 47-49) introduces the notion of *universe of small sets*. A universe $\mathbf{U}$ is a set of codes of sets: $\mathbf{n}^n$ is the code of the set $\mathbb{N}^n$. A small set is a set with a code. The universe $\mathbf{U}$ has no code in $\mathbf{U}$ (otherwise a paradox would follow). The formation of a universe requires a decoding function $\mathcal{T}$ that yields sets from codes, i.e. the evaluation of $\mathcal{T}(\mathbf{n}^k)$ yields the set $\mathbb{N}^k$ whose code is $\mathbf{n}^k$. In the dialogical setting the formation rule can be formulated in the following way:

<table><caption>Table 47: Formation rules for $\mathbf{U}$</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th rowspan="2">Formation of <i>U</i></th><td><b>X</b>! <i>U</i></td><td><b>Y</b>?<sub>F</sub> <i>U</i></td><td><b>X</b> <i>n</i><sup>0</sup>: <i>U</i><br>...<br><b>X</b> <i>n</i><sup><i>k</i></sup>: <i>U</i></td></tr><tr><td><b>X</b> <i>n</i><sup><i>k</i></sup>: <i>U</i></td><td><b>Y</b>?<sub><i>T</i></sub>(<i>n</i><sup><i>k</i></sup>)</td><td><b>X</b> <i>\N</i><sup><i>k</i></sup>: set</td></tr></tbody></table>