inferential pragmatism. However, there are also some significant differences that are at center of the dialogical approach to meaning. The present paper does not discuss explicitly phenomenology, however, one might see our proposal as setting the basis for a further study linking phenomenology and the dialogical conception of meaningthe development of such a link is part of several ongoing researches. different fashion, Hintikka's plea for the fruitfulness of game-theoretical semantics in the context of epistemic approaches to logic, semantics, and the foundations of mathematics. 4 From the dialogical point of view, the actions-such as choices-that the particle rules associate with the use of logical constants are crucial elements of their full-fledged (local) meaning: if meaning is conceived as constituted during interaction, then all of the actions involved in the constitution of the meaning of an expression should be made explicit; that is, they should all be part of the object-language. This perspective roots itself in Wittgenstein's remark according to which one cannot position oneself outside language in order to determine the meaning of something and how it is linked to syntax; in other words, language is unavoidable: this is his Unhintergehbarkeit der Sprache. According to this perspective of Wittgensteins, language-games are supposed to accomplish the task of studying language from a perspective that acknowledges its internalized feature. This is what underlies the approach to meaning and syntax of the dialogical framework in which all the speech-acts that are relevant for rendering the meaning and the "formation" of an expression are made explicit. In this respect, the metalogical perspective which is so crucial for model-theoretic conceptions of meaning does not provide a way out. It is in such a context that Lorenz writes: Also propositions of the metalanguage require the understanding of propositions, […] and thus cannot in a sensible way have this same understanding as their proper object. The thesis that a property of a propositional sentence must always be internal, therefore amounts to articulating the insight that in propositions about a propositional sentence this same propositional sentence does not express a meaningful proposition anymore, since in this case it is not the propositional sentence that is asserted but something about it.

Thus, if the original assertion (i.e., the proposition of the ground-level) should not be abrogated, then this same proposition should not be the object of a metaproposition […]. 5

 was the first to link game-theoretical approaches with CTT. Ranta took Hintikka's (1973) Game-Theoretical Semantics (GTS) as a case study, though his point does not depend on that particular framework: in game-based approaches, a proposition is a set of winning strategies for the player stating the proposition. In game-based approaches, the notion of truth is 4 Cf. Hintikka (1973). 5 Lorenz (1970, p. 75), translated from the German by Shahid Rahman. 6 Lorenz (1970, p. 109), translated from the German by Shahid Rahman.

respectively as on one hand must-requests (commitments or obligations) and on the other mayrequests (or entitlements or rights) as follows:1

[…] So, let's call them rules of interaction, in addition to inference rules in the usual sense, which of course remain in place as we are used to them.

[…] Now let's turn to the request mood. And then it's simplest to begin directly with the rules, because the explanation is visible directly from the rules. So, the rules that involve request are these, that if someone has made an assertion, then you may question his assertion, the opponent may question his assertion.

(Req1)

⊢ 𝐶 ? ⊢ 𝑚𝑎𝑦 𝐶 Now we have an example of a rule where we have a may. The other rule says that if we have the assertion ⊢ 𝐶, and it has been challenged, then the assertor must execute his knowledge how to do 𝐶. [ … ].

(Req2) ⊢ 𝐶 ? ⊢ 𝐶 ⊢ 𝑚𝑢𝑠𝑡 𝐶′
In relation to the third condition of Brandom, endorsement, it involves the use of assertions brought forward by the interlocutor. In this context Göran Sundholm (2013, p. 17) produced the following proposal that embeds Austin's remark (1946, p. 171) on assertion acts in the context of inference:

When I say therefore, I give others my authority for asserting the conclusion, given theirs for asserting the premisses.

Herewith, the assertion of one of the interlocutors entitles the other one to endorse it. Moreover, in recent lectures, Per [START_REF] Martin-Löf | Is Logic Part of Normative Ethics? Lecture Held at the research Unity Sciences, Normes, Décisions (FRE 3593)[END_REF] used this dialogical perspective in order to escape a form of circle threatening the explanation of the notions of inference and demonstration. A demonstration may indeed be explained as a chain of (immediate) inferences starting from no premisses at all. That an inference 𝐽 1 . . . 𝐽 𝑛 𝐽

is valid means that one can make the conclusion (judgement 𝐽) evident on the assumption that 𝐽 1 , … , 𝐽 𝑛 are known. Thus the notion of epistemic assumption appears when explaining what a valid inference is. According to this explanation however, we cannot take 'known' in the sense of demonstrated, or else we would be explaining the notion of inference in terms of demonstration when demonstration has been explained in terms of inference. Hence the threatening circle. In this regard Martin-Löf suggests taking 'known' here in the sense of asserted, which yields epistemic assumptions as judgements others have made, judgements whose responsibility others have already assumed. An inference being valid would accordingly mean that, given others have assumed responsibility for the premisses, I can assume responsibility for the conclusion.

So, again it is the dialogical take on endorsement which is at stake here that amounts to the following: whatever reason the Opponent has for stating some elementary assertion authorizes the Proponent to use it himself. In other words, whatever reason the Opponent adduces for some elementary assertion the Proponent can take it as rendering the asserted proposition true and therefore can now use the same reason for defending his own assertion of that proposition. In doing so, the Proponent attributes knowledge to the Opponent when he asserts some elementary proposition, but the Opponent does nothe is trying to build a counterargument after all. Thus, the dialogical framework already seems to offer a formal system where the main features of Brandom's epistemological games can be rendered explicit. However, the system so far does not make explicit the reasons behind an assertion. In order to do so we need to incorporate into the dialogical framework expressions standing for those reasons. This requires combining dialogical logic with Per Martin Löfs Constructive Type Theory (1984) in a more thorough way.

We call the result of such enrichment of the expressive power of the dialogical framework, dialogues for immanent reasoning precisely because reasons backing a statement, now explicit denizens of the object-language of plays, are internal to the development of the dialogical interaction itselfsee Rahman/McConaugey/Klev/Clerbout (2018). 2However, despite the undeniable links of the dialogical framework to both CTT and Brandom's inferentialist approach to meaning there are also some significant differences that are at the center of the dialogical conception of meaning, namely the identification of a level of meaning, i.e. the play-level, that does not reduce to the proof-theoretical one. We will start by presenting the main features of dialogues for immanent reasoning and then we will come back to the general philosophical discussion on the play-level as the core of what is known as dialoguedefiniteness.

The present paper does not discuss explicitly phenomenology, however, Mohammad [START_REF] Shafiei | Intentionnalité et signification: Une approche dialogique[END_REF] developed in his thesis: Intentionnalité et signification: Une approche dialogique, a thorough study of the bearing of the dialogical framework for phenomenology. Nevertheless, his work did not deploy the new development we call immanent reasoning. So, one might see our proposal as setting the basis for a further study linking phenomenology and the dialogical conception of meaning.

Local reasons

Recent developments in dialogical logic show that the Constructive Type Theory approach to meaning is very natural to the game-theoretical approaches in which (standard) metalogical features are explicitly displayed at the object language-level. 3 This vindicates, albeit in quite a at the level of such winning strategies. Ranta's idea should therefore in principle allow us to apply, safely and directly, instances of game-based methods taken from CTT to the pragmatist approach of the dialogical framework.

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

Fully spelled out it means that for an entity to be a proposition there must exist a dialogue game associated with this entity, i.e., the proposition A, such that an individual play of the game where A occupies the initial position, i.e., a dialogue D(A) about A, reaches a final position with either win or loss after a finite number of moves according to definite rules: the dialogue game is defined as a finitary open two-person zero-sum game. Thus, propositions will in general be dialogue-definite, and only in special cases be either proofdefinite or refutation-definite or even both which implies their being value-definite. A. 7 Given the distinction between the play level and the strategy level, and deploying within the dialogical framework the CTT-explicitation program, it seems natural to distinguish between local reasons and strategic reasons: only the latter correspond to the notion of proof-object in CTT and to the notion of strategic-object of Ranta. In order to develop such a project we enrich the language of the dialogical framework with statements of the form "𝑝 ∶ 𝐴". In such expressions, what stands on the left-hand side of the colon (here 𝑝) is what we call a local reason; what stands on the right-hand side of the colon (here 𝐴) is a proposition (or set).

Within this game-theoretic framework […] truth of A is defined as existence of a winning strategy for A in a dialogue game about A; falsehood of A respectively as existence of a winning strategy against

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

The most basic contribution of a local reason is its contribution to a dialogue involving an elementary proposition. Informally, we can say that if the Proponent P states the elementary proposition 𝐴, it is because P claims that he can bring forward a reason in defence of his statement, it is this reason that provides content to the proposition.

Local meaning and local reasons

Statements in dialogues for immanent reasoning

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

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

Adding concessions

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

X ! (x 1 , …, x n ) [x i : A i ]
where "" stands for some statement in which (x 1 , …, x n ) ocurs, and where [x i : A i ] stands for some condition under which the statement (x 1 , …, x n ) has been brought forward. Thus, the statement reads: X states that (x 1 , …, x n ) under the condition that the antagonist concedes x i : A i .

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

Formation rules for local reasons: an informal overview

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

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

These considerations yield the following condensed presentation of the logical constants (plus falsum), in which "K" in AKB"expresses a connective, and "Q" in "(Qx : A) B(x) " expresses a quantifier.

Formation rules, condensed presentation

Connective

Quantifier Falsum Move X AKB : prop X (Qx :

A) B(x) : prop X  : prop Challenge Y ? F K 1
and/or

Y ? F K  Y ? F Q 1 and/or Y ? F Q  - Defence X A : prop (resp.) X B : prop X A : set (resp.) X B(x) : prop (x : A) -

Synthesis of local reasons

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

Implication

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

i. that the challenger Y must state the antecedent (while providing a local reason for it): Y p 1 : A 8 ii.

that the defender X must respond to the challenge by stating the consequent (with its corresponding local reason): X p 2 : B. In other words, the rules for the synthesis of a local reason for implication are as follows:

Synthesis of a local reason for implication

Implication

Move X ! AB Challenge Y p 1 : A Defence X p 2 : B
Notice that the initial statement (X ! AB) does not display a local reason for the claim the the implication holds: player X simply states that he has some reason supporting the claim. We express such kind of move by adding an exclamation mark before the proposition. The further dialogical actions indicate the moves required for producing a local reason in defence of the initial claim.

Conjunction

The synthesis rule for the conjunction is straightforward:

Synthesis of a local reason for conjunction

Conjunction

Move X ! 𝐴 ∧ 𝐵 Challenge Y ? 𝐿 ∧ or Y ? 𝑅 ∧  Defence X 𝑝 1 : 𝐴 (resp.) X 𝑝 2 : 𝐵

Disjunction

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

Synthesis of a local reason for disjunction

Disjunction

Move X ! 𝐴 ∨ 𝐵 Challenge Y ? ∨  Defence X 𝑝 1 : 𝐴 or X 𝑝 2 : 𝐵
The general structure for the synthesis of local reasons More generally, the rules for the synthesis of a local reason for a constant K is determined by the following triplet: General structure for the synthesis of a local reason for a constant

A constant K Implication Conjunction Disjunction Move X ! K X claims that 𝜙 X ! AB X ! 𝐴 ∧ 𝐵 X ! 𝐴 ∨ 𝐵

Analysis of local reasons

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

Approaching the analysis rules for local reasons

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

Move X ! (A∧B)B

Challenge Y p 1 : A∧B Recall that the synthesis rule prescribes that X must now provide a local reason for the consequent; but instead of defending his implication (with 𝐗 𝑝 2 : 𝐵 for instance), X can choose to parse the reason p 1 provided by Y in order to force Y to provide a local reason for the right-hand side of the conjunction that X will then be able to copy; in other words, X can force Y to provide the local reason for B out of the local reason 𝑝 1 for the antecedent 𝐴 ∧ 𝐵 of the initial implication. The analysis rules prescribe how to carry out such a parsing of the statement by using instructions. The rule for the analysis of a local reason for the conjunction 𝑝 1 : 𝐴 ∧ 𝐵 will thus indicate that its defence includes expressions such as  the left instruction for the conjunction, written 𝐿 ∧ (𝑝 1 ), and  the right instruction for the conjunction, written 𝑅 ∧ (𝑝 1 ). These instructions can be informally understood as carrying out the following step: for the defence of the conjunction 𝑝 1 : 𝐴 ∧ 𝐵 separate the local reason 𝑝 1 in its left (or right) component so that this component can be adduced in defence of the left (or right) side of the conjunction.

Here is a play with local reasons for the thesis (𝐴 ∧ 𝐵) ⊃ 𝐵 using instructions:

O P ! (𝐴 ∧ 𝐵) ⊃ 𝐵 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 3 𝑝 1 ∶ 𝐴 ∧ 𝐵 0 𝑅 ∧ (𝑝 1 ) ∶ 𝐵 6 5
𝑅 ∧ (𝑝 1 ) ∶ 𝐵 3 ? 𝑅 ∧ 4 P wins. In this play, P uses the analysis of local reasons for conjunction in order to force O to state 𝑅 ∧ (𝑝 1 ) ∶ 𝐵, that is to provide a local reason9 for the elementary statement 𝐵; P can then copy that local reason in order to back his statement 𝐵, the consequent of his initial implication. With these local reasons, we explicitly have in the object-language the reasons that are given and asked for and which constitute the essence of an argumentative dialogue.

The general structure for the analysis rules of local reasons

Move

Challenge Defence

Interaction procedures embedded in instructions

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

1. Resolution of instructions: this procedure determines how to carry out the instructions prescribed by the rules of analysis and thus provide an actual local reason. 2. Substitution of instructions: this procedure ensures the following; once a given instruction has been carried out through the choice of a local reason, say b, then every time the same instruction occurs, it will always be substituted by the same local reason b. 3. Application of the Socratic rule: the Socratic rule prescribes how to constitute equalities out of the resolution and substitution of instructions, linking synthesis and analysis together.

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

From Reasons to Equality: a new visit to endorsement

One of the most salient features of dialogical logic is the so-called, Socratic rule (or Copycat rule or rule for the formal use of elementary propositions in the standard-that is, non-CTTcontext), establishing that the Proponent can play an elementary proposition only if the Opponent has played it previously.

The Socratic rule is a characteristic feature of the dialogical approach: other game-based approaches do not have it and it relates to endorsing condition mentioned in the introduction. With this rule the dialogical framework comes with an internal account of elementary propositions: an account in terms of interaction only, without depending on metalogical meaning explanations for the non-logical vocabulary.

The rule has a clear Platonist and Aristotelian origin and sets the terms for what it is to carry out a formal argument: see for instance Plato's Gorgias (472b-c). We can sum up the underlying idea with the following statement: there is no better grounding of an assertion within an argument than indicating that it has been already conceded by the Opponent or that it follows from these concessions. 10 What should be stressed here are the following two points:

1. formality is understood as a kind of interaction; and 2. formal reasoning should not be understood here as devoid of content and reduced to purely syntactic moves.

Both points are important in order to understand the criticism often raised against formal reasoning in general, and in logic in particular. It is only quite late in the history of philosophy that formal reasoning has been reduced to syntactic manipulation-presumably the first explicit occurrence of the syntactic view of logic is Leibniz's "pensée aveugle" (though Leibniz's notion was not a reductive one). Plato and Aristotle's notion of formal reasoning is neither "static" nor "empty of meaning". In the Ancient Greek tradition logic emerged from an approach of assertions in which meaning and justification result from what has been brought forward during 10 Recent researches on deploying the dialogical framework for the study of history of logic claim that this rule is central to the interpretation of dialectic as the core of Aristotle's logicsee Crubellier (2014, pp. 11-40) and [START_REF] Marion | Aristotle on universal quantification: a study from the perspective of game semantics[END_REF].

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

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

Statements of definitional equality emerge precisely at this point. In particular reflexivity statements such as p = p : A express from the dialogical point of view the fact that if O states the elementary proposition A, then P can do the same, that is, play the same move and do it on the same grounds which provide the meaning and justification of A, namely p.

These remarks provide an insight only on simple forms of equality and barely touch upon the finer-grain distinctions discussed above; we will be moving to these by means of a concrete example in which we show, rather informally, how the combination of the processes of analysis, synthesis, and resolution of instructions lead to equality statements.

Example

Assume that the Proponent brings forward the thesis (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴):

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0
Both players then choose their repetition ranks:

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2
O must now challenge the implication if she accepts to enter into the discussion. The rule for the synthesis of a local reason for implication (provided above) stipulates that in order to challenge the thesis, O must state the antecedent and provide a local reason for it:

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 1 𝑚 ≔ 1 𝑛 ≔ 2
Synthesis of a local reason for conjunction

3

𝑝 ∶ 𝐴 ∧ 𝐵 0

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

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 3 𝑝 ∶ 𝐴 ∧ 𝐵 0 𝑞 ∶ 𝐵 ∧ 𝐴 4
The Opponent launches her challenge asking for the left component of the local reason 𝑞 provided by P, an application of the rule for the analysis of a local reason for a conjunction described above.

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 1 𝑚 ≔ 1 𝑛 ≔ 2 3 𝑝 ∶ 𝐴 ∧ 𝐵 0 𝑞 ∶ 𝐵 ∧ 𝐴

Analysis of a local reason for conjunction

5

? 𝐿 ∧ 4

Assume that P responds immediately to this challenge:

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 3 𝑝 ∶ 𝐴 ∧ 𝐵 0 𝑞 ∶ 𝐵 ∧ 𝐴 4 5 ? 𝐿 ∧ 4 𝐿 ∧ (𝑞): 𝐵 6
O will now ask for the resolution of the instruction:

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 3 𝑝 ∶ 𝐴 ∧ 𝐵 0 𝑞 ∶ 𝐵 ∧ 𝐴 4 5 ? 𝐿 ∧ 4 𝐿 ∧ (𝑞): 𝐵 6
Resolution of an instruction 7 ? …/𝐿 ∧ (𝑞) 6

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

In this case, resolving the instruction will lead P to bring forward an elementary statement-that is, a statement in which both the local reason and the proposition are elementary, which falls under the restriction of the Socratic rule. The idea for P then is to postpone his answer to the challenge launched with move 7 and to force O to choose a local reason first so as to copy it in his answer to the challenge. This yields a further application of the analysis rule for the conjunction: Move 11 thus provides P with the information he needed: he can then copy O's choice to answer the challenge she launched at move 7.

O P ! (𝐴 ∧ 𝐵) ⊃ (𝐵 ∧ 𝐴) 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 3 𝑝 ∶ 𝐴 ∧ 𝐵 0 𝑞 ∶ 𝐵 ∧ 𝐴 4 5 ? 𝐿 ∧ 4 𝐿 ∧ (
Note: It should be clear that a similar end will come about if O starts by challenging the right component of the conjunction statement, instead of challenging the left component.

Analysis of the example

Let us now go deeper in the analysis of the example and make explicit what happened during the play:

When O resolves R  (p) with the local reason b (for instance) and P resolves the instruction L  (q) with the same local reason, then P is not only stating b : In other words, the definitional equality 𝑅 ∧ (𝑝) 𝑂 = 𝑏: 𝐵 that provides content to B makes it explicit at the object-language level that an application of the Socratic rule has been initiated and achieved by means of dialogical interaction.

B
The development of a dialogue determined by immanent reasoning thus includes four distinct stages:

1. applying the rules of synthesis to the thesis; 2. applying the rules of analysis; 3. launching the Resolution and Substitution of instructions; 4. applying the Socratic rule. 5. We can then add a fifth stage: Producing the strategic reason.

While the first two steps involve local meaning, step 3 concerns global meaning and step 4 requires describing how to produce a winning strategy. Now that the general idea of local reasons has been provided, we will present in the next chapter all the rules together, according to their level of meaning.

The dialogical roots of equality: dialogues for immanent reasoning

In this section we will spell out a simplified version of the dialogues for immanent reasoning, that is, the dialogical framework incorporating features of Constructive Type Theory-a dialogical framework making the players' reasons for asserting a proposition explicit. The rules can be divided, just as in the standard framework, into rules determining local meaning and rules determining global meaning. These include: We will be presenting these rules in this order in the next two sections, along with the adaptation of the other structural rules to dialogues for immanent reasoning in the second section.

Local meaning in dialogues for immanent reasoning

The formation rules

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

Formation rules

Move

Challenge Defence In the formulation of this rule, "𝜋" is a statement and "𝜏 𝑖 " is a local reason of the form either 𝑎 𝑖 : 𝐴 𝑖 or 𝑥 𝑖 ∶ 𝐴 𝑖 .

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

The rules for local reasons: synthesis and analysis

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

Synthesis rules for local reasons

Move

Challenge Defence

Analysis rules for local reasons

Move

Anaphoric instructions: dealing with cases of anaphora

One of the most salient features of the CTT framework is that it contains the means to deal with cases of anaphora. For example anaphoric expressions are required for formalizing Barbara in CTT. In the following CTT-formalization of Barbara the projection fst(z) can be seen as the tail of the anaphora whose head is 𝑧:

(z : (x : D)A)B[fst(z)] true premise 1 (z : (x : D)B)C[fst(z)] true premise 2 -------------- (z : (x : D)A)C[fst(z)] true conclusion
In dialogues for immanent reasoning, when a local reason has been made explicit, this kind of anaphoric expression is formalized through instructions, which provides a further reason for introducing them. For example if a is the local reason for the first premise we have

P p : (z : (x : D)A(x))B(L  (L  (p) O ))
However, since the thesis of a play does not bear an explicit local reason (we use the exclamation mark to indicate there is an implicit one), it is possible for a statement to be bereft of an explicit local reason. When there is no explicit local reason for a statement using anaphora, we cannot bind the instruction L  (p) O to a local reason 𝑝. We thus have something like this, with a blank space instead of the anaphoric local reason:

P ! (z : (x : D)A(x))B(L  ( L  ( ) O ))
But this blank stage can be circumvented: the challenge on the universal quantifier will yield the required local reason: O will provide 𝑎: (∃𝑥: 𝐷)𝐴(𝑥), which is the local reason for 𝑧. We can therefore bind the instruction on the missing local reason with the corresponding variable-𝑧 in this case-and write

P ! (z : (x : D)A(x))B(L  (L  (z) O ))
We call this kind of instruction, Anaphoric instructions. For the substitution of Anaphoric instructions the following two cases are to be distinguished:

Substitution of Anaphoric Instructions 1

Given some Anaphoric instruction such as L  (z) Y , once the quantifier (∀𝑧: 𝐴)𝐵(… ) has been challenged by the statement a : A the occurrence of L  (z) Y can be substituted by a. The same applies to other instructions.

In our example we obtain: P ! (z : (x :

D)A(x))B(L  ( L  (z) O )) O a : (x : D)A(x) P b : B(L  (L  (z) O )) O ? a / L  (z) O P b : B(L  (a)) …

Substitution of Anaphoric Instructions 2

Given some Anaphoric instruction such as L  (z) Y , once the instruction L  (c)-resulting from an attack on the universal z : has been resolved with a : then any occurrence of L  (z) Y can be substituted by a. The same applies to other instructions.

Global Meaning in dialogues for immanent reasoning

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

Structural Rules SR0: Starting rule

The start of a formal dialogue of immanent reasoning is a move where P states the thesis. The thesis can be stated under the condition that O commits herself to certain other statements called initial concessions; in this case the thesis has the form ! [  , …,  n ], where 𝐴 is a statement with implicit local reason and 𝐵 1 , … , 𝐵 𝑛 are statements with or without implicit local reasons.

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

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

SR1: Development rule

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

SR1i: Intuitionistic Development rule, or Last Duty First

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

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

Note: This structural rule is known as the Last Duty First condition, and makes dialogical games suitable for intuitionistic logic, hence the name of this rule.

SR1c: Classical Development rule

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

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

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

SR2: Formation rules for formal dialogues

SR2i: Starting a formation dialogue

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

SR2ii: Developing a formation dialogue

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

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

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

SR3: Resolution of instructions

SR4: Substitution of instructions

Once the local reason b has been used to resolve the instruction I K (p) X , and if the same instruction occurs again, players have the right to require that the instruction be resolved with 𝑏.

The substitution request has the form ?𝑏/I k (p) X . Players cannot choose a different substitution term (in our example, not even X, once the instruction has been resolved).

This rule also applies to functions.

SR5: Socratic rule and definitional equality

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

SR5.1: Restriction of P statements P cannot make an elementary statement if O has not stated it before, except in the thesis. An elementary statement is either an elementary proposition with implicit local reason, or an elementary proposition and its local reason (not an instruction).

SR5.2: Challenging elementary statements in formal dialogues

Challenges of elementary statements with implicit local reasons take the form: 𝑿 ! 𝐴 𝒀 ? 𝑟𝑒𝑎𝑠𝑜𝑛 𝑿 𝑎 ∶ 𝐴 Where 𝐴 is an elementary proposition and 𝑎 is a local reason.13 P cannot challenge O's elementary statements, except if O provides an elementary initial concession with implicit local reason, in which case P can ask for a local reason, or in the context of transmission of equality.

SR5.3: Definitional equality

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

1. non-reflexive cases; 2. reflexive cases.

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

SR5.3.1: Non-reflexive cases of the Socratic rule

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

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

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

SR5.3.2: Reflexive cases of the Socratic rule

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

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

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

Definitional Equality transmits by reflexivity, transitivity and symmetry

Content and Material Dialogues

As pointed out by Krabbe (1985, p. 297), material dialoguesthat 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,14 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 objectlanguage 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 preceding sections of our study entirely leaves the introduction of local reasons to the Opponent (the Proponent only being allowed to endorse 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 reasoningto 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 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 both Socratic rules that are player dependent rules for elementary statements specific to that very statement, but also global rules, that is player independent rules for elementary statements, specific to those statements (thus providing the material level).

In fact, in principle; 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 prescibed 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.

We cannot in this paper develop these kind of dialogues, however we invite the reader to visit the chapter on material dialogues in Rahman/McConaughey/ [START_REF] Rahman | Immanent Reasoning. A plaidoyer for the Play-Level[END_REF], where the main we sketch the main features of material dialogues that include sets of natural numbers and the set 𝐁𝐨𝐨𝐥. 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. 15 . The final section of the chapter on Marial dialogues in Rahman/McConaughey/Klev/Clerbout (2018), discusses the epistemological notion of internalization of contes. 16 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 provides 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 [START_REF] Brandom | A Study Guide[END_REF] 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 sujective 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

Strategic reasons in dialogues for immanent reasoning

The conceptual backbone on which rests the metalogical properties of the dialogical framework is the notion of strategic reason which allows to adopt a global view on all the possible plays that constitute a strategy. However, this global view should not be identified with the perspective common in proof theory: strategic reasons are a kind of recapitulation of what can happen for a given thesis and show the entire history of the play by means of the instructions. Strategic reasons thus yield an overview of the possibilities enclosed in a thesis-what plays can be carried out from it-, but without ever being carried out in an actual play: they are only a perspective on all the possible variants of plays for a thesis and not an actual play. In this way the rules of synthesis and analysis of strategic reasons provided below are not of the same nature as the analysis and synthesis of local reasons, they are not produced through challenges and their defence, but are a recapitulation of the plays that can actually be carried out.

The notion of strategic reasons enables us to link dialogical strategies with CTTdemonstrations, since strategic reasons (and not local reasons) are the dialogical counterpart of CTT proof-objects; but it also shows clearly that the strategy level by itself-the only level that proof theory considers-is not enough: a deeper insight is gained when considering, together with the strategy level, the fundamental level of plays; strategic reasons thus bridge these two perspectives, the global view of strategies and the more in-depth and down-to-earth view of actual plays with all the possible variations in logic they allow,17 without sacrificing the one for the other. This vindication of the play level is a key aspect of the dialogical framework and one of the purposes of the present study: other logical frameworks lack this dimension, which besides is not an extra dimension appended to the concern for demonstrations, but actually constitutes it, the heuristical procedure for building strategies out of plays showing the gapless link there is between the play level and the strategy level: strategies (and so demonstrations) stem from plays. Thus the dialogical framework can say at least as much as other logical frameworks, and, additionally, reveals limitations of other frameworks through this level of plays.

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 Pstrategy, 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 P 𝑤 ∶ 𝐴 ∧ 𝐵.

In providing a strategic reason 𝑤 for the conjunction 𝐴 ∧ 𝐵, 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 𝐴 and 𝐵 prior to move 𝑖, two different plays can be carried out from this point, which we provide without the strategic reason:

Introducing strategic reasons: stating a conjunction

O P Concessions Thesis 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 … … … … … … ! 𝐴 ∧ 𝐵 𝑖
Introducing strategic reasons: left decision option on conjunction

O P Concessions Thesis 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 … … … … … … ! 𝐴 ∧ 𝐵 𝑖 𝑖 + 1 ? ∧ 1 𝑖 ! 𝐴 𝑖 + 2
Introducing strategic reasons: right decision option on conjunction

O P Concessions Thesis 0 1 𝑚 ≔ 1 𝑛 ≔ 2 2 … … … … … … ! 𝐴 ∧ 𝐵 𝑖 𝑖 + 1 ? ∧ 2 𝑖 ! 𝐵 𝑖 + 2
So if P brings forward the strategic reason 𝑤 to support his conjunction at move 𝑖, he is claiming to be able to win both Erreur ! Source du renvoi introuvable. and Erreur ! Source du renvoi introuvable., 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 strategy as recapitulation

Since a strategic reason (𝑤 for instance) is brought forward during a play (say at move 𝑖), 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 𝑖 + 2 depending on the Opponent's decision at move 𝑖 + 1, so the strategic object 𝑤 played at move 𝑖 will contain these two possible scenarios with the 𝑖 + 2 P-move depending of the 𝑖 + 1 Odecision. The strategic reason 𝑤 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, 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 developed, 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.

3.2

Rules for the synthesis of P-strategic reasons: 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 𝑝 2 is dependent upon O's choice of 𝑝 1 .

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 section we are seeking a notion of winning strategy that corresponds to that of a CTTdemonstration, and since these strategies have being identified to be those where P wins, we will only provide the synthesis of strategic reasons for P. 18Synthesis of strategic reasons for P: 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 𝐏 ! ⊥, which would amount to P losing; this statement "P n O

Move

Correspondence between the synthesis of strategic reasons and CTT introduction rules and elimination rules

Since we are considering a P-winning strategy, we are searching what P needs to justify in order to justify his thesis, which is the point of the synthesis rules for strategic reasons. This search corresponds to the CTT introduction rules, since these determine what one needs in order to carry out an inference. The following table displays the correspondence between the procedures of synthesis of a strategic reason and an introduction rule.

Correspondence between synthesis of strategic reasons and introduction rules

Synthesis of P-strategic reasons: CTT-introduction rule:

Existential quantification

𝐏 ! (∃𝑥 ∶ 𝐴)𝐵(𝑥) (∃𝑥 ∶ 𝐴)𝐵(𝑥) 𝒕𝒓𝒖𝒆 𝑝 1 ∶ 𝐴 𝑝 2 ∶ 𝐵(𝑝 1 ) 〈𝑝 1 , 𝑝 2 〉 ∶ (∃𝑥 ∶ 𝐴)𝐵(𝑥) 𝐎 ? 𝐿 ∃ 𝐏 𝑝 1 ∶ 𝐴 𝐎 ? 𝑅 ∃ 𝐏 𝑝 2 ∶ 𝐵(𝑝 1 ) 𝐏 〈𝑝 1 , 𝑝 2 〉 ∶ (∃𝑥 ∶ 𝐴)𝐵(𝑥) Conjunction 𝑷 ! 𝐴 ∧ 𝐵 𝐴 ∧ 𝐵

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 choicedependence 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.

P-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 Pstrategic 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. The second presentation on the other hand, allows P to back any proposition 𝐶 with the local reason '𝑦𝑜𝑢 𝑔𝑎𝑣𝑒 𝑢𝑝 (𝑛)' once O has stated ⊥ at move 𝑛. Thus the strategic reason for any proposition 𝐶 is constituted by '𝑦𝑜𝑢 𝑔𝑎𝑣𝑒 𝑢𝑝 (𝑛)', provided that O has provided P with the means for resolving the instruction 𝐿 ⊃ (𝑝).

Analysis rules for P-strategic reasons

Move

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: P 𝑦𝑜𝑢 𝑔𝑎𝑣𝑒 𝑢𝑝 (𝑛) ⟦𝐿 ⊃ (𝑝) 𝑃 = 𝑝 1 𝑷,𝑶 ⟧ : C corresponds to the CTT-elimination-rule for absurdity, that is: ⊥true 𝐶 true interpreted as the fact that we shall never get an element of ⊥ defined as the empty ℕ 0  More precisely, if 𝑐 ∶ ℕ 0 , then the proof-object of 𝐶 is "𝑅 0 " understood as an "aborted programme" 𝑐 ∶ ℕ 0 𝑅 0 (𝑐) ∶ 𝐶(𝑐).

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.

A Plaidoyer for the play-level

To some extent, the criticisms the dialogical approach to logic has been subject to provides an opportunity for clarifying its basic tenets. We will therefore herewith consider some recent objections raised against the dialogical framework in order to pinpoint some of its fundamental features, whose importance may not have appeared clearly enough through the main body of the paper; namely, dialogue-definiteness, player-independence, and the dialogical conception of proposition.

Showing how and why these features have been developed, and specifying their point and the level they operate on, will enable us to vindicate the play level and thus disarm the objections that have been raised against the dialogical framework for having neglected this crucial level.

We shall first come back on the central notion of dialogue-definiteness and on the dialogical conception of propositions, which are essential for properly understanding the specific role and importance of the play level. We shall then be able to address three objections to the dialogical framework, due to a misunderstanding of the notion of Built-in Opponent, of the principles of dialogue-definiteness and of player-independence, and of the reflection on normativity that constitutes the philosophical foundation of the framework; all of these misunderstandings can be reduced to a misappraisal of the play level. We shall then go somewhat deeper in the normative aspects of the dialogical framework, according to the principle that logic has its roots in ethics.

Dialogue-Definiteness and Propositions

The dialogical theory of meaning is structured in three levels, that of the local meaning (determined by the particle rules for the logical constants), of the global meaning (determined by the structural rules), and the strategic level of meaning (determined by what is required for having a winning strategy). The material level of consideration is part of the global meaning, but with particular rules so precise that they determine only one specific expression (through a modified Socratic rule). A characteristic of the local meaning is that the rules are player independent: the meaning is thus defined in the same fashion for each player; they are bound by the same sets of duties and rights when they start a dialogue. This normative aspect is thus constitutive of the play level (which encompasses both the local meaning and the global meaning): it is even what allows one to judge that a dialogue is taking place. In this regard, meaning is immanent to the dialogue: what constitutes the meaning of the statements in a particular dialogue solely rests on rules determining interaction (the local and the global levels of meaning). The strategy level on the other hand is built on the play level, and the notion of demonstration operates on the strategy level (it amounts to having a winning strategy).

Two main tenets of the dialogical theory of meaning can be traced back to Wittgenstein, and ground in particular the pivotal notion of dialogue-definiteness:

1. the internal feature of meaning (the Unhintergehbarkeit der Sprache 19 ), and 2. the meaning as mediated by language-games.

As for the first Wittgensteinian tenet, the internal feature of meaning, we already mentioned in the introduction that if we relate the notion of internalization of meaning with both languagegames and fully-interpreted languages of CTT, then a salient feature of the dialogical approach to meaning can come to fore: the expressive power of CTT allows all these actions involved in the dialogical constitution of meaning to be incorporated as an explicit part of the object-language of the dialogical framework.

In relation to the second tenet, the inceptors of the dialogical framework observed that if language-games are to be conceived as mediators of meaning carried out by social interaction, these language-games must be games actually playable by human beings: it must be the case that we can actually perform them, 20 which is captured in the notion of dialogue-definiteness. 21Dialogue-definiteness is essential for dialogues to be mediators of meaning, but it is also constitutive of what propositions are, as Lorenz clearly puts it:

[…] for an entity to be a proposition there must exist an individual play, such that this entity occupies the initial position, and the play reaches a final position with either win or loss after a finite number of moves according to definite rules. (Lorenz, 2001, p. 258) A proposition is thus defined in the standard presentation of dialogical logic as a dialoguedefinite expression, that is, an expression 𝐴 such that there is an individual play about 𝐴, that can be said to be lost or won after a finite number of steps, following given rules of dialogical interaction. 22The notion of dialogue-definiteness is in this sense the backbone of the dialogical theory of meaning: it provides the basis for implementing the human-playability requirement and the notion of proposition. 19 See Tractatus Logico-Philosophicus, 5.6. 20 As observed by Marion (2006, p. 245), a lucid formulation of this point is the following remark of Hintikka (1996, p. 158) who shared this tenet (among others) with the dialogical framework:

[Finitism] was for Wittgenstein merely one way of defending the need of language-games as the sense that [sic] they had to be actually playable by human beings. […] Wittgenstein shunned infinity because it presupposed constructions that we human beings cannot actually carry out and which therefore cannot be incorporated in any realistic language-game. […]

What was important for Wittgenstein was not just the finitude of the operations we perform in our calculi and other language-games, but the fact that we can actually perform them. Otherwise the entire idea of language-games as meaning mediators will lose its meaning. The language-games have to be humanly playable. And that is not possible if they involve infinitary elements. Thus it is the possibility of actually playing the meaning-conferring language-games that is the crucial issue for Wittgenstein, not finitism as such.

Dialogue-definiteness sets apart rather decisively the level of strategies from the level of plays, as Lorenz's notion of dialogue-definite proposition does not amount to a set of winning strategies, but rather to an individual play. Indeed, a winning strategy for a player X is a sequences of moves such that X wins independently of the moves of the antagonist. It is crucial to understand that the qualification independently of the moves of the antagonist amounts to the fact that the one claiming 𝐴 has to play under the restriction of the Copy-cat rule: if possessing a winning strategy for player X involves being in possession of a method (leading to the win of X) allowing to choose a move for any move the antagonist might play, then we must assume that the propositions brought forward by the antagonist are justified. There is a winning strategy if X can base his moves leading to a win by endorsing himself those propositions whose justification is rooted on Y's authority. For short, the act of endorsing is what lies behind the so-called Copy-cat rule and structures dialogues for immanent reasoning: it ensures that X can win whatever the contender might bring forward in order to contest 𝐴 (within the limits set by the game).

Furthermore, refuting, that is bringing up a strategy against 𝐴, amounts to the dual requirement: that the antagonist Y possess a method that leads to the loss of X ! 𝐴, whatever X is can bring forward, and that she can do it under the Copy-cat restriction:

X ! 𝐴 is refuted, if the antagonist Y can bring up a sequence of moves such that she (Y) can win playing under the Copy-cat restriction.

Refuting is thus different and stronger than contesting: while contesting only requires that the antagonist Y brings forward at least one counterexample in a kind of play where Y does not need to justify her own propositions, refuting means that Y must be able to lead to the loss of X ! A, whatever X's justification of his propositions might be.

In this sense, the assumption that every play is a finitary open two-person zero-sum game does not mean that either there is a winning strategy for 𝐴 or a winning strategy against 𝐴: the play level cannot be reduced to the strategy level.

For instance, if we play with the Last-duty first development rule P will lose the individual plays relevant for the constitution of a strategy for ∨ ¬𝐴 . So 𝐴 ∨ ¬𝐴 is dialogue-definite, though there is no winning strategy against 𝐴 ∨ ¬𝐴.

The distinction between the play level and the strategy level thus emerges from the combination of dialogue-definiteness and the Copy-cat rule.

The classical reduction of strategies against 𝐴 to the falsity of 𝐴 (by means of the saddlepoint theorem) assumes that the win and the loss of a play reduce to the truth or the falsity of the thesis. But we claim that the existence of the play level and a loss in one of the plays introduces a qualification that is not usually present in the purely proof-theoretic approach; to use the previous example, we know that P does not have a winning strategy for ! 𝐴 ∨ ¬𝐴 (playing under the intuitionisitic development rule), but neither will O have one against it if she has to play under the Copy-cat rule herself (notice the switch in the burden of the restriction of the Copy-cat rule when refuting a thesis). Let us identify the player who has to play under the Copy-cat restriction by highlighting her moves:

Play against P ! 𝐴 ∨ ¬𝐴 O P ! 𝐴 ∨ ¬𝐴 0 1 𝑛 ≔ 1 𝑚 ≔ 2 2 3 ? ∨ 0 ! 𝐴 4 P wins
The distinction between the play and the strategy level can be understood as a consequence of introducing the notion of dialogue-definiteness which amounts to a win or a loss at the play level, though strategically seen, the proposition at stake may be (proof-theoretically) undecidable. Hence, some criticisms to the purported lack of dynamics to dialogical logic are off the mark if they are based on the point that "games" of dialogical logic are deterministic: 23 plays are deterministic in the sense that they are dialogue-definite, but strategies are not deterministic in the sense that for every proposition there would either be a winning strategy for it or a winning strategy against it.

Before ending this section let us quote quite extensively [START_REF] Lorenz | Basic Objectives of Dialogue Logic in Historical Perspective[END_REF], who provides a synopsis of the historical background that lead to the introduction of the notion of dialoguedefiniteness and the distinction of the deterministic conception of plays-which obviously operates at the level of plays-from the proof-theoretical undecidable propositions-which operate at the level of strategies:

[…] It was Alfred Tarski who, in discussions with Lorenzen in 1957/58, when Lorenzen had been invited to the Institute for Advanced Study at Princeton, convinced him of the impossibility to characterize arbitrary (logically compound) propositions by some decidable generalization of having a decidable proof-predicate or a decidable refutation-predicate.

[…] It became necessary to search for some decidable predicate which may be used to qualify a linguistic entity as a proposition about any domain of objects, be it elementary or logically compound. Decidability is essential here, because the classical characterization of a proposition as an entity which may be true or false, has the awkward consequence that of an undecided proposition it is impossible to know that it is in fact a proposition. This observation gains further weight by L. E. J. Brouwer's discovery that even on the basis of a set of "value-definite", i.e., decidably true or false, elementary propositions, logical composition does not in general preserve value-definiteness. And since neither the property of being proof-definite nor the one of being refutation-definite nor properties which may be defined using these two, are general enough to cover the case of an arbitrary proposition, some other procedure had to be invented which is both characteristic of a proposition and satisfies a decidable concept. The concept looked for and at first erroneously held to be synonymous with argumentation[ 24 ] turned out to be the concept of dialogue about a proposition 23 For such criticismssee Trafford (2017, pp. 86-88). 24 Lorenz identifies argumentation rules with rules at the strategy level and he would like to isolate the interaction displayed by the moves constituting the play levelsee Lorenz (2010a, p.79). We deploy the term argumentationrule for request-answer interaction as defined by the local and structural rules. It is true that nowadays argumentation-rules has even a broader scope including several kinds of communicative interaction and this might produce some confusion on the main goal of the dialogical framework which is in principle, to provide an argumentative understanding of logic rather than the logic of argumentation. However, once this distinction has been drawn nothing prevents to develop the interface dialogical-understanding of logic/logical structure of a dialogue. In fact, it is our claim that in order to study the logical structure of a dialogue, the dialogical conception of logic provides the right venue.

A (which had to replace the concept of truth of a proposition A as well as the concepts of proof or of refutation of a proposition A, because neither of them can be made decidable). Fully spelled out it

means that for an entity to be a proposition there must exist a dialogue game associated with this entity, i.e., the proposition A, such that an individual play of the game where A occupies the initial position, i.e., a dialogue D(A) about A, reaches a final position with either win or loss after a finite number of moves according to definite rules: the dialogue game is defined as a finitary open twoperson zero-sum game. Thus, propositions will in general be dialogue-definite, and only in special cases be either proof-definite or refutation-definite or even both which implies their being valuedefinite. Within this game-theoretic framework where win or loss of a dialogue D(A) about A is in general not a function of A alone, but is dependent on the moves of the particular play D(A), truth of A is defined as existence of a winning strategy for A in a dialogue game about A; falsehood of A respectively as existence of a winning strategy against A. Winning strategies for A count as proofs of A, and winning strategies against A as refutations of A. The meta-truth of "either 'A is true' or 'A is false' " which is provable only classically by means of the saddlepoint theorem for games of this kind may constructively be reduced to the decidability of win or loss for individual plays about A. The concept of truth of dialogue-definite propositions remains finitary, and it will, as it is to be expected of any adequate definition of truth, in general not be recursively enumerable. The same holds for the concept of falsehood which is conspicuously defined independently of negation. (Lorenz, 2001, pp. 257-258).

4.2

The Built-in Opponent and the Neglect of the Play Level

In recent literature Catarina Duthil Novaes (2015) and James Trafford (2017, pp. 102-105) deploy the term internalization for the proposal that natural deduction can be seen as having an internalized Opponent, thereby motivating the inferential steps. This form of internalization is called the built-in Opponent. The origin of this concept is linked to Göran Sundholm who, by 2000, in order to characterize the fundamental links between natural deduction and dialogical logic, introduced in his lectures and talks the term implicit interlocutor. Yet, since the notion of implicit interlocutor was meant to link the strategy level with natural deduction, the concept of built-in Opponent-being the implicit interlocutor's offspring-inherited the same strategic perspective on logical truth. Thus, logical truth can be seen as the encoding of a process through which the Proponent succeeds in defending his assertion against a stubborn ideal interlocutor. 25From the dialogical point of view however, the ideal interlocutor of the strategy level is the result of a process of selecting the relevant moves from the play level. Rahman/Clerbout/ [START_REF] Keiff | Dialogical Logic[END_REF], in a paper dedicated to the Festschrift for Sundholm, designate the process as incarnation, using Jean-Yves Girard's term. Their thorough description of the incarnation process already displays those aspects of the cooperative endeavour, which was formulated by Duthil Novaes (2015) and quoted by Trafford (2017, p. 102) as a criticism of the dialogical framework. Their criticism seems to rest on the idea that the dialogues of the dialogical framework are not truly cooperative, since they are reduced to constituting logical truth. If this is really the point of their criticism, it is simply wrong, for the play level would then be completely neglected: the intersubjective in-built and implicit cooperation of the strategy level (which takes care of inferences) grows out of the explicit interaction of players at the play level in relation to the formation-rules; accepting or contesting a local reason is a process by the means of which players cooperate in order to determine the meaning associated to the action-schema at stake. 26 It is fair to say that the standard dialogical framework, not enriched with the language of CTT, did not have the means to fully develop the so-called material dialogues, that is dialogues that deal with content. Duthil Novaes (2015, p. 602)-but not Trafford (2017, p. 102)-seems to be aware that dialogues are a complex interplay of adversarial and cooperative moves, 27 even in Lorenzen and Lorenz' standard formulation. However, since she understands this interplay as triggered by the built-in implicit Opponent at the strategy level, Duthil Novaes suggestions or corrections motivated by reflections on the Opponent's role cannot be made explicit in the framework, and the way this role contributes in finally constituting a winning strategy cannot be traced back. 28 Duthil Novaes ' (2015, pp. 602-604) approach leads her to suggest that monotonicity is a consequence of the role of the Opponent as a stubborn adversary, which takes care of the nondefeasibility of the demonstration at stake; from this perspective, she contends that the standard presentations of dialogical logic, being mostly adversarial or competitive, are blind to defeasible forms of reasons and are thus […] rather contrived forms of dialogical interaction, and essentially restricted to specific circles of specialists (Duthil Novaes, 2015, p. 602). But this argument is not compelling when considering the strategy level as being built from the play level: setting aside the point on content mentioned above, if we conceive the constitution of a strategy as the end-result of the complementary role of competition and cooperation taking place at the play level, we do not seem to need-at least in many cases-to endow the notion of 26 In fact, when [START_REF] Trafford | Meaning in Dialogue. An Interactive Approach to Logic and Reasoning[END_REF] criticizes dialogical logic in his chapter 4, he surprisingly claims that this form of dialogical interaction does not include the case in which the plays would be open-ended in relation to the logical rules at stake, though it has already been suggested-see for instance in (Rahman & Keiff, 2005, pp. 394-403)-how to develop what we called Structure Seeking Dialogues (SSD). Moreover, [START_REF] Keiff | Le Pluralisme dialogique : Approches dynamiques de l'argumentation formelle[END_REF] PhD-dissertation is mainly about SSD. The idea behind SSD is roughly the following; let us take some inferential practice we would like to formulate as an action-schema, mainly in a teaching-learning situation; we then search for the rules allowing us to make these inferential practices to be put into a schema. For example: we take the third excluded to be in a given context a sound inferential practice; we then might ask what kind of moves P should be allowed to make if he states the third excluded as thesis. It is nonetheless true to say that SSD were studied only in the case of modal logic. 27 To put it in her own words: "the majority of dialogical interactions involving humans appear to be essentially cooperative, i.e., the different speakers share common goals, including mutual understanding and possibly a given practical outcome to be achieved." Duthil Novaes (2015, p. 602). 28 See for instance her discussion of countermoves Duthil Novaes (2015, p. 602) : indefeasibility means that the Opponent has no available countermove: "A countermove in this case is the presentation of one single situation, no matter how far-fetched it is, where the premises are the case and the conclusion is not-a counterexample." The question then would be to know how to show that the Opponent has no countermove available. The whole point of building winning strategies from plays is to actually construct the evidence that there is no possible move for the Opponent that will lead her to win: that is a winning strategy. But when the play level is neglected, the question remains: how does one know the Opponent has no countermove available? It can actually be argued that the mere notion of countermove tends to blurr the distinction between the level of plays and of strategies: a countermove makes sense if it is 'counter' to a winning strategy, as if the players were playing at the strategy level, but that is something we explicitly reject. At the play level, there are only simple moves: these can be challenges, defences, counterattacks, but countermoves do not make any sense.

inference with non-monotonic features. The play level is the level were cooperative interaction, either constructive or destructive, can take place until the definitive answer-given the structural and material conditions of the rules of the game-has been reached. 29 The strategy level is a recapitulation that retains the end result. These considerations should also provide an end to Trafford's (2017, pp. 86-88) search for open-ended dialogical settings: open-ended dialogical interaction, to put it bluntly, is a property of the play level. Certainly the point of the objection may be to point out either that this level is underdeveloped in the literature-a fact that we acknowledge with the provisos formulated above-, or that the dialogical approach to meaning does not manage to draw a clean distinction between local and strategic meaning-the section on tonk below intends to make this distinction as clear as possible.

At this point of the discussion we can say that the role of the (built-in) Opponent in Lorenzen and Lorenz' dialogical logic has been fully misunderstood. Indeed, the role of both interlocutors (implicit or not) is not about assuring logical truth by checking the non-defeasibility of the demonstration at stake, but their role is about implementing both the dialogical definiteness of the expressions involved and the internalization of meaning.30

Pathological cases and the Neglect of the Play Level

The notorious case of [START_REF] Prior | The Runabout Inference-ticket[END_REF] tonk has been several times addressed as a counterargument to inferentialism and also to the "indoor-perspective" of the dialogical framework. This also seems to constitute the background of how Trafford (2017, p. 86) for instance reproduces the circularity objection against the dialogical approach to logical constants. At this point of the discussion, Trafford (2017, pp. 86-88) is clearly aware of the distinction between the rules for local meaning and the rules of the strategy level, though he points out that the local meaning is vitiated by the strategic notion of justification. This is rather surprising as [START_REF] Rahman | On How to be a Dialogician[END_REF], Rahman/Clerbout/ [START_REF] Keiff | Dialogical Logic[END_REF], [START_REF] Rahman | Negation in the Logic of First Degree Entailment and Tonk. A Dialogical Study[END_REF] and [START_REF] Redmond | Armonía Dialógica: tonk Teoría Constructiva de Tipos y Reglas para Jugadores Anónimos[END_REF] have shown it is precisely the case of tonk that provides a definitive answer to the issue.

In this respect, three well distinguished levels of meaning are respectively determined by specific rules:

 the local meaning of an expression establishes how a statement involving such an expression is to be attacked and defended (through the particle rules);  the global meaning of an expression results from structural rules prescribing how to develop a play having this expression for thesis;  the strategy rules (for P) determine what options P must consider in order to show that he does have a method for winning whatever O may do-in accordance with the local and structural rules.

It can in a quite straightforward fashion be shown (see below) that an inferential formulation of rules for tonk correspond to strategic rules that cannot be constituted by the formulation of particle rules. The player-independence of the particle rules-responsible for the branches at the strategy level-do not yield the strategic rules that the inferential rules for tonk are purported to prescribe.

For short, the dialogical take on tonk shows precisely how distinguishing rules of local meaning from strategic rules makes the dialogical framework immune to tonk. As this distinction is central to the dialogical framework and illustrates the key feature of player-independence of particle rules, we will now develop the argument; we will then be able to contrast this pathological tonk case to another case, that of the black-bullet operator.

The tonk challenge and player-independence of local meaning

To show how the dialogical framework is immune to tonk through the importance and priority it gives to the play level, winning strategies are linked to semantic tableaux. According to the dialogical perspective, if tableaux rules (or any other inference system for that matter) are conceived as describing the core of strategic rules for P, then the tableaux rules should be justified by the play level, and not the other way round: the tonk case clearly shows that contravening this order yields pathological situations. We will here only need conjunction and disjunction for dealing with tonk. 31 A systematic description of the winning strategies available for P in the context of the possible choices of O can be obtained from the following considerations: if P is to win against any choice of O, we will have to consider two main different dialogical situations, namely those (a) in which O has uttered a complex formula, and those (b) in which P has uttered a complex formula. We call these main situations the O-cases and the P-cases, respectively. In both of these situations another distinction has to be examined:

(i) P wins by choosing i.1. between two possible challenges in the O-cases (a), or i.2. between two possible defences in the P-cases (b), iff he can win with at least one of his choices.

(ii) When O can choose ii.1. between two possible defences in the O-cases (a), or ii.2. between two possible challenges in the P-cases (b), P wins iff he can win irrespective of O's choices.

The description of the available strategies will yield a version of the semantic tableaux of Beth that became popular after the landmark work on semantic-trees by Raymond Smullyan (1968), where O stands for T (left-side) and P for F (right-side), and where situations of type ii (and not of type i) will lead to a branching-rule. (𝐎)𝐴 ∧ 𝐵 (𝐎)𝐴 ∨ 𝐵 〈𝐏 ?∧ 1 〉 (𝐎)𝐴 〈𝐏?∧ 2 〉 (𝐎)𝐵 〈𝐏? 〉 (𝐎)𝐴  (𝐎)𝐵 However, as mentioned above, semantic tableaux are not dialogues. The main point is that dialogues are built bottom up, from local to global meaning, and from global meaning to validity. This establishes the priority of the play level over the winning strategy level. From the dialogical point of view, Prior's original tonk contravenes this priority.

Let us indeed temporarily assume that we can start not by laying down the local meaning of tonk, but by specifying how a winning strategy for tonk would look like with the help of T(left)side and F(right)-side tableaux-rules (or sequent-calculus) for logical constants; in other words, let us assume that the tableaux-rules are necessary and sufficient to set the meaning of tonk.

Prior's tonk rules are built for half on the disjunction rules (taking up only its introduction rule), and for half on the conjunction rules (taking up only its elimination rule). This renders the following tableaux version for the undesirable tonk: 32 Tonk is certainly a nuisance: if we apply the cut-rule, it is possible to obtain a closed tableau for T𝐴, F𝐵, for any 𝐴 and 𝐵. Moreover, there are closed tableaux for both {𝐓𝐴, 𝐴𝑡𝑜𝑛𝑘¬𝐴} and {𝐓𝐴, ¬(𝐴𝑡𝑜𝑛𝑘¬𝐴)}.

From the dialogical point of view, the rejection of tonk is linked to the fact there is no way to formulate rules for its local meaning that meet the condition of being player-independent: if we try to formulate rules for local meaning matching the ones of the tableaux, the defence yields a different response, namely the tail of tonk if the defender is O, and the head of tonk if the defender is The fact that we need two sets of rules for the challenge and the defence of a tonk move means that the rule that should provide the local meaning of tonk is player-dependent, which should not be the case.

Summing up, within the dialogical framework tonk-like operators are rejected because there is no way to formulate player-independent rules for its local meaning that justify the tableaux rules designed for these operators. The mere possibility of writing tableaux rules that cannot be linked to the play level rules shows that the play level rules are not vitiated by strategic rules.

This brief reflection on tonk should state our case for both, the importance of distinguishing the rules of the play level from those of the strategy level, and the importance of including in the rules for the local meaning the feature of player-independence: it is the player-independence that provides the meaning explanation of the strategic rules, not the other way round.

The black-bullet challenge and dialogue-definiteness Trafford (2017, pp. 37-41) contests the standard inferentialist approach to the meaning of logical constants by recalling the counterexample of Stephen Read, the black-bullet operator. Indeed, [START_REF] Read | Harmony and Modality[END_REF][START_REF] Read | General Elimination Harmony and the Meaning of the Logical Constants[END_REF] introduces a different kind of pathological operator, the black-bullet •, a zero-adic operator that says of itself that it is false. Trafford (2017, p. 39 footnote 35) suggests that the objection also extends to CTT; this claim however is patently wrong, since those counterexamples would not meet the conditions for the constitution of a type. 33 Within the dialogical framework, though player-independent rules for black-bullet can be formulated (as opposed to tonk), they do not satisfy dialogue-definiteness.

Let us have the following tableaux rules for the black-bullet, showing that it certainly is pathological: they deliver closed tableaux for both • and ¬ •:

(P) • 〈𝐎? 〉 (P)•⊃⊥ (𝐎) • 〈𝐏? 〉 (𝐎) •⊃⊥
We can in this case formulate the following player-independent rules: 33 Klev (2017, p. 12 footnote 7) points out that the introduction rule of such kind of operator fails to be meaninggiving because the postulated canonical set Λ(𝐴) occurs negatively in its premiss, and that the restriction avoiding such kind of operators have been already formulated by Martin-Löf (1971, pp. 182-183), and by [START_REF] Dybjer | Inductive families[END_REF].

Black-bullet player-independent particle rules

Move

Challenge Defence 𝐗 ! • 𝐘 ? • 𝐗! •⊃⊥
The black-bullet operator seems therefore to meet the dialogical requirement of playerindependent rules, and would thus have local meaning. But if it does indeed have playerindependent rules, the further play on the defence (which is a negation) would require that the challenger concedes the antecedent, that is black-bullet itself:

Deploying the black-bullet challenges

Y X … … ! • 𝑖 𝑖 + 1 ? • 𝑖 ! •⊃⊥ 𝑖 + 2 𝑖 + 3 ! • 𝑖 + 2 𝑖 + 3 ? • 𝑖 + 4
Obviously, this play sequence can be carried out indefinitely, regardless of which player initially states black-bullet. So the apparently acceptable player-independent rules for playing black-bullet would contravene dialogue-definiteness; and the only way of keeping dialoguedefiniteness would be to give up player-independence!34

Conclusion: the meaning of expressions comes from the play level

The two pathological cases we have discussed, the tonk and the black-bullet operators, stress the difference between the play level and the strategy level and how the meaning provided by rules at the strategy level does not carry to the local meaning. Thus, from the dialogical point of view, the rules determining the meaning of any expression are to be rooted at the play level, and at this level what is to be admitted and rejected as a meaningful expression amounts to the formulation of a player-independent rule, that prescribe the constitution of a dialogue-definite proposition (where that expression occurs as a main operator).

Notice that if we include material dialogues the distinction between logical operators and non-logical operators is not important any more. If we enrich the dialogical framework with the CTT-language, this feature comes more prominently to the fore. What the dialogical framework adds to the CTT framework is, as pointed out by Martin-Löf (2017a;[START_REF] Martin-Löf | Assertion and Request[END_REF], to set a pragmatic layer where normativity finds its natural place. Let us now discuss the notion of normativity.

Normativity and the Dialogical Framework: A New Venue for the Interface Pragmatics-Semantics

In his recent book, Jaroslav [START_REF] Peregrin | Inferentialism. Why Rules Matter[END_REF] marshals the distinction between the play level and the strategy level (that he calls tactics) in order to offer another insight, more general, into the issue of normativity mentioned at that start of our volume (Indeed, Peregrin understands the normativity of logic not in the sense of a prescription on how to reason, but rather as providing the material by the means of which we reason.

It follows from the conclusion of the previous section that the rules of logic cannot be seen as tactical rules dictating feasible strategies of a game; they are the rules constitutive of the game as such. (MP does not tell us how to handle implication efficiently, but rather what implication is.) This is a crucial point, because it is often taken for granted that the rules of logic tell us how to reason precisely in the tactical sense of the word. But what I maintain is that this is wrong, the rules do not tell us how to reason, they provide us with things with which, or in terms of which, to reason. (Peregrin, 2014, pp. 228-229) Peregrin endorses at this point the dialogical distinction between rules for plays and rules for strategies. In this regard, the prescriptions for developping a play provide the material for reasoning, that is, the material allowing a play to be developped, and without which there would not even be a play; whereas the prescriptions of the tactical level (to use his terminology) prescribe how to win, or how to develop a winning-strategy:

This brings us back to our frequently invoked analogy between language and chess. There are two kinds of rules of chess: first, there are rules of the kind that a bishop can move only diagonally and that the king and a rook can castle only when neither of the pieces have previously been moved. These are the rules constitutive of chess; were we not to follow them, we have seen (Section 5.5) we would not be playing chess. In contrast to these, there are tactical rules telling us what to do to increase our chance of winning, rules advising us, e.g., not to exchange a rook for a bishop or to embattle the king by castling. Were we not to follow them, we would still be playing chess, but with little likelihood of winning. (Peregrin, 2014, pp. 228-229) This observation of Peregrin plus his criticism on the standard approach to the dialogical framework, according to which this framework would only focus on logical constants (Peregrin, 2014, pp. 100, 106)-a criticism shared by many others since (Hintikka, 1973, pp. 77-82)naturally leads to the main subject of our book, namely immanent reasoning, or linking CTT with the dialogical framework.

The criticism according to which the focus would be on logical constants and not on the meaning of other expressions does indeed fall to some extent on the standard dialogical framework, as little studies have been carried out on material dialogues in this basic framework;35 but the enriched CTT language in material dialogues deals with this shortcoming.

Yet this criticism seems to dovetail this other criticism, summoned by Martin-Löf as starting point in his Oslo lecture: I shall take up criticism of logic from another direction, namely the criticism that you may phrase by saying that traditional logic doesn't pay sufficient attention to the social character of language. (Martin-Löf, 2017a, p. 1) The focus on the social character of language not only takes logical constants into account, of course, but it also considers other expressions such as elementary propositions or questions, as well as the acts bringing these expressions forward in a dialogical interaction, like statements, requests, challenges, or defences-to take examples from the dialogical framework-and how these acts made by persons intertwine and call for-or put out of order-other specific responses by that person or by others. In this regard, the social character of language is put at the core of immanent reasoning through the normativity present in dialogues: normativity involves, within immanent reasoning, rules of interaction which allow us to consider assertions as the result of having intertwined rights and duties (or permissions and obligations). This central normative dimension of the dialogical framework at large, which stems from questionning what is actually being done when implementing the rules of this very framework, entails that objections according to which the focus would be only on logical constants will always be, from the dialogical perspective, slightly off the mark.

As mentioned in the introduction, in his Oslo and Stockholm lectures, Martin-Löf's (2017a;[START_REF] Martin-Löf | Assertion and Request[END_REF] delves in the structure of the deontic and epistemic layers of statements within his view on dialogical logic. In order to approach this normative aspect which pervades logic up to its technical parts, let us discuss more thoroughly the following extracts of "Assertion and Request": 36

[…] we have this distinction, which I just mentioned, between, on the one hand, the social character of language, and on the other side, the non-social […] view of language. But there is a pair of words that fits very well here, namely to speak of the monological conception of logic, or language in general, versus a dialogical one. And here I am showing some special respect for Lorenzen, who is the one who introduced the very term dialogical logic.

The first time I was confronted with something of this sort was when reading Aarne Ranta's book Type-Theoretical Grammar in (1994). Ranta there gave two examples, which I will show immediately. The first example is in propositional logic, and moreover, we take it to be constructive propositional logic, because that does matter here, since the rule that I am going to show is valid constructively, but not valid classically. Suppose that someone claims a disjunction to be true, asserts, or judges, a disjunction to be true. Then someone else has the right to come and ask him, Is it the left disjunct or is it the right disjunct that is true? There comes an opponent here, who questions the original assertion, and I could write that in this way:

? ⊢ 𝐴 ∨ 𝐵 𝑡𝑟𝑢𝑒

And by doing that, he obliges the original assertor to answer either that 𝐴 is true that is, to assert either that 𝐴 is true or that 𝐵 is true, so he has a choice, and we need to have some symbol for the choice here.

(Dis)

⊢ 𝐴 ∨ 𝐵 𝑡𝑟𝑢𝑒 ? ⊢ 𝐴 ∨ 𝐵 𝑡𝑟𝑢𝑒 ⊢ 𝐴 𝑡𝑟𝑢𝑒 | ⊢ 𝐵 𝑡𝑟𝑢𝑒 Ranta's second example is from predicate logic, but it is of the same kind. Someone asserts an existence statement, ⊢ (∃𝑥 ∶ 𝐴)𝐵(𝑥) 𝑡𝑟𝑢𝑒 and then someone else comes and questions that ? ⊢ (∃𝑥 ∶ 𝐴)𝐵(𝑥) 𝑡𝑟𝑢𝑒 And in that case the original assertor is forced, which is to say, he must come up with an individual from the individual domain and also assert that the predicate 𝐵 is true of that instance.

[…] So, what are the new things that we are faced with here? Well, first of all, we have a new kind of speech act, which is performed by the| oh, I haven't said that, of course I will use the standard terminology here, either speaker and hearer, or else respondent and opponent, or proponent and opponent, as Lorenzen usually says, so that's terminology but the novelty is that we have a new kind of speech act in addition to assertion.

[…] So, let's call them rules of interaction, in addition to inference rules in the usual sense, which of course remain in place as we are used to them.

[…] Now let's turn to the request mood. And then it's simplest to begin directly with the rules, because the explanation is visible directly from the rules. So, the rules that involve request are these, that if someone has made an assertion, then you may question his assertion, the opponent may question his assertion.

(Req1)

⊢ 𝐶 ? ⊢ 𝑚𝑎𝑦 𝐶 Now we have an example of a rule where we have a may. The other rule says that if we have the assertion ⊢ 𝐶, and it has been challenged, then the assertor must execute his knowledge how to do 𝐶. And we saw what that amounted too in the two Ranta examples, so I will write this schematically that he will continue by asserting zero, one, or more we have two in the existential case so I will call that schematically by 𝐶0.

(Req2)

⊢ 𝐶 ? ⊢ 𝐶 ⊢ 𝑚𝑢𝑠𝑡 𝐶′

The Oslo and the Stockholm lectures of Martin-Löf (2017a; 2017b) contain challenging and deep insights in dialogical logic, and the understanding of defences as duties and challenges as rights is indeed at the core of the deontics underlying the dialogical framework.37 More precisely, the rules Req1 and Req2 do both, they condense the local rules of meaning, and they bring to the fore the normative feature of those rules, which additionally provides a new understanding for Sunholm's notion of implicit interlocutor: once we make explicit the role of the interlocutor, the deontic nature of logic comes out. 38 Moreover, as Martin-Löf points out, and rightly so, they should not be called rules of inference but rules of interaction.

Accordingly, a dialogician might wish to add players X and Y to Req2, in order to stress both that the dialogical rules do not involve inference but interaction, and that they constitute a new approach to the action-based background underlying Lorenzen's (1955) Operative Logik. This would yield the following, where we substitute the horizontal bar for an arrow: 39

⊢ 𝐗 𝐶 ? ⊢ 𝑚𝑎𝑦 𝐘 𝐶 (Req2) ⇓ ? ⊢ 𝑚𝑢𝑠𝑡 𝐗 𝐶 ′
Such a rule does indeed condense the rules of local meaning, but it still does not express the choices while defending or challenging; yet it is the distribution of these choices that determines for example that the meaning of a disjunction is different from that of a conjunction: while in the former case (disjunction) the defender must choose a component, the latter (conjunction) requires of the challenger that, her right to challenge is bounded to her duty to choose the side to be requested (though she might further on request the other side). Hence, the rules for disjunction and conjunction (if we adapt them to Martin-Löf's rules) would be the following: Notice however that these rules only determine the local meaning of disjunction and conjunction, not their global meaning. For example, while classical and constructive disjunction share the same rules of local meaning, they differ at the global level of meaning: in a classical disjunction the defender may come back on the choice he made for defending his disjunction, though in a constructive disjunction this is not allowed, once a player has made a choice he must live with it.

What is more, these rules are not rules of inferences (for example rules of introduction and elimination): they become rules of inference only when we focus on the choices P must take into consideration in order to claim that he has a winning strategy for the thesis. Indeed, as mentioned at the start of the present chapter strategy rules (for P) determine what options P must consider in order to show that he has a method for winning whatever O does, in accordance with the rules of local and global meaning.

The introduction rules on the one hand establish what P has to bring forward in order to assert it, when O challenges it. Thus in the case of a disjunction, P must choose and assert one of the two components. So, P's obligation lies in the fact that he must choose, and so P's duty to choose yields the introduction rule. Compare this with the conjunction where it is the challenger who has the right to choose (and who does not assert but request his choice). But in both cases, defending a disjunction and defending a conjunction, only one conclusion will be produced, not two: in the case of a conjunction, the challenger will ask one after the other (recall that it is an interaction taking place within a dialogue where each step alternates between moves of each of the players).

The elimination rules on the other hand prescribe what moves O must consider when she asserted the proposition at stake. So if O asserted a disjunction, P must be able to win whatever the choices of O be.

The case of the universal quantifier adds the interdependence of choices triggered by the may-moves and the must-moves: if the thesis is a universal quantifier of the form (∀𝑥 ∶ 𝐴) 𝐵(𝑥), P must assert 𝐵(𝑎), for whatever 𝑎 O may chose from the domain 𝐴: this is what correspond to the introduction rule. If it is O who asserted the universal quantifier, and if she also conceded that, 𝑎 ∶ 𝐴, then P may challenge the quantifier by choosing 𝑎 ∶ 𝐴, and request of O that she asserts 𝐵(𝑎); this is how the elimination rule for the universal quantifier are introduced in the dialogical framework (for details see chapter 0). These distinctions can be made explicit if we enrich the first-order language of standard dialogical logic with expressions inspired by CTT. The first task is to introduce statements of the form " 𝑝 ∶ 𝐴". On the right-hand side of the colon is the proposition 𝐴, on the left-hand side is the local reason 𝑝 brought forward to back the proposition during a play. The local reason is therefore local if the force of the assertion is limited to the level of plays. But when the assertion "𝑝 ∶ 𝐴" is backed by a winning strategy, the judgement asserted draws its justification precisely from that strategy, thus endowing 𝑝 with the status of a strategic reason that, in the most general cases, encodes an arbitrary choice of O.

The rock bottom of the dialogical approach is still the play level notion of dialoguedefiniteness of the proposition, namely

For an expression to count as a proposition 𝐴 there must exist an individual play about the statement 𝑿 ! 𝐴, in the course of which 𝑿 is committed to bring forward a local reason to back that proposition, and the play reaches a final position with either win or loss after a finite number of moves according to definite local and structural rules.

The deontic feature of logic is here built directly within the dialogical concept of statements about a proposition. More generally, the point is that, as observed by Martin-Löf (2017a, p. 9), according to the dialogical conception, logic belongs to the area of ethics.

One way of explaining how this important aspect has been overseen or misunderstood might be that the usual approaches to the layers underlying logic got the order of priority between the deontic notions and the epistemic notions the wrong way round. 40Martin-Löf's lectures propose a fine analysis of the inner and outer structure of the statements of logic from the point of view of speech-act theory, that put the order of priority mentioned above right; in doing so it pushes forward one of the most cherished tenets of the dialogical framework, namely that logic has its roots in ethics.

In fact, Martin-Löf's insights on dialogical logic as re-establishing the historical links of ethics and logic provides a clear answer to Wilfried Hodges's (2008) 41 sceptical view in his section 2 as to what the dialogical framework's contribution is. Hodges's criticism seems to target the mathematical interest of a dialogical conception of logic, rather than a philosophical interest which does not seem to attract much of his interest.

In lieu of a general plaidoyer for the dialogical framework's philosophical contribution to the foundations of logic and mathematics, which would bring us too far, let us highlight these three points which result from the above discussions:

1) the dialogical interpretation of epistemic assumptions offers a sound venue for the development of inference-based foundations of logic; 2) the dialogical take on the interaction of epistemic and deontic notions in logic, as well as the specification of the play level's role, display new ways of implementing the interface pragmatics-semantics within logic. 3) the introduction of knowing how into the realm of logic is of great import (Martin-Löf, 2017a;[START_REF] Martin-Löf | Assertion and Request[END_REF].

Obviously, formal semantics in the Tarski-style is blind to the first point, misunderstands the nature of the interface involved in the second, and ignores the third.

Final Remarks

The play level is the level where meaning is forged: it provides the material with which we reason. 42 It reduces neither to the (singular) performances that actualize the interaction-types of the play level, nor to the "tactics" for the constitution of the schema that yields a winning strategy.

We call our dialogues involving rational argumentation dialogues for immanent reasoning precisely because reasons backing a statement, that are now explicit denizens of the objectlanguage of plays, are internal to the development of the dialogical interaction itself. More generally, the emergence of concepts, so we claim, are not only games of giving and asking for reasons (games involving Why-questions) they are also games that include moves establishing how is it that the reason brought forward accomplishes the explicative task. Dialogues for immanent reasoning are dialogical games of Why and How. Notice that the notion of dialogue-definiteness is not bound to knowing how to win-this is rather a feature that characterizes winning strategies; to master meaning of an implication, within the dialogical framework, amounts rather to know how to develop an actual play for it. In this context it is worth mentioning that during the Stockholm and Oslo talks on dialogical logic, Martin-Löf (2017a;[START_REF] Martin-Löf | Assertion and Request[END_REF] points out that one of the hallmarks of the dialogical approach is the notion of execution, which-as mentioned in the preface-is close to the requirement of bringing forward a suitable equality while performing an actual play. Indeed from the dialogical point of view, an equality statement comes out as an answer to a question on the local reason 𝑏 of the form how: How do you show the efficiency of 𝑏 as providing a reason for 𝐴? In this sense the how-question presupposes that 𝑏 has been brought-forward as an answer to a why question: Why does A hold? Thus, equalities express the way how to execute or carry out the actions encoded by the local reason; however, the actualization of a play-schema does not require the ability of knowing how to win a play. Thus, while execution, or performance, is indeed important the backbone of the framework lies in the dialogue-definiteness notion of a play.

The point of the preceding paragraph is that though actualizing and schematizing are processes at the heart of the dialogical construction of meaning, they should not be understood as performing two separate actions: through these actions we acquire the competence that is associated to the meaning of an expression by learning to play both, the active and the passive role. This feature of Dialogical Constructivism stems from Herder's view 43 that the cultural process is a process of education, in which teaching and learning always occur together: dialogues display this double nature of the cultural process in which concepts emerge from a complex interplay of why and how questions.. In this sense, as pointed out by Lorenz (2010a, pp. 140-147) the dialogical teaching-learning situation is where competition, the I-perspective, and cooperation interact, the You-perspective: both intertwine in collective forms of dialogical interaction that take place at the play level.

If the reader allows us to condense our proposal once more, we might say that the perspective we are trying to bring to the fore is rooted in the intimate conviction that meaning and knowledge are something we do together; our perspective is thus an invitation to participate in the open-ended dialogue that is the human pursuit of knowledge and collective understanding, since philosophy's endeavour is immanent to the kind of dialogical interaction that makes reason happen. [START_REF] Brandom | Making it Explicit[END_REF]. Making it Explicit. Cambridge: Harvard University Press. 43 See [START_REF] Herder | Abhandulung über der Ursprung der Sprache[END_REF][START_REF] Herder | Abhandulung über der Ursprung der Sprache[END_REF], Part II).

  𝐗 𝑅 ∧ (𝑝) : 𝐵 Existential quantifiation 𝐗 𝑝: (∃𝑥: 𝐴)𝐵(𝑥) 𝐘 ? 𝐿 ∃ or 𝐘 ? 𝑅 ∃ 𝐗 𝐿 ∃ (𝑝) : 𝐴 (resp.) 𝐗 𝑅 ∃ (𝑝) : 𝐵(𝐿 ∃ (𝑝) ) Subset separation 𝐗 𝑝: {𝑥 ∶ 𝐴 |𝐵(𝑥)} 𝐘 ? 𝐿 or 𝐘 ? 𝑅 𝐗 𝐿 {… } (𝑝) : 𝐴 (resp.) 𝐗 𝑅 ∧ (𝑝) : 𝐵(𝐿 {… } (𝑝) ) 𝐘 𝐿 ¬ (𝑝) : 𝐴 𝐗 𝑅 ¬ (𝑝) : ⊥ Also expressed as 𝐗 𝑝: 𝐴 ⊃⊥ 𝐘 𝐿 ⊃ (𝑝) : 𝐴 𝐗 𝑅 ⊃ (𝑝) : ⊥

  1. A player may ask his adversary to carry out the prescribed instruction and thus bring forward a suitable local reason in defence of the proposition at stake. Once the defender has replaced the instruction with the required local reason we say that the instruction has been resolved. 2. The player index of an instruction determines which of the two players has the right to choose the local reason that will resolve the instruction. a. If the instruction I for the logical constant K has the form I K (p) X and it is Y who requests the resolution, then the request has the form Y ?…/ I K (p) X , and it is X who chooses the local reason. b. If the instruction I for the logic constant K has the form I K (p) Y and it is player Y who requests the resolution, then the request has the form Y p i / I K (p) Y , and it is Y who chooses the local reason.

  P I = a : A SR5.3.1b 𝐏 𝑎 ∶ 𝐴(𝑏) 𝐎 ? = 𝑏 𝐴(𝑏) P I = b : D SR5.3.1c P I = b : D (this statement stems from SR5.3.1b ) 𝐎 ? = 𝐴(𝑏) P A(I) = A(b) : prop Presuppositions: (i) The response prescribed by SR5.3.1a presupposes that O has stated A or a = b : A as the result of the resolution or substitution of instruction I occurring in I : A or in I = b : A. (ii) The response prescribed by SR5.3.1b presupposes that O has stated A and b : D as the result of the resolution or substitution of instruction I occurring in a : A(I). (iii) SR5.3.1c assumes that P I = b : D is the result of the application of SR5.3.1b. The further challenge seeks to verify that the replacement of the instruction produces an equality in prop, that is, that the replacement of the instruction with a local reason yields an equal proposition to the one in which the instruction was not yet replaced. The answer prescribed by this rule presupposes that O has already stated A(b) : prop (or more trivially A(I) = A(b) : prop).

  1 〉(𝐏)𝐴  〈𝐏?∧ 2 〉(𝐏)𝐵 〈𝐎? 〉 (𝐏)𝐵The expressions of the form 〈𝐗 … 〉 constitute interrogative utterances.The expressions of the form 〈𝐗 … 〉 constitute interrogative utterances.

  (O) [or (T)] 𝐴𝑡𝑜𝑛𝑘𝐵 (O) [(T)] 𝐵 (P) [or (F)] 𝐴𝑡𝑜𝑛𝑘𝐵 (P)[(F)] 𝐴

  These rules can be considered as inserting in the rules the back and forth movement described byMartin-Löf (2017a, p. 8) with the following diagram:

  but he is doing this by choosing 𝑏 as local reason for B, that is, by choosing exactly the same local reason as O for the resolution of R  (p).Let us assume that O can ask P to make his choice for a given local reason explicit. P would then answer that his choice for his local reason depends on O's own choice: he simply copied what O considered to be a local reason for 𝐵, that is 𝑅 ∧ (𝑝) 𝑂 = 𝑏: 𝐵. The application of the Socratic rule yields in this respect definitional equality. This rule prescribes the following response to a challenge on an elementary local reason:When O challenges an elementary statement of P such as b : B, P must be able to bring forward a definitional equality such as P R  (p) = b : B.

	Which reads:
	P grounds his choice of the local reason b for the proposition B in O's resolution
	of the instruction R  (p). At the very end P's choice is the same local reason
	brought forward by O for the same proposition B.

.1.2 The substitution rule within dependent statements

  𝐗 𝜋(𝑥 1 , … , 𝑥 𝑛 )[𝑥 𝑖 : 𝐴 𝑖 ] 𝐘 𝜏 1 : 𝐴 1 , … , 𝜏 𝑛 : 𝐴 𝑛 𝐗 𝜋(𝜏 1 , … , 𝜏 𝑛 )

	Existential quantification X (∃𝑥: 𝐴)𝐵(𝑥): 𝒑𝒓𝒐𝒑	Y ? 𝐹 ∃1 or	X 𝐴: 𝒔𝒆𝒕 (resp.)
				Y ? 𝐹 ∃2	X 𝐵(𝑥): 𝒑𝒓𝒐𝒑[𝑥: 𝐴]
	Subset separation	𝐗 {𝑥 ∶ 𝐴 |𝐵(𝑥)}: 𝒑𝒓𝒐𝒑	Y ? 𝐹 1 or	X 𝐴: 𝒔𝒆𝒕 (resp.)
				Y ? 𝐹 2	X 𝐵(𝑥): 𝒑𝒓𝒐𝒑[𝑥: 𝐴]
	Falsum	X ⊥: 𝒑𝒓𝒐𝒑		-	-
	2.2The following rule is not really a formation-rule but is very useful while applying formation
	rules where one statement is dependent upon the other such as 𝐵(𝑥): 𝒑𝒓𝒐𝒑[𝑥: 𝐴]. 11
	Substitution rule within dependent statements (subst-D)
		Move	Challenge	Defence
	Subst-D
				Y ? 𝐹 ∧1	X 𝐴: 𝒑𝒓𝒐𝒑
	Conjunction	X 𝐴 ∧ 𝐵: 𝒑𝒓𝒐𝒑		or	(resp.)
				Y ? 𝐹 ∧2	X 𝐵: 𝒑𝒓𝒐𝒑
				Y ? 𝐹 ∨1	X 𝐴: 𝒑𝒓𝒐𝒑
	Disjunction	X 𝐴 ∨ 𝐵: 𝒑𝒓𝒐𝒑		or	(resp.)
				Y ? 𝐹 ∨2	X 𝐵: 𝒑𝒓𝒐𝒑
				Y ? 𝐹 ⊃1	X 𝐴: 𝒑𝒓𝒐𝒑
	Implication	X 𝐴 ⊃ 𝐵: 𝒑𝒓𝒐𝒑		or	(resp.)
				Y ? 𝐹 ⊃2	X 𝐵: 𝒑𝒓𝒐𝒑
	Universal quantification X (∀𝑥: 𝐴)𝐵(𝑥): 𝒑𝒓𝒐𝒑	Y ? 𝐹 ∀1 or	X 𝐴: 𝒔𝒆𝒕 (resp.)
				Y ? 𝐹 ∀2	X 𝐵(𝑥): 𝒑𝒓𝒐𝒑[𝑥: 𝐴]

  ⟦p 1 A" indicates that P's strategic reason for the negation is based on O's move n (where O is forced to state move 𝑛 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:

			Synthesis of the strategic reason for negation
		Move	Challenge	Defence	Strategic reason (synthesis)
				𝐎 ! ⊥
	Negation	𝐏 ! ¬𝐴 Also expressed as 𝐏 ! 𝐴 ⊃⊥	𝐎 𝑝 1 : 𝐴	P's successful defence of the negation amounts to a switch such that O must now state that she has a local reason for 𝐴. However this move leads her to give up by bringing forward ⊥ (𝑛)	O ⟧ : A The move O p 1 : A, P n O ⟦p 1 allows P to force her to give up in move n, which leads to P's victory.

O

⟧ :

  Note that the analysis of strategic reasons for negation is divided into two presentations of negation, 𝐎 𝑝: ¬𝐴 and 𝐎 𝑝: 𝐴 ⊃⊥, which, at the play level, are governed by SR7 (see p. 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 𝐴 with the means provided by O

			Analysis of local reasons		Analysis of P-
			Challenge	Defence		strategic reasons
	Conjunction	O 𝑝: 𝐴 ∧ 𝐵	𝐏 ? 𝐿 ∧ or 𝐏 ? 𝑅 ∧	𝐎 𝐿 ∧ (𝑝) 𝐎 : 𝐴 (resp.) 𝐎 𝑅 ∧ (𝑝) 𝐎 : 𝐵	𝑷,𝑶 : 𝐴 𝑷,𝑶 : 𝐵 𝐏 𝐿 ∧ (𝑝) 𝑶 = 𝑝 1 (resp.) 𝐏 𝑅 ∧ (𝑝) 𝑶 = 𝑝 2
	Existential quantification	𝐎 𝑝: (∃𝑥: 𝐴)𝐵(𝑥)	𝐏 ? 𝐿 ∃ or 𝐏 ? 𝑅 ∃	𝐎 𝐿 ∃ (𝑝) 𝐎 : 𝐴 (resp.) 𝐎 𝑅 ∃ (𝑝) 𝑂 : 𝐵(𝐿 ∃ (𝑝) 𝐎 )	𝐏 𝐿 ∃ (𝑝) 𝐎 = 𝑝 1 (resp.) 𝐏 𝑅 ∃ (𝑝) 𝐎 = 𝑝 2 𝐏,𝐎 : 𝐵(𝑝 1 𝐏,𝐎 : 𝐴 𝐏,𝐎 )
	Subset separation	𝐎 𝑝: {𝑥 ∶ 𝐴 |𝐵(𝑥)}	𝐏 ? 𝐿 or 𝐏 ? 𝑅	𝐎 𝐿 {… } (𝑝) 𝐎 : 𝐴 (resp.) 𝐎 𝑅 ∧ (𝑝) 𝐎 : 𝐵(𝐿 {… } (𝑝) 𝐎 )	𝐏 𝐿 {… } (𝑝) 𝐎 = 𝑝 1 (resp.) 𝐏 𝑅 ∧ (𝑝) 𝐎 = 𝑝 2 𝐏,𝐎 : 𝐵(𝑝 1 𝐏,𝐎 : 𝐴 𝐏,𝐎 )
	Disjunction	𝐎 𝑝: 𝐴 ∨ 𝐵	𝐏 ? ∨	𝐎 𝐿 ∨ (𝑝) 𝐎 : 𝐴 or 𝐎 𝑅 ∨ (𝑝) 𝐎 : 𝐵	𝐏 𝐿 ∨ (𝑑) 𝐎 = 𝑑 1 = 𝑑 2 𝐏,𝐎 : 𝐶	𝐏,𝐎 |𝑅 ∨ (𝑑) 𝐎
						𝑷 𝑅 ⊃ (𝑝) 𝐎
	Implication	𝐎 𝑝: 𝐴 ⊃ 𝐵	𝐏 𝐿 ⊃ (𝑝) 𝐏 : 𝐴	𝐎 𝑅 ⊃ (𝑝) 𝐎 : 𝐵		= 𝑝 2	𝐏,𝐎 ⟦𝐿 ⊃ (𝑝) 𝐏
						= 𝑝 1	𝐏,𝐎 ⟧ : 𝐵
	Universal quantification	𝐎 𝑝: (∀𝑥: 𝐴)𝐵(𝑥)	𝐏 𝐿 ∀ (𝑝) 𝐏 : 𝐴	𝐎 𝑅 ∀ (𝑝) 𝐎 : 𝐵(𝐿 ∀ (𝑝) 𝐏 )		𝑷 𝑅 ∀ (𝑝) 𝑶 𝑷,𝑶 ⟦𝐿 ∀ (𝑝) 𝐏 = 𝑝 2 = 𝑝 1 𝑷,𝑶 ⟧: 𝐵(𝑝 1 𝐏,𝐎 )
		𝐎 𝑝: ¬𝐴	𝐏 𝐿 ¬ (𝑝) 𝐏 : 𝐴	𝐎 𝑅 ¬ (𝑝) 𝐎 : ⊥		𝑷 𝐿 ¬ (𝑝) 𝑷 = 𝑝 1 𝐏,𝐎 : 𝐴
	Negation	Also expressed as 𝐎 𝑝: 𝐴 ⊃⊥	𝐏 𝐿 ⊃ (𝑝) 𝐏 : 𝐴	𝐎 𝑅 ⊃ (𝑝) 𝐎 : ⊥	P 𝑦𝑜𝑢 𝑔𝑎𝑣𝑒 𝑢𝑝 (𝑛)⟦𝐿 ⊃ (𝑝) 𝐏 =
					𝑝 1	𝑷,𝑶 ⟧ : C
	(𝐿 ¬ (𝑝) = 𝑝 1	𝑶 ).

Erreur ! Signet non défini.).

Ansten Klev's transcription of Martin Löf (2017a, pp. 1-3, 7).

In fact, the present paper relies on the main technical and philosophical results of Rahman/McConaugey/ Klev/Clerbout (2018).

Lorenz (2001, p. 258).

Speaking of local reasons is a little premature at this stage, since only instructions are provided and not actual local reasons; but the purpose is here to give the general idea of local reasons, and instructions are meant to be resolved into proper local reasons, which requires only an extra step.

This rule is an expression at the level of plays of the rule for the substitution of variables in a hypothetical judgement. SeeMartin-Löf (1984, pp. 9-11).

Note that P is allowed to make an elementary statement only as a thesis (Socratic rule); he will be able to respond to the challenge on an elementary statement only if O has provided the required local reason in her initial concessions.

Krabbe (1985, p. 297).

See[START_REF] Martin-Löf | Truth of Empirical Propositions[END_REF].

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 internalizationseePeregrin (2014, pp. 36-42).

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

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.

The fact that these language-games must be finite does not rule out the possibility of a (potentially) infinite number of them.

While establishing particle rules the development rules have not been fixed yet, so we might call those expressions propositional schemata.

With "ideal" we mean an interlocutor that always make the optimal choices in order to collaborate in the task of testing the thesis.

See Rahman (2015) and[START_REF] Rahman | Unfolding parallel reasoning in islamic jurisprudence (I). Epistemic and Dialectical Meaning within Abū Isḥāq al-Shīrāzī's System of Co-Relational Inferences of the Occasioning Factor[END_REF].

Notice that if the role of the Opponent in adversial dialogues is reduced to checking the achievement of logical truth, one would wonder what the role of the Opponent might be in more cooperation-featured dialogues: A soft interlocutor ready to accept weak arguments?

We could provide at the local level of meaning a set of player-independent rules, and add some special structural rule in order to force dialogue-definiteness-seeRahman (2012, p. 225); however, such kinds of rules would produce a mismatch in the formation of black-bullet: the formulation of the particle rule would have to assume that black-bullet is an operator, but the structural rule would have to assume it is an elementary proposition.

This kind of criticism does not seem to have been aware of[START_REF] Lorenz | Elemente der Sprachkritik. Eine Alternative zum Dogmatismus und Skeptizismus in der Analytischen Philosophie[END_REF] 2009; 2010a; 2010b), carrying out a thorough discussion on predication from a dialogical perspective, which discusses the interaction between perceptual and conceptual knowledge. However, perhaps it is fair to say that this philosophical work has not been integrated into the dialogical logic-we will come back to this subject below.

See Lorenz (1981, p. 120), who uses the expressions right to attack and duty to defend.

This crucial insight of Martin-Löf on dialogical logic and on the deontic nature of logic seems to underly recent studies on the dialogical framework which are based on Sundholm's notion of the implicit interlocutor, such as Duthil Novaes (2015) and[START_REF] Trafford | Meaning in Dialogue. An Interactive Approach to Logic and Reasoning[END_REF].

See (Martin-Löf, 2017b, p. 9).

See also[START_REF] Hodges | Dialogue foundations: A sceptical look[END_REF] andTrafford (2017, pp. 87-88).

To usePeregrin's (2014, pp. 228-229) words.