# A Plaidoyer for the Play LeveL

Shahid Rahman, Zoe Mc Conaughey, Ansten Klev, Nicolás Clerbout

► To cite this version:

Shahid Rahman, Zoe Mc Conaughey, Ansten Klev, Nicolás Clerbout. A Plaidoyer for the Play LeveL. 2015. halshs-01226153v2

HAL Id: halshs-01226153

https://shs.hal.science/halshs-01226153v2

Preprint submitted on 13 Feb 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
IMMANENT REASONING OR
EQUALITY IN ACTION

A PLAIDOYER FOR THE PLAY LEVEL

Shahid Rahman,<fnref n="1" /> Zoe McConaughey,<fnref n="2" /> Ansten Klev,<fnref n="3" /> Nicolas Clerbout<fnref n="4" />

<footnote n="1">¹ Univ. Lille, CNRS, UMR 8163 - STL - Savoirs Textes Langage, F-59000 Lille, France, ADA-MESHS (NPdC)</footnote>

<footnote n="2">² Univ. Lille, CNRS, UMR 8163 - STL - Savoirs Textes Langage, F-59000 Lille, France and Université du Québec à Montréal</footnote>

<footnote n="3">³ Academy of Sciences of the Czech Republic</footnote>

<footnote n="4">⁴ Instituto de Filosofia, Universidad de Valparaíso. The results of the present work have been developed in the frame of the Project: Fondecyt Regular N° 1141260.</footnote>
<figure><img src="image_2.png" /></figure>
To all of the present and past members of
the Dialogicians' team of Lille and beyond
# TABLE OF CONTENTS

TABLE OF CONTENTS..................................................................................1

PREFACE ........................................................................................................6

Acknowledgments:................................................................................................10

I. INTRODUCTION: SOME BRIEF HISTORICAL AND PHILOSOPHICAL
REMARKS....................................................................................................11

I.1 The dialogical turn and the operative justification of intuitionistic logic..................11

I.1.1 Admissibility in operative logic ........................................................................12

I.1.2 Implication and admissibility: another circle?..................................................12

I.1.3 From admissibility to dialogue-definiteness ....................................................13

I.2 Linking Dialogues and Constructive Type Theory ....................................................15

I.2.1 Equality and the Socratic Rule ........................................................................15

I.2.2 Local Reasons and Content: The Socratic Rule within *Material Dialogues*........17

I.2.3 Dialogues for Immanent Reasoning as *Games of Why and How*....................18

I.3 A Basic Overview of the Book........................................................................18

II. A BRIEF INTRODUCTION TO CONSTRUCTIVE TYPE THEORY......20

II.1 Judgements and categories................................................................................20

II.1.1 Forms of categorical judgement ........................................................................20

II.1.2 Categories ................................................................................................................22

II.1.3 General rules of judgemental equality .................................................................23

II.1.4 Propositions ................................................................................................................24

II.1.5 Forms of hypothetical judgement........................................................................25

II.1.6 Assumptions and other speech acts........................................................................27

II.1.7 Hypothetical judgements with more than one assumption..................................28

II.2 Rules.................................................................................................................................29

II.2.1 Cartesian product of a family of sets.................................................................30

II.2.2 The logical interpretation of the Cartesian product ........................................31

II.2.3 Disjoint union of a family of sets ........................................................................33

II.2.4 The logical interpretation of the disjoint union of a family of sets ....................35

II.2.5 Disjoint union of two sets ....................................................................................35

II.2.6 Finite sets....................................................................................................................36

II.2.7 The natural numbers ..................................................................................................38

II.2.8 Propositional identity..................................................................................................39

Exercises .................................................................................................................................44

Solutions .................................................................................................................................45

III. BASIC NOTIONS FOR DIALOGICAL LOGIC........................................51

III.1 The general framework ....................................................................................51

Dialogues and interaction..................................................................................................51

Particle rules ....................................................................................................................51

Structural rules..................................................................................................................52

III.2 The rules at the play level................................................................................53

III.2.1 Particle rules ........................................................................................................53

III.2.2 Structural rules........................................................................................................55
<table><tr><td>III.3</td><td>Building a dialogue: step-by-step instructions</td><td>56</td></tr><tr><td></td><td>Setting up the game</td><td>56</td></tr><tr><td></td><td>Playing the game</td><td>56</td></tr><tr><td></td><td>Ending the game</td><td>57</td></tr></table>

<table><tr><td>III.4</td><td>Commented construction of a play: A ∧ B ⊃ A</td><td>57</td></tr></table>

<table><tr><td>Exercises</td><td>59</td></tr></table>

<table><tr><td>Solutions</td><td>59</td></tr></table>

<table><tr><td>III.5</td><td>Approaching the strategy level</td><td>59</td></tr><tr><td></td><td>Building a P-winning strategy step-by-step</td><td>60</td></tr><tr><td></td><td>Exercise</td><td>61</td></tr><tr><td></td><td>Solution</td><td>61</td></tr></table>

<table><tr><td>III.6</td><td>Rounding up some key notions</td><td>62</td></tr></table>

<table><tr><td>III.7</td><td>Further reading</td><td>63</td></tr><tr><td></td><td>Textbook presentations</td><td>63</td></tr><tr><td></td><td>Logical studies in dialogic</td><td>63</td></tr><tr><td></td><td>On the use of the dialogical framework in epistemology, philosophy and history of ideas</td><td>63</td></tr></table>

## IV. ADVANCED DIALOGUES: PLAY LEVEL 64

<table><tr><td>IV.1</td><td>Preliminary notions</td><td>64</td></tr><tr><td></td><td>The language</td><td>64</td></tr><tr><td></td><td>Plays</td><td>64</td></tr><tr><td></td><td>Dialogical games</td><td>65</td></tr><tr><td></td><td>A move in a play</td><td>65</td></tr><tr><td></td><td>Challenges and defences</td><td>65</td></tr><tr><td></td><td>Terminological note: challenge, attack and defence</td><td>65</td></tr></table>

<table><tr><td>IV.2</td><td>Local meaning of logical constants</td><td>65</td></tr><tr><td></td><td>Particle rules</td><td>65</td></tr><tr><td></td><td>Summing up</td><td>67</td></tr></table>

<table><tr><td>IV.3</td><td>Symmetry and harmony</td><td>67</td></tr></table>

<table><tr><td>IV.4</td><td>Global meaning:</td><td>68</td></tr><tr><td>IV.4.1</td><td>Preliminary terminology</td><td>69</td></tr><tr><td>IV.4.2</td><td>The structural rules</td><td>69</td></tr><tr><td></td><td>Linking the Copy-cat rule (SR2) and equality</td><td>70</td></tr></table>

<table><tr><td>IV.5</td><td>Examples of plays</td><td>71</td></tr><tr><td></td><td>First example, the third excluded: A ∨ ¬A</td><td>71</td></tr><tr><td></td><td>Second example, the double negation elimination: ¬¬A ⊃ A</td><td>72</td></tr><tr><td></td><td>Third example, the double negation of the third excluded: ¬¬(A ∨ ¬A)</td><td>73</td></tr></table>

## V. ADVANCED DIALOGUES: STRATEGY LEVEL 74

<table><tr><td>V.1</td><td>Preliminary notions</td><td>74</td></tr><tr><td>V.1.1</td><td>Definitions</td><td>74</td></tr><tr><td>V.1.2</td><td>Some results from existing literature on the strategy level</td><td>75</td></tr></table>

<table><tr><td>V.2</td><td>Developing a dialogical demonstration: reaching the core of a strategy</td><td>76</td></tr><tr><td>V.2.1</td><td>Features essential to the procedure yielding the core of a strategy</td><td>76</td></tr></table>

<table><tr><td>V.3</td><td>Heuristical presentation of the core (succession of plays)</td><td>80</td></tr><tr><td>V.3.1</td><td>Procedure</td><td>81</td></tr></table>

<table><tr><td>Two examples of the heuristical procedure</td><td>82</td></tr><tr><td>First example: A ∨ B ∧ ¬A ⊃ B</td><td>83</td></tr></table>
Second example: $A \lor B \land C \land \neg A \supset B \land C \land (D \lor E \supset D \lor E)$. 84

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

The graphic presentation without the heuristic procedure 87

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

Two examples of the graphic presentation of the core 89

First example: $A \lor B \land \neg A \supset B$. 89

Second example: $A \lor B \land C \land \neg A \supset B \land C \land D \lor E \supset D \lor E$. 90

VI. LOCAL REASONS AND DIALOGUES FOR IMMANENT REASONING 91

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

VI.2 Local reasons and material truth. 93

Approaching material truth 94

Material truth and local reasons 94

Material dialogues and formal dialogues 94

VI.3 The local meaning of local reasons 95

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

VI.3.2 Synthesis of local reasons 97

VI.3.3 Analysis of local reasons 99

VI.4 From Reasons to Equality 100

VII. THE DIALOGICAL ROOTS OF EQUALITY: DIALOGUES FOR IMMANENT REASONING 105

VII.1 Local meaning in dialogues for immanent reasoning 105

VII.1.1 The formation rules 105

Example of a formation-play 106

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

VII.2 Global Meaning in dialogues for immanent reasoning 111

VII.2.1 Structural Rules 111

VII.2.2 Rules for the transmission of definitional equality 115

VII.3 Example: $\forall x: DQx \supset Qx$. 116

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

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

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

Recalling the O-decisions: 118

Recalling left and right decisions: 118

Getting rid of infinite ramifications in a strategy: 118

Local reasons and proof-objects: 118

Disregarding formation rules for formal plays 119

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

Example: obtaining the core for $\forall x: DQx \supset Qx$. 119

Litterature on the link between CTT and the dialogical framework: 120

VII.6 Exercises and solutions 121

Solutions 121

VII.6.1 $B \lor A c: A \lor B$. 121

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

VII.6.3 $A \land A \supset \bot \supset \bot$. 122

VII.6.4 $A \supset B \supset A \supset A$. 122

VII.6.5 $A \land B \supset \bot \supset A \supset B \supset \bot$. 123

VII.6.6 $*A \land B \land C c: A \land B \land C$. 123
<table><tbody><tr><td>X.3</td><td>Mathematics and logic</td><td>200</td></tr><tr><td>X.3.1</td><td>Material dialogues for N</td><td>200</td></tr><tr><td>X.3.2</td><td>Beyond Bool: Finite Sets and Large Sets of Answers</td><td>203</td></tr><tr><td>X.3.3</td><td>The set Bool and some applications to mathematics and logic</td><td>204</td></tr><tr><td>X.4</td><td>Empirical Quantities and Material Dialogues</td><td>211</td></tr><tr><td>X.4.1</td><td>Empirical Quantities as Finite Sets of Answers</td><td>211</td></tr><tr><td>X.4.2</td><td>Dependent Empirical Quantities</td><td>213</td></tr><tr><td>X.4.3</td><td>Conclusion on Empirical Quantities</td><td>216</td></tr><tr><td>X.5</td><td>Some General Epistemological Consequences</td><td>217</td></tr><tr><td>X.5.1</td><td>Play Level and Material Dialogues</td><td>217</td></tr><tr><td>X.5.2</td><td>The Dialogical Internalization and the Myth of the Given</td><td>220</td></tr><tr><td colspan="2">XI. CONCLUDING REMARKS: A PLAIDOYER FOR THE PLAY LEVEL 222</td><td></td></tr><tr><td>XI.1</td><td>Dialogue-Definiteness and Propositions</td><td>222</td></tr><tr><td>XI.2</td><td>The Built-in Opponent and the Neglect of the Play Level</td><td>226</td></tr><tr><td>XI.3</td><td>Pathological cases and the Neglect of the Play Level</td><td>228</td></tr><tr><td>XI.3.1</td><td>The tonk challenge and player-independence of local meaning</td><td>229</td></tr><tr><td>XI.3.2</td><td>The black-bullet challenge and dialogue-definiteness</td><td>231</td></tr><tr><td>XI.4</td><td>Other than logical constants</td><td>232</td></tr><tr><td>XI.5</td><td>Normativity and the Dialogical Framework: A New Venue for the Interface Pragmatics-Semantics</td><td>233</td></tr><tr><td>XI.6</td><td>A brief historical study on material dialogues</td><td>238</td></tr><tr><td></td><td>Identifying versus Individuating</td><td>241</td></tr><tr><td>XI.7</td><td>Intersubjectivity, Dialogues, and Learning</td><td>242</td></tr><tr><td>XI.8</td><td>Final Words</td><td>245</td></tr><tr><td colspan="2">APPENDIX: MAIN NOTATION FOR CTT</td><td>246</td></tr><tr><td colspan="2">BIBLIOGRAPHY</td><td>247</td></tr><tr><td colspan="2">INDEX OF TABLES</td><td>257</td></tr><tr><td colspan="2">LIST OF EXERCISES AND EXAMPLES</td><td>265</td></tr></tbody></table>
# PREFACE

Prof. Göran Sundholm of Leiden University inspired the group of logicians who nowadays develop their work in Lille and Valparaíso to undertake a fundamental review of the dialogical conception of logic by linking it to Constructive Type Logic. One of Sundholm's insights was that inference can be understood as involving an *implicit interlocutor*. This led to several investigations whose purpose was to explore the consequences of joining winning strategies to the proof-theoretical conception of meaning: while introduction rules lay down the conditions under which a winning strategy for the Proponent can be built, the elimination rules lay down precisely those elements of the Opponent's assertions that the Proponent has the right to use for building a winning strategy. The pragmatic and ethical features of obligations and rights naturally brings forth the dialogical interpretation of natural deduction.

During the 2012 Visiting Professorship of Prof. Sundholm in Lille, the logic group of Lille started probing possible ways of implementing Per Martin-Löf's Constructive Type Theory (CTT)<fnref n="5" /> in the dialogical perspective. The first publication in particular on the subject—Aarne Ranta's (1988) paper—was read and discussed during Sundholm's seminar. These discussions strongly suggested that the game-theoretical conception of quantifiers, which marshalls interdependent moves, provides a natural link between CTT and dialogical logic. This idea triggered several publications by the group of Lille in collaboration with Nicolas Clerbout and Juan Redmond at the University of Valparaíso, including that of the (2015) book by Clerbout & Rahman providing a systematic development of this way of linking CTT and the dialogical conception of logic.

However the (Clerbout & Rahman, 2015) book was written from the CTT perspective on dialogical logic, rather than the other way round. The present book, *Immanent Reasoning or Equality in Action*, should provide the other perspective in the dialogue between the dialogical framework and Constructive Type Theory.

In order to develop a dialogical perspective on the links between CTT and dialogical logic we will follow three complementary paths:

A. One of the chief ideas animating our study is that we believe Sundholm's (1997)<fnref n="6" /> notion of *epistemic assumption* is closely linked to the *Copy-Cat rule* or *Socratic rule* that distinguishes the dialogical framework from any other game-theoretical approach; this link is established through the dialogical understanding of definitional equality.

B. We will join—with some nuances linked to point C below—Martin-Löf's (2017a; 2017b) suggestions that the new insights provided by the dialogical framework mainly amount to the following three interconnected points:

B.1. the introduction of *rules of interaction* rather than of inference rules;

B.2. the challenge to what Kuno Lorenz (2010a, p. 71) calls the *semantization of pragmatics*: deontic features are formalized with the help of specific propositional operators (and indexes) upon which the truth-value of the resulting proposition is made dependent;

B.3. the central role of the notion of *execution* in the rules of interaction: executions are responses to questions of *knowing how*.

<footnote n="5">⁵ For an overview see for instance (Nordström, Petersson, & Smith, 1990; 2000), (Primiero, 2008), (Thompson, 1991).</footnote>

<footnote n="6">⁶ See also (Sundholm, 1998; 2012; 2013b).</footnote>
C. As indicated by the subtitle, “A Plaidoyer for the Play Level”, we will stress the importance of the play level over the strategy level: this binds the point of execution with that of equality.

In relation to A and B.3, the present book can indeed be read as furthering Sundholm’s own extension to inference of Austin’s remark (1946, p. 171) on assertion acts; Sundholm (2013a, p. 17) did indeed produce this forceful formulation:

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

In recent lectures, Per Martin-Löf used the dialogical perspective with epistemic assumptions 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

$$ \frac{J_1 \dots J_n}{J} $$

is valid means that one can make the conclusion (judgement J) evident on the assumption that $J_1, \dots, J_n$ 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:

### A. Martin-Löf's circularity problem

> The circularity problem is this: if you define a demonstration to be a chain of immediate inferences, then you are defining demonstration in terms of inference. Now we are considering an immediate inference and we are trying to give a proper explanation of that; but, if that begins by saying: Assume that $J_1, \dots, J_n$ have been demonstrated—then you are clearly in trouble, because you are about to explain demonstration in terms of the notion of immediate inference, hence when you are giving an account of the notion of immediate inference, the notion of demonstration is not yet at your disposal. So, to say: Assume that $J_1, \dots, J_n$ have already been demonstrated, makes you accusable of trying to explain things in a circle. The solution to this circularity problem, it seems to me now, comes naturally out of this dialogical analysis. [...]

> The solution is that the premisses here should not be assumed to be known in the qualified sense, that is, to be demonstrated, but we should simply assume that they have been asserted, which is to say that others have taken responsibility for them, and then the question for me is whether I can take responsibility for the conclusion. So, the assumption is merely that they have been asserted, not that they have been demonstrated. That seems to me to be the appropriate definition of epistemic assumption in Sundholm's sense.<fnref n="7" />

The present study makes a further step, namely that of relating judgemental equality with the rule known in the literature as the *Copy-Cat rule*, or *Formal rule*, or, as more aptly called now by (Marion & Rückert, 2015), the *Socratic rule*.<fnref n="8" /> We hold it as one of our main tenets that this relation provides both a simpler and a more direct way to implement the Constructive Type Theoretical approach within the dialogical framework. Such a reconsideration of the Socratic rule roughly amounts to the following:

1. When Proponent P makes a move bringing forward a local reason—say b—to defend an elementary proposition A, this move can be challenged by the

<footnote n="7">⁷ Transcription by Ansten Klev of Martin-Löf's talk in May 2015 (Martin-Löf, 2015).</footnote>

<footnote n="8">⁸ See for instance below, section III.2.2 or section VII.2.1.</footnote>
Opponent **O**. That is, given **P** *b*: *A*, the antagonist may play the attack **O**? = *b*.

2. To respond to such a challenge from **O**, **P** must bring forward a definitional equality explicating that the local reason chosen by **P** copies precisely the reason **O** chose when stating *A*. In short, this equality expresses at the object-language level the fact that **P**'s defence move rests on the authority **O** has previously asserted when producing her local reason.

More generally, according to this view a definitional equality established by **P** and brought forward while defending the proposition *A* expresses the equality between a local reason (introduced by **O**) on the one hand, and the instruction on the other hand used for building a local reason brought forward by **O** when stating *A*. A definitional equality can therefore be read as a computation rule indicating how to compute the instructions **O** brought forward during a play.<fnref n="9" />

From the dialogical perspective though, providing local reasons must be distinguished from providing equalities: while providing an explicit local reason *b* is a way of answering a *why* question, such as “why does *A* hold?”, providing an equality is more a way of answering a *how* question, such as “how do you show that *b* accomplishes the explicative task?”. Equalities thus express how to execute or carry out the actions encoded by the local reasons.

Let us recall that from the strategic point of view, **O**'s moves correspond to elimination rules (including the selector-functions deployed by these rules) of demonstrations. Thus, the dialogical rules prescribing how to introduce a definitional equality correspond—at the strategy level—to the definitional equality rules for CTT as applied to the selector-functions involved in the elimination rules.

We are in this fashion extending the dialogical interpretation of Sundholm's *epistemic assumption* to the rules that set up the definitional equality of a type. Actually, Sundholm (2017) himself suggests in his section 4 this extension when he points out that if some object, say *a*, is granted by a suitable *epistemic assumption* to be a proof-object of *C*, then it *executes to a canonical proof of C*. In other words, on the grounds of the *epistemic assumption* we know that *a* must be equal to a canonical element of *C*.

Notice however that from the dialogical perspective equalities grounded on the sole authority of the Opponent (i.e. on *epistemic assumptions*) are a trade-mark of what we call *formal dialogues*.

Yet the dialogical perspective also includes *material dialogues*, where the Opponent must carry out some process *specific* to the proposition at stake before the Proponent can answer to the *how*-question with a suitable equality. In other words, though equalities of material dialogues are the result of the application of the Socratic rule, they are not “merely” grounded on *epistemic assumptions*.

In relation to **B1** and **B2**, the Oslo and 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 deontic feature underlying the dialogical framework. More precisely, these two rules *Req1* and *Req2*:

$$ (Req 1) \frac{\vdash C}{? \vdash_{may} C} $$

and

<footnote n="9">⁹ These elements are formalized in the Socratic rule for immanent reasoning, section VII.2.1.</footnote>
$$ (\text{Req 2}) \frac{\vdash C \qquad ? \vdash C}{\vdash_{\text{must}} C'} $$

both condense the particle rules of meaning and bring to the fore the normative feature of those rules. What is more, Martin-Löf points out rightly that they should not be called *rules of inference* but *rules of interaction*.

Still, a dialogician might wish to draw further distinctions to the divide between play level rules and those of the strategy level, such as distinctions between players, or the distinction in terms of choice as to how to defend or challenge moves: it is such a distribution of choices that distinguishes the meaning for instance of the conjunction and of the disjunction; the meaning of a disjunction binds the right to state a disjunction with the *defender's duty to choose* a component of the disjunction to defend, but the meaning of the conjunction binds the right to challenge it with the *challenger's duty to choose* the side to be requested.<fnref n="10" />

On our view, point C is at the core of the innovations of the dialogical framework and our point of departure from Ranta's (1988) seminal paper: he proposes to identify proof-objects with winning-strategies, so that we have canonical and non-canonical winning-strategies. Winning strategies are however not primitive in the dialogical framework, but are constituted by some finite sequence of legal moves (that is, a sequence of moves which observes the game rules) called plays. The notion of plays is what grounds meaning within the dialogical framework, and this notion also leads to the notion of proposition: in the standard presentation of dialogical logic a proposition is defined as a *dialogue-definite expression*, that is, an expression A such that there is an individual play about A that can be said to be lost or won after a finite number of steps, following some given rules of dialogical interaction.<fnref n="11" />

As discussed in chapter III and section XI.1, the rock-bottom of the dialogical approach to CTT is the play level notion of dialogue definiteness of the proposition. Thus to paraphrase (Lorenz, 2001, p. 258): *for an expression to count as a proposition A there must exist an individual play about the statement X! A*, in the course of which X is committed to bring forward a local reason to back that proposition, play which must reach a final position with either win or loss after a finite number of moves according to definite particle and structural rules.

Though performing the interaction schemata defining a play is in this sense a crucial aspect of the dialogical framework, it must be stressed that the actualization of a play (performing it) *does not* require winning the play. Immanent reasoning thus conceives *performance* as *putting dialogue definiteness into action*.

In a nutshell, we call our dialogues involving rational argumentation *dialogues for immanent reasoning* precisely because the *reasons* backing a statement, now *explicit denizens* of the object-language of plays, *are internal* to the development of the dialogical interaction itself: the emergence of concepts are not only games of giving and asking for reasons (games involving *why*-questions), they are also games including moves establishing *how is it that the reason brought forward accomplishes the explicative task*. Immanent reasoning is thus a dialogical framework for games of *why* and *how*.

<footnote n="10">¹⁰ In the conclusion we enrich Martin-Löf's (2017a; 2017b) rules Req1 and Req2 with players and with choice-options.</footnote>

<footnote n="11">¹¹ See for instance (Lorenz, 2001, p. 258): "[...] *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.*" See also below chapter III and conclusion XI.1.</footnote>
## Acknowledgments:

Many thanks to Mark van Atten (Paris1), Giuliano Bacigalupo (Zürich), Charles Zacharie Bowao (Univ. Ma Ngouabi de Brazzaville, Congo), Christian Berner (Lille3), Michel Crubellier (Lille3), Pierre Cardascia (Lille3), Oumar Dia (Dakar), Marcel Nguimbi (Univ. Marien Ngouabi de Brazzaville, Congo), Adjoua Bernadette Dango (Lille3 / Alassane Ouattara de Bouaké, Côte d'Ivoire), Stephen Rossy Eckoubili (Lille3), Johan Georg Granström (Zürich), Gerhard Heinzmann (Nancy2), Muhammad Iqbal (Lille3), Matthieu Fontaine (Lille3), Radmila Jovanovic (Belgrad), Hanna Karpenko (Lille3), Laurent Keiff (Lille3), Sébastien Magnier (Saint Dennis, Réunion), Clément Lion (Lille3), Gildas Nzokou (Libreville), Juan Redmond (Valparaíso), Fachrur Rozie (Lille3), Helge Rückert (Mannheim), Mohammad Shafiei (Paris1), and Hassan Tahiri (Lisbon), for rich interchanges, suggestions on the main claims of the present study and proof-reading of specific sections of the text.

Special thanks to Kuno Lorenz (Univ. Saarland) and Mathieu Marion (Montreal), for many suggestions and inspired discussions.

Special thank also to Gildas Nzokou (Libreville), Stephen Rossy Eckoubili (Lille) and Clément Lion (Lille), who are working out through a visiting professorship of Gildas Nzokou in Lille a Pre-Graduate Textbook in French on dialogical logic and CTT. In the present book, Eckoubili is the author of the sections with exercises for dialogical logic.

We are also very thankful to our host institutions which have fostered our researches in the framework of specific research-programs: the results of the present work have been developed in the frameworks of

* the transversal research axis *Argumentation* (UMR 8163: STL),

* the research project ADA at the MESH-S-Nord-pas-de-Calais and

* the research projects: ANR-SÊMAINÔ (UMR 8163: STL) and

* Fondecyt Regular N° 1141260 (Chile).

Shahid Rahman,<fnref n="12" /> Zoe McConaughey,<fnref n="13" />

Ansten Klev,<fnref n="14" /> Nicolas Clerbout<fnref n="15" />

<footnote n="12">¹² Univ. Lille, CNRS, UMR 8163 - STL - Savoirs Textes Langage, F-59000 Lille, France, ADA-MESH S (NPdC)</footnote>

<footnote n="13">¹³ Univ. Lille, CNRS, UMR 8163 - STL - Savoirs Textes Langage, F-59000 Lille, France and Université du Québec à Montréal</footnote>

<footnote n="14">¹⁴ Academy of Sciences of the Czech Republic</footnote>

<footnote n="15">¹⁵ Instituto de Filosofía, Universidad de Valparaíso. The results of the present work have been developed in the frame of the Project: Fondecyt Regular N° 1141260.</footnote>
# I. INTRODUCTION: SOME BRIEF HISTORICAL AND PHILOSOPHICAL REMARKS

The present volume develops a new way of linking Constructive Type Theory (CTT) with dialogical logic by following these three complementary paths, as mentioned in the preface:

A. The path observing that Sundholm's (1997)<fnref n="16" /> notion of *epistemic assumption* is closely linked to the *Copy-cat* and *Socratic rules*<fnref n="17" /> and that it provides the dialogical conception of definitional equality;

B. the path joining (in principle) Martin-Löf in his (2017a; 2017b) suggestions, according to which the new insights provided by the dialogical framework mainly amount to the following three interconnected points:

B.1. the introduction of *rules of interaction* rather than of rules of inference;

B.2. the challenge to the *semantization of pragmatics* and the claim of the deontic nature of logic;<fnref n="18" />

B.3. the central role of the notion of *execution* in the rules of interaction: executions are responses to questions of *knowing how*.

C. The path stressing the importance of the *play level* and the associated notion of *dialogue-definiteness*.

Before displaying some of the conceptual background behind the project we will first make some brief historical remarks concerning the *dialogical turn* that took Lorenzen (1955) from his *Operative Logik* to the inception of *dialogical logic*.

## I.1 The dialogical turn and the operative justification of intuitionistic logic

The origins of a deontic nature of logic in its dialogical conception can be traced back to Paul Lorenzen's 1958 endeavour of overcoming difficulties specific to his (1955) *Einführung in die Operative Logik und Mathematik* (1955), which lead him to turn the normative perspectives of the operative logic into the dialogical framework. We will here closely follow Schroeder-Heister's thorough (2008) paper on the subject.<fnref n="19" /> It should be noted that these difficulties are reminiscent of Martin-Löf's circularity puzzle mentioned in the Preface and which motivated his dialogical interpretation of the notion of epistemic assumption (see p. 7).

<footnote n="16">¹⁶ See also (Sundholm, 1998; 2012; 2013a).</footnote>

<footnote n="17">¹⁷ See section III.2.2 for the Copy-cat rule, and section VII.2.1 for the Socratic rule.</footnote>

<footnote n="18">¹⁸ In fact, as opposed to Martin-Löf's understanding of dialogical logic, Lorenz's dialogical constructivism does not only reject the *semantization of pragmatics* in which deontic features are formalized using specific propositional operators and indexes upon which depends the truth-value of the resulting proposition, but it also rejects the *pragmatization of semantics* in which a propositional kernel is complemented by moods yielding assertions, questions, commands, and so on. According to dialogical constructivism, pragmatic and semantic features are produced within one and the same act. See (Lorenzen, 1969), (Kamlah & Lorenzen, 1972), (Lorenzen & Schwemmer, 1975). It is precisely this tenet on the dual nature of actions in both their *significative* and *communicative* role, thoroughly worked out by Lorenz (2010a, pp. 71-80), that leads to this central claim that logic is part of ethics—see section XI.5 for further details.</footnote>

<footnote n="19">¹⁹ See also Lorenz's (2001) study of the origins of the dialogical approach to logic.</footnote>
### I.1.1 Admissibility in operative logic

In the context of the operative justification of intuitionistic logic, the operative meaning of an elementary proposition is understood as a proof of its derivability in relation to some given calculus. Calculus is here understood as a general term close to the *formal systems* of Curry (1951) which include basic expressions, and rules for producing complex expressions out of basic ones. More precisely, as Schroeder-Heister puts it:

> Lorenzen starts with elementary calculi (OL, §1) which permit to generate words (strings of signs) over an arbitrary (finite) alphabet. The elements of the alphabet are called atoms, the words are called sentences ("Aussagen"). A calculus K is specified by giving certain initial formulas ("Anfänge") A and rules $A_1, \dots, A_n \rightarrow A$.<fnref n="20" />

Instead of starting with the functor-argument structure common in logic, Lorenzen starts here with an arbitrary word-structure, where expressions in K are just strings of atoms and variables, allowing his notion of calculus to be particularly general.

In such a framework, logic is introduced as a system of proof procedures for asserting the *admissibility* of rules:<fnref n="21" />

> A rule R is called admissible in a calculus K, if its addition to the primitive rules of K—resulting in an extended calculus $K + R$—does not enlarge the set of derivable sentences. If $\vdash_K A$ denotes the derivability of A in K, then R is admissible in K if

$$ \vdash_{K+R} A \text{ implies } \vdash_K A $$

for every sentence A.

Thus, implication is explained in terms of admissibility. But how is admissibility to be explained?

### I.1.2 Implication and admissibility: another circle?

Since implication is explained by the notion of admissibility, admissibility cannot be explained by the notion of implication. In fact, Lorenzen (1955) in his chapter 3 invests admissibility with an operative meaning through the notion of an *elimination procedure*, stating that R is admissible in K if every application of R can be eliminated from every derivation in $K + R$. The above implication ($\vdash_{K+R} A$ implies $\vdash_K A$) reduces to a form of elimination procedure, for the derivation in $K + R$ can be brought down to a derivation which no longer uses R: the R rule can be disposed of. Schroeder-Heister thus concludes:

> According to Lorenzen, this is the sort of insight (evidence) on which constructive logic and mathematics is based. It goes beyond the insight that something is derivable in K, but is still something which has a "definite" meaning. (Schröder-Heister, 2008, p. 217)

This approach thus goes beyond the formalistic focus on derivability: what provides meaning is *the further understanding gained through the notion of admissibility*. In this respect, according to Schröder-Heister:

> Lorenzen's theory of implication is based on the idea that an implicational sentence $A \rightarrow B$ expresses the admissibility of the rule $A \rightarrow B$, so the assertion of an implication is justified if this implication, when read as a rule, is admissible. In this sense an implication expresses a meta-statement about a calculus. This has a clear meaning as long as there is no iteration of the implication sign. (Schröder-Heister, 2008, p. 222)

<footnote n="20">²⁰ (Schröder-Heister, Lorenzen's Operative Justification of Intuitionistic Logic, 2008). All the following quotations of this section, if not otherwise specified, will come from this same source.</footnote>

<footnote n="21">²¹ Nowadays, the notion of *admissibility* is a fundamental concept of proof-theory; Schröder-Heister (2008, p. 218) pointed out that Lorenzen was the one to have coined this term.</footnote>
It is precisely to deal with iterated implications that Lorenzen develops the idea of finitely iterated meta-calculi. Schröder-Heister (2008, p. 235) points out that the operative approach has its own means to draw the distinction between *direct* and *indirect inferences*, a distinction which triggered Martin-Löf's puzzle quoted in our preface (see p. 7). In this sense, the implication $A \to B$ can be asserted as either

(i) *a direct derivation* in a meta-calculus *MK*, based on a demonstration of the admissibility in *K* of the rule $A \to B$, or as

(ii) *an indirect derivation* by means of a formal derivation in *MK* using axioms and rules already shown to be valid.

In the context of operative logic, *direct knowledge* or *canonical inference* of the implication $A \to B$ is obtained by the demonstration of the admissibility in *K* of the rule $A \to B$, and *indirect knowledge* or *non-canonical inference* results from the derivation of $A \to B$ by means of rules already established as admissible.

### I.1.3 From admissibility to dialogue-definiteness

There is however a high price to pay for this way out of the circularity problem, as knowledge cannot be characterized in the required way showing that the reasoner actually masters the meaning of an implication. Schröder-Heister (2008, p. 236) indeed pointed out that in the Gentzen-style introduction rule for implication, the conclusion prescribes that there is a derivation of the consequent from the antecedent, *independently of the validity of the hypothetical derivation* itself. Indeed, the meaning explanation of the implication is based on the idea that from the assumption of a derivation of the antecedent a method can be found that transforms the derivation in one of the consequent.

This undesired consequence on knowledge motivated Lorenzen to move to the dialogical framework in which the *play level* takes care of all the issues on meaning and *strategies* are associated to validity features: in this context, a proof of admissibility amounts to showing that some specific sequence of plays yields a winning strategy.

Now, if dialogues are to be conceived as mediators of meaning, these dialogues must be games actually playable by human beings: it must be the case *that we can actually perform them*—see our chapter XI.1.<fnref n="22" /> These games must therefore be finite, though this does not excluded that there might be a (potentially) infinite number of them. In fact it is the notion of *dialogue-definiteness* that provides both, the basis for implementing the requirement of human-playable games, and the notion of proposition. Under such a background a proposition is defined as a dialogue-definite expression, that is, an expression *A* such that there is an individual play about *A*, that can be said to be lost or won after a finite number of steps, following some given rules of dialogical interaction.

Notice however 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; 2017b) 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 (see I.2.2), an equality statement comes out as an answer to a question on the local reason *b* of the form *how: How do you show the efficiency of b as providing a reason for A?* In this sense the *how*-question presupposes that *b* has been brought-forward as an

<footnote n="22">²² See also (Marion, 2006, p. 231).</footnote>
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—see our point B.3 above, the backbone of the framework lies in the *dialogue-definiteness notion of a play*.

Perhaps a way of formulating the distinction we are aiming at is to stress the difference between *ability* and *knowing how*. In this context, one might speak of *ability* in the sense of the *ability to win*—in a way not far from Peregrin’s (2014, pp. 228-229) notion of *tactics*—, but *ability* has strategy level underpinnings rather than play level ones. The fundamental notion in this dialogical perspective is therefore that of *knowing how to do* *develop a play* for some proposition *C*, rather than that of having the ability to develop a *winning play* for *C*.

This is how the problematic case of operative logic is overcome by a turn where the actions that were understood as operations within the framework of *operative logic* are now understood as *dialogical interaction*. In other words, *the dialogical approach turned monological operations into dialogical interactions* (see section XI.5).<sup>23</sup>

## Content and Interaction

Another important issue in the passage from the operative to the dialogical framework is that while the operative framework allowed quite naturally to deal with mathematical content, the dialogical framework appears to be restricted to the meaning of logical constants. This has been the subject of many criticisms, old (Hintikka, 1973, pp. 77-82), and new (Trafford, 2017, pp. 86-88); see chapter XI, in particular section XI.4. There have nonetheless been attempts to compensate this gap by introducing in the dialogical framework definitions conceived as operation rules—see (Piecha & Schröder-Heister, 2011) and (Piecha, 2012). However, these attempts have rather been received as highly programmatic.

It is actually quite fair to say that the notion of *material dialogues*—that is dialogues containing rules for expressions other than logical constants—seems to be underdeveloped in respect to *formal dialogues* (restricted mostly to logical constants) which have gathered much more attention. It is also true that a similar kind of criticism has also been raised against inferentialist approaches to meaning, and *operative logic* and dialogical logic, inspired by these inferentialist approaches, seemed to inherit this problem. However, let us stress that the fathers of dialogical logic where aware of the need of a contentual (*material* was the chosen term) basis from the beginning, and they tackled the issue with different devices. Lorenz (1970) in particular dedicated to this issue very thorough and deep studies, most of them collected in (Lorenz, 2010a; 2010b).

One of the widely acknowledged achievements of Constructive Type Theory rests in its ability to furnish the means to develop a language in which mathematical content can be introduced with the same kind of inferential rules displayed by systems of natural deduction. This virtue of CTT motivated us to explore the possibilities of enriching the language of the dialogical framework with the means of CTT. However, though chapter X deals to some extent with mathematical content and contains some brief remarks on empirical content, we shall here content ourselves with the more modest task of setting the basis for future, more thorough, developments on the issue.

## The Ancient Greek Roots of the Dialogical Turn and its Renaissance

Before turning to the links between CTT and the dialogical framework, let us point out that Lorenzen’s *dialogical turn* did not come out of the blue: Lorenzen was an

<footnote n="23"><sup>23</sup> Winning strategies in the first writings of Lorenzen and Lorenz (1978) were formulated in the form of sequent-calculus; thus the demonstration of “admissibility” amounts in this context to show that the sequence of plays determined by the local and structural rules for the logical constants yield those of the sequent calculus.</footnote>
admirer of Ernst Kapp’s (1942) perspective on the dialectical origins of logic, and had a frequent and lively interaction with the philologist Kurt von Fritz. In fact, Lorenzen had a thorough and intimate knowledge of Ancient Greek mathematics and logic, even before he gathered the chair in Kiel in 1956, where he continued these kinds of studies then in contact with Oskar Becker (who influenced Lorenzen’s appointment). In this context it might also well be that the inception of operative logic had a dialectical background that finally found its explicit expression in his *Logik und Agon* (1958).<fnref n="24" />

A striking witness of the Ancient Greek roots of the passage from the operative to the dialogical framework is *Ein formales Modell der Syllogistik des Aristoteles* (1964) by Lorenzen's student Kurt Ebbinghaus, where, after developing a remarkable proof-theoretical reconstruction of Aristotle's syllogistic in the style of *Operative Logik*, he discusses the advantages of a dialogical approach to Aristotle's notion of quantification—see (Ebbinghaus, 1964, pp. 57-58).<fnref n="25" />

In this context it is worth mentioning that nowadays history of mathematics is experiencing a revival in the studies linking the development of deductive proof in Ancient Greek mathematics with the dialogical practices of those days. Some of the most thorough studies on the subject are the ones of G. E. R. Lloyd (1996) and Reviel Netz (1999; 2005; 2009) who stress the importance of debates and oral dialogues for the emergence of classical mathematics in Ancient Greece. It seems like from the very start of mathematics the notion of proof was associated with the endeavour of explaining *why* the putative statement is true. Explaining *why* something is the case requires conceiving this explanation as directed towards a *stubborn interlocutor*, a point which does not hold only for the notion of proof in Ancient Greek mathematics—see (Fischer, 1989, p. 50).

Let us end this more historical section with the remark that the normative approach underlying the Dialogical Constructivism Program of Erlangen that emerged from the dialogical turn coupled explaining *why a putative statement is true* with the task of explaining *what the statement is good for*: according to the Erlangen-Programme the general notion of explaining is always conceived as *explaining to an audience what the purposes of an specific action (that give rise to the claim) are*—see (Lorenzen, 1969), (Kamlah & Lorenzen, 1972), (Lorenzen & Schwemmer, 1975).<fnref n="26" />

The general epistemological lesson behind Lorenzen's bold proposal of a dialogical turn might be put in the following words: the dialogical turn is an invitation to think of actions involving scientific enquiry as interaction. It took a while until the scientific community picked up Lorenzen's gauntlet, but as the most recent studies and projects in history and philosophy of logic, mathematics, foundations of computer sciences, linguistics, and epistemology point out, the time seems ripe now for the development of such a perspective.<fnref n="27" />

# I.2 Linking Dialogues and Constructive Type Theory

## I.2.1 Equality and the Socratic Rule

One of the main tenets of the present study is that a direct way to implement the Constructive Type Theoretical (CTT) approach within the dialogical framework is to focus on the CTT notion of judgemental equality.

<footnote n="24">²⁴ Kuno Lorenz conveyed this information to S. Rahman by a personal email.</footnote>

<footnote n="25">²⁵ See (Crubellier, Marion, McConaughey, & Rahman, 2018) and (Rahman & Lion, 2018).</footnote>

<footnote n="26">²⁶ For a brief presentation of the philosophical tenets of Dialogical Constructivism see section XI.7.</footnote>

<footnote n="27">²⁷ See, among others, (Fischer, 1989), (Sellars, 1991), (Brandom, 1997), (Girard, 1999), (Heinzmann, 2006), (Ginzburg, 2012), (Lecomte, 2011), (Lecomte & Quatrini, 2010), (Paseau, 2011), (Peregrin, 2014), Duthil Novaes (2015).</footnote>
In CTT, every category needs to be associated with a criterion of identity (see chapter II, written by Ansten Klev). More precisely, there are two basic forms of categorical judgement in CTT:

i) $a : C$

ii) $a = b : C$

The first is read “a is an object of the category C”, and the second, the judgemental or definitional equality, is read “a and b are identical objects of the category C”. We thus require that any category C occurring in a judgement of CTT be associated with a

* criterion of application, which tells us what a C is; the fact that a meets this criterion is precisely what is expressed in $a : C$; and a

* criterion of identity, which tells us what it is for a and b to be identical C's; the fact that a and b together meet this criterion is precisely what is expressed in $a = b : C$.

In the dialogical framework, on the other hand, equality involves plays in which players explicitly expose in the object-language<sup>28</sup> the reasons they have for stating judgements. More precisely, as mentioned in the preface, definitional equality is implemented at the play level by means of the Socratic rule.

The Socratic rule is one of the most salient characteristics of dialogical logic. As discussed by (Marion & Rückert, 2015), it can be traced back to Aristotle's reconstruction of the Platonic dialectics. A purely argumentative point of view can be defined within dialectics as refraining from calling on some authority beyond what has actually been brought forward during the current argumentative interaction (following the suitable rules determined by the game). Thus, when an elementary statement is challenged, the challenge can be answered only by invoking the challenger's own concessions (or his own constructions). In such a context, the Socratic rule can be understood in the following way, when a player plays an elementary statement:<sup>29</sup>

> "My reasons for stating this proposition you are now challenging are exactly the same as the ones you brought forward when you yourself stated that very same proposition."

In this fashion the Socratic rule provides for equality, but through interaction: equality is built within an argumentative play by copying exactly the same reasons for a proposition as what the other player has already provided. Statements of definitional equality have thus emerged in a dialogical perspective, in particular reflexivity statements such as

$p = p : A$

which express the fact that if the Opponent states the elementary proposition A, then the Proponent 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.

In order to introduce in the object-language of the dialogical framework (dialogues for immanent reasoning) definitional identities at the play level, we must extend the language of a dialogical game with statements of the form

$p : A$

where on the right-hand side of the colon is the proposition A, and on the left-hand side is the *local reason* brought forward to back the proposition *during a play* (see chapter VI). The local reason is therefore *local* if the force of the statement is limited to the level of plays. But when the assertion $p : A$ is backed by a *winning strategy*, the

<footnote n="28"><sup>28</sup> This is the main feature of dialogues for immanent reasoning, the dialogical framework which incorporates features of CTT. For a presentation of this framework, see chapters VI-VII. The Socratic rule is the equivalent in immanent reasoning of the Copy-Cat rule in the standard dialogical framework. For a presentation of the standard framework, see chapters III-V.</footnote>

<footnote n="29"><sup>29</sup> See (Rahman, Clerbout, & Keiff, 2009) and (Rahman & Keiff, 2010).</footnote>
judgement asserted draws its justification precisely from that strategy, thus endowing *p* with the status of a *strategic reason* (see section VII.7).

Thus *reasons* backing a statement are manifest at the object-language level, and are internal to the development of a play, which is why we have named this dialogical framework incorporating CTT features making these reasons explicit, *dialogues for immanent reasoning*.

The notion of *reason* (local and strategic) shows how we link the dialogical framework to CTT, but also how we can preserve the flexibility of the dialogical framework and bring out its full potential, ranging from material dialogues (at the play level) to the equivalent of the CTT demonstrations (at the strategy level) and all that which comes in-between. Immanent reasoning and equality in action are in this sense not exclusively at one level, but are embedded in the whole framework through the constitutive role of the Socratic rule.

### 1.2.2 Local Reasons and Content: The Socratic Rule within *Material Dialogues*

Local reasons are fundamental to dialogues for immanent reasoning as they also contribute to *material dialogues* for elementary propositions (see chapter X). Informally, the idea is that if the Proponent is entitled to his statement on the elementary proposition *A*, it is because he is ready to defend *A* by giving a *reason* in favor of that statement. The Proponent can find such a local reason backing *A* in a process governed by the Socratic rule which spells out the precise forms of the local reason required by the *content* of *A*. The appropriate local reason will thus be governed by the Socratic rule (which ensures, by preventing the Proponent to provide his own grounds for what he says, that the grounds for stating an elementary proposition are taken from the play itself, that is, it ensures the reasons are immanent to the play), but this rule will have to be adapted to each individual content brought forward, bringing us to *material dialogues*, and should be contrasted with the development of *formal dialogues* in which the Socratic rule allows the Proponent to replicate an elementary proposition *A* stated by the Opponent, but also to replicate the local reasons that the Opponent brought forward when stating *A*, and this independently of checking what these local reasons are: in purely formal dialogues, if the Opponent states for instance that 2 is odd, the Proponent can state this too on the sole grounds that the Opponent herself stated it and provided some reason for it, whatever this reason be.

But in material dialogues, if the Proponent asserts for example: "1 is an uneven number," the Opponent would be entitled to request of the Proponent a natural number *n* such that $1 = 2 \cdot n + 1$. The local reason in this case would be $1 = 2 \cdot 0 + 1$, which is a reason specific to that particular statement the Opponent challenged.

In these dialogues, the Socratic rule determines the canonical elements and the definitions (the definitional equalities) specific to each of the elementary expressions in a play. This yields *material truth*.

Stating the *material truth* of a proposition requires exhibiting a local reason specific to the content of that proposition.

The origins of the normative approach to meaning can be found in this aspect of the dialogical framework: *meaning as use* should be understood as *the use is spelled out by a rule of dialogical interaction* which applies to the meaning of the logical constants, but also to the meaning of the elementary propositions. Strictly speaking, the meaning of each elementary expression requires a specific rule that determines its proper content and distinguishes it from other elementary propositions.<fnref n="30" /> Material dialogues in this

<footnote n="30">³⁰ Jaroslav Peregrin (2014, pp. 3-5) calls the notion of *use* understood as *following a rule* "role". *Role* distinguish linguistic uses from other uses such as using a hammer.</footnote>
perspective are not only a matter of putting back normativity in logic, they also deal with
the important matter of elaborating a contentful language.

### I.2.3 Dialogues for Immanent Reasoning as *Games of Why and How*

The present study aims at showing that, if we follow Lorenzen's and Lorenz's advice of looking at mathematical operations as interaction, then definitional equality can be considered as exposing the dialogical intertwining of *entitlements* and *duties*. In this perspective, the standard monological presentation of these rules for both definitional and predicative equality implicitly encodes an underlying process, a process in which the Proponent "copies" some of the Opponent's choices, thus providing its dialogical and normative roots.

We shall in this fashion rally to some extent to Robert Brandom’s insight<fnref n="31" /> that conceptual meaning is entirely constituted by the way judgements are inserted into *games of giving and asking for reasons*, the touchstone of inferential pragmatism. Our task now lies in describing, in the context of these *games of giving and asking for reasons*, the moves on the ontological level grounding statements of equality (definitional equality), and on the propositional level grounding statements of identity (the dyadic-predicate of standard first-order logic). This is necessary in order to have games of *Why* and *How*.<fnref n="32" />

The emergence of concepts, 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 it is that the reason brought forward accomplishes the explicative task*. Immanent reasoning are dialogical games of *Why* and *How*.

We call our dialogues involving rational argumentation *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 itself.

## I.3 A Basic Overview of the Book

One of the important lessons of the Constructive Type Theory approach to meaning is that equality is at the center of a constructivist project of types. Indeed, it has been stressed that the constructivist parallel to Quine's (1969, p. 23) notorious "*no entity without identity*" is

* No entity without a type

* No type without a criterion of identity

<footnote n="31">³¹ See for instance (Brandom, 1994). To some extent only, for it seems like Brandom starts from the strategy level rather than from the play level as we do.</footnote>

<footnote n="32">³² As discussed in section X.5, Brandom’s approach only has the propositional level (i.e. his framework does not include the ontological level of the *local reasons* relevant for the backing of the proposition involved in the judgement), perhaps because he fears that such a move would amount to incorporating into the framework an *authority* which would be *external* to the games that determine concepts. As far as we understand it, this is a serious limitation of Brandom’s approach since it fails to distinguish between the notations, or written forms, concerning the ontological level, and those concerning the propositional level: the present book, we hope, shows how to make the ontological level immanent to the dialogical process of reasoning. This suggests that the dialogical approach to CTT offers a way to integrate within one epistemological framework the two conflicting readings of Willfried Sellars’ (1991, pp. 129-194) notion of *space of reasons* brought forward by John McDowell (2009, pp. 221-238) on the one side, who insists in distinguishing world-direct thought and knowledge gathered by inference, and by Robert Brandom (1997) on the other side, 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 the piece of evidence justifying a proposition, but it is also that the dialogical framework allows distinguishing between the objective justification (strategy) level targeted by Brandom (1997, p. 129) and the subjective (play) level stressed by McDowell—see also (Rahman, 2017).</footnote>
Definitional equality is central to the constitution of a type. Moreover, in the context of logic, definitional equality makes the coordination of analytic and synthetic steps explicit. So, if we are looking at ways of linking the normativity of dialogical logic with the normativity of CTT, it becomes apparent that we should try to provide an answer to the question of how the criterion of identity of a type is manifested in the dialogical framework—this is what the book is about.

The purpose of the book is therefore rather technical, though it has deep
philosophical roots in what argumentation and reasoning are. Perhaps one way to
condense our philosophical perspective on identity is that it has been developed in the
general epistemological framework according to which

argumentation is, all in all, nothing more—but nothing less—than a
collaborative enquiry into the ways of constructing the symmetries
grounding rationality within inquisitive interaction.<fnref n="33" /> By building these
symmetries we provide meaning to our actions, a meaning deployed in our
actions' internal coordination with the actions of others (interaction).

In order to allow readers to follow the technical aspects of this book, we have
divided it into progressive sections, with examples and exercises.

The next section (chapter II) provides an elementary introduction to Constructive
Type Theory (CTT), original in its equal emphasis on basic ideas and finer technical
details.

The third chapter introduces essential notions for the dialogical framework and provides a basic and step by step approach to dialogues.

The fourth and fifth chapters aim at more advanced readers, who are either already familiar with the dialogical framework or well versed into logic; they respectively deal with the two fundamental levels characteristic of dialogues: the play level and the strategy level.

The reader should by then be fully equiped for the following sections, which are
the core of this book and deal precisely with the problem at issue, that is, with immanent
reasoning and equality in action. Thus the sixth chapter introduces local reasons in the
dialogical framework, a crucial step for immanent reasoning; the seventh chapter
presents again the local reasons but from a more technical side, deals with the strategy
level in dialogues for immanent reasoning, and introduces a key notion: strategic objects,
the dialogical counterpart to CTT proof-objects.

The eighth chapter illustrates some of the imports of the constructive perspective
in general and of dialogues for immanent reasoing in particular through the case of the
Axiom of Choice.

The ninth chapter provides an algorithm allowing to go from dialogical strategies to CTT demonstrations, and reversewise.

The tenth chapter touches on the less studied material dialogues, that is, dialogues
with rules for local and global meaning that are not restricted to the rules of logical
constants. We study the case of propositional identity, the set **Bool**, Boolean operations,
and finite sets.

The final chapter will be our conclusion, which contains some philosophical
remarks on dialogical constructivism and suggests some responses to standard objections
to the dialogical framework.

<footnote n="33"><sup>33</sup> For more details on symmetry in the dialogical framework, see section IV.3.</footnote>
# II. A BRIEF INTRODUCTION TO CONSTRUCTIVE TYPE THEORY

By Ansten Klev

Martin-Löf's Constructive Type Theory (CTT) is a formal language developed in order to reason constructively about mathematics. It is thus a formal language conceived primarily as a tool to reason with rather than a formal language conceived primarily as a mathematical system to reason about. Constructive Type Theory is therefore much closer in spirit to Frege's ideography and to the language of Russell and Whitehead's *Principia Mathematica* than to the majority of logical systems ("logics") studied by contemporary logicians. Since CTT is designed as a language to reason with, much attention is paid to the explanation of basic concepts. This is perhaps the main reason why the style of presentation of CTT differs somewhat from the style of presentation typically found in, for instance, ordinary logic textbooks. For those new to the system it might be useful to approach an introduction, such as the one given below, more as a language course than as a course in mathematics.

## II.1 Judgements and categories

Statements made in Constructive Type Theory are called judgements. Judgement is thus a technical term, chosen because of its long pedigree in the history logic. (cf. e.g. (Martin-Löf, 1996; 2011) and (Sundholm, 2009)). Judgement thus understood is a logical notion and not, as it is commonly understood in contemporary philosophy, a psychological notion. As in traditional logic, a judgement may be categorical or hypothetical. Categorical judgements are conceptually prior to hypothetical judgements, hence we must begin by explaining them.

### II.1.1 Forms of categorical judgement

There are two basic forms of categorical judgement in CTT:

$$a : C$$

$$a = b : C$$

The first is read “a is an object of the category $C$” and the second is read “a and b are identical objects of the category $C$”. Ordinary grammatical analysis of $a : C$ yields a as subject, $C$ as predicate, and the colon as copula. We thus call the predicate $C$ in $a : C$ a category. This use of the term ‘category’ is in accordance with one of the original meanings of the Greek *katēgoria*, namely as predicate. It is also in accordance with a common use of the term ‘category’ in current philosophy.<fnref n="34" /> We require, namely, that any category $C$ occurring in a judgement of CTT be associated with

* a *criterion of application*, which tells us what a $C$ is; that $a$ meets this criterion is precisely what is expressed in $a : C$;

* a *criterion of identity*, which tells us what it is for $a$ and $b$ to be identical $C$s; that $a$ and $b$ together meet this criterion is precisely what is expressed in $a = b : C$.

What the categories of CTT are will be explained below.

In CTT any object belongs to a category. The theory recognizes something as an object only if it can appear in a judgement of the form $a : C$ or $a = b : C$. Since

<footnote n="34">³⁴ See, in particular, the definition of category given by Dummett (1973, pp. 75-76), which has been taken over by Hale and Wright (2001) for instance.</footnote>
associated with any category there is a criterion of identity, we can recover Quine's
(1969, p. 23) precept of "no entity without identity" as

no object without category +
no category without a criterion of identity.

Thus we derive Quine’s precept from two of the fundamental principles of CTT.
We shall have more to say later about the treatment of identity in CTT.

Neither semantically nor syntactically does *a* : *C* agree with the basic form of
statement in predicate logic:

$F(a)$

In *F(a)* a function *F* is applied to an argument *a* (in general there may be more
than one argument). The judgement *a* : *C*, by contrast, does not have function-argument
form. In fact, the ‘*a* : *C*’-form of judgement is closer to the ‘*S* is *P*’-form of traditional
sylogistic logic than to the function-argument form of modern, Fregean logic. Since we
have required that the predicate *C* be associated with criteria of application and identity,
the judgement *a* : *C* can only be compared with a special case of the ‘*S* is *P*’-form, for
no such requirement is in general laid on the predicate *P* in a judgement of Aristotle’s
sylogistics—it can be any general term.

To understand the restriction that *P* be associated with criteria of application and identity, in terms of traditional logic, we may invoke Aristotle's doctrine of predicables from the *Topics*.<fnref n="35" /> A predicable may be thought of as a certain relation between the *S* and the *P* in an ‘*S* is *P*’-judgement. Aristotle distinguishes four predicables: genus, definition, *idion* or *proprium*, and accident. That *P* is a genus of *S* means that *P* reveals a *what*, or a *what-it-is*, of the subject *S*; a genus of *S* may thus be proposed in answer to the question of what *S* is. The class of judgements of Aristotelian syllogistics to which judgements of the form *a* : *C* may be compared is the class of judgements whose predicate is a genus of the subject. Provided the judgement *a* : *C* is correct, the category *C* is namely an answer to the question of what *a* is; we may thus think of *C* as the genus of *a*. Aristotle's other predicables will not concern us here.

Being a natural number is in a clear sense a *what* of 7. The number 7 is also a
prime number; but being prime is not a *what* of 7 in the sense that being a natural
number is, even though 7 is necessarily, and perhaps even essentially, a prime number.
Following Almog (1991) we may say that being prime is one of the *hows* of 7. This
difference between the *what* and the *how* of a thing captures quite well the difference in
semantics between a judgement *a* : *C* of CTT and a sentence *F(a)* of predicate logic. In
the predicate-logical language of arithmetic we do not express the fact that 7 is a number
by means of a sentence of the form *F(a)*. That the individual terms of the language of
arithmetic denote numbers is rather a feature of the interpretation of the language that we
may express in the metalanguage.<fnref n="36" /> We do, however, say in the language of arithmetic
that 7 is prime by means of a sentence of the form *F(a)*, for instance as **Pr(7)**. It is
therefore natural to suggest that by means of the form of statement *F(a)* we express a
*how*, but not the *what*, of the object *a*. The opposite holds for the form of statement *a* :
*C*—by means of this we express the *what*, but not the *how*, of the object *a*. Thus, in CTT
we do say that 7 is a number by means of a judgement, namely as 7 : N, where N is the
category of natural numbers; but we do not say that 7 is prime by means of a similar
judgement such as 7 : **Pr**. Precisely how we express in CTT that 7 is prime will become

<footnote n="35">³⁵ (Barnes, 1984), (Crubellier, 2008).</footnote>

<footnote n="36">³⁶ Compare Carnap’s treatment of what he calls *Allwörter* (‘universal words’ in the English translation) in §§ 76, 77 of *Logische Syntax der Sprache*, (Carnap, 1934).</footnote>
clear only later; it will then be seen that we express the primeness of 7 by a judgement of the form

$$p : \mathbf{Pr}(7)$$

where $\mathbf{Pr}(7)$ is a proposition and $p$ is a proof of this proposition. The proposition $\mathbf{Pr}(7)$ has function-argument form, just as the atomic sentences of ordinary predicate logic.

## II.1.2 Categories

The forms of judgement $a : C$ and $a = b : C$ are only schematic forms. The specific forms of categorical judgement employed in CTT are obtained from these schematic forms by specifying the categories of the theory. There is then a choice to be made, namely between what may be called a higher-order and a lower-order presentation of the theory. The higher-order presentation results in a somewhat conceptually cleaner theory, but the lower-order presentation is preferable for pedagogical purposes, both because it requires less machinery and because it is the style of presentation found in the standard references of Martin-Löf (1975b; 1982; 1984) and Nordström et al. (1990, pp. ch. 4-16). We shall therefore follow this style of presentation. The categories are then the following. There is a category **set** of sets in the sense of Martin-Löf; and for any **set** $A$, $A$ itself is a category. We therefore have the following four forms of categorical judgement:

$$A : \mathbf{set} \\ A = B : \mathbf{set}$$

and for any **set** $A$,

$$a : A \\ a = b : A$$

In the higher-order presentation the categories are **type** and $\alpha$, for any **type** $\alpha$. The higher-order presentation in a sense subsumes the lower-order presentation, since we have there, firstly, as an axiom **set** : **type**, hence **set** itself is a category; and secondly, there is a rule to the effect that if $A : \mathbf{set}$, then $A : \mathbf{type}$, hence also any **set** $A$ will be a category. The higher-order presentation can be found in Nordström et al. (1990, pp. ch. 19-20; 2000).

We have so far only given names to our categories. To justify calling **set** as well as any **set** $A$ a category we must specify the criteria of application and identity of **set** and of $A$, for any **set** $A$. Thus we have to explain four things: what a **set** is, what identical **sets** are, what an element of a **set** $A$ is, and what identical elements of a **set** $A$ are. By giving these explanations we also explain the four forms of categorical judgement $A : \mathbf{set}$, $A = B : \mathbf{set}$, $a : A$, and $a = b : A$. Our explanations follow those given by Martin-Löf (1984, pp. 7-10).

We explain the form of judgement $A : \mathbf{set}$ as follows. A **set** $A$ is defined by saying what a *canonical* element of $A$ is and what equal canonical elements of $A$ are. (Instead of 'canonical element' one can also say 'element of canonical form'.) What the canonical elements are, as well as what equal canonical elements are, of a **set** $A$ is determined by the so-called introduction rules associated with $A$. For instance, the introduction rules associated with the set of natural numbers $\mathbb{N}$ are as follows.

$$0 : \mathbb{N} \quad 0 = 0 : \mathbb{N} \quad \frac{n : \mathbb{N}}{\mathbf{s}(n) : \mathbb{N}} \quad \frac{n = m : \mathbb{N}}{\mathbf{s}(n) = \mathbf{s}(m) : \mathbb{N}}$$

By virtue of these rules $0$ is a canonical element of $\mathbb{N}$, as is $\mathbf{s}(n)$ provided $n$ is a $\mathbb{N}$, which does not have to be canonical. Moreover, $0$ is the same canonical element of $\mathbb{N}$ as
0, and $s(n)$ is the same canonical element of $\mathbb{N}$ as $s(m)$ provided $n = m : \mathbb{N}$. It is required that the specification of what equal canonical elements of a set $A$ are renders this relation reflexive, symmetric, and transitive.

The form of judgement $A = B : \mathbf{set}$ means that from $a$'s being a canonical element of $A$ we may infer that $a$ is also a canonical element of $B$, and vice versa; and that from $a$ and $b$'s being identical canonical elements of $A$ we may infer that they are also identical canonical elements of $B$, and vice versa.

Thus we have given the criteria of application and identity for the category **set**.

Suppose that $A$ is a **set**. Then we know how the canonical elements of $A$ are formed as well as how equal canonical elements of $A$ are formed. The judgement $a : A$ means that $a$ is a programme which, when executed, evaluates to a canonical element of $A$. For instance, once one has introduced the addition function, $+$, and the definitions $1 = s(0) : \mathbb{N}$ and $2 = s(1) : \mathbb{N}$, one can see that $2 + 2$ is an element of $\mathbb{N}$, since it evaluates to $s(2 + 1)$, which is of canonical form. A canonical element of a **set** $A$ evaluates to itself; hence, any canonical element of $A$ is an element of $A$.

The judgement $a = b : A$ presupposes the judgements $a : A$ and $b : A$. Hence, if we can make the judgement $a = b : A$, then we know that both $a$ and $b$ evaluate to canonical objects of $A$. The judgement $a = b : A$ means that $a$ and $b$ evaluate to equal canonical elements of $A$. The value of a canonical element $a$ of a **set** $A$ is taken be $a$ itself. Hence, if $b$ evaluates to $a$, then we have $a = b : A$.

Thus we have given the criteria of application and identity for the category $A$, for any **set** $A$.

A note on terminology is here in order. ‘Set’ is the term used by Martin-Löf from (Martin-Löf, 1984) onwards for what in earlier writings of his were called types.<fnref n="37" /> A set in the sense of Martin-Löf is a very different thing from a set in the sense of ordinary axiomatic set theory. In the latter sense a set is typically conceived of as an object belonging to the cumulative hierarchy $V$. It is, however, this hierarchy $V$ itself rather than any individual object belonging to $V$ that should be regarded as a set in the sense of Martin-Löf. A set in the sense of Martin-Löf is in effect a domain of individuals, and $V$ is precisely a domain of individuals. That was certainly the idea of Zermelo in his paper on models of set theory (Zermelo, 1930): he there speaks of such models as *Mengenbereiche*, domains of sets. And Aczel (1978) has defined a set in the sense of Martin-Löf that is “a type theoretic reformulation of the classical conception of the cumulative hierarchy of types” (Aczel, 1978, p. 61). It is in order to mark this difference in conception that we denote a set in the sense of Martin-Löf with boldface type, thus writing ‘set’.<fnref n="38" />

### II.1.3 General rules of judgemental equality

Recall that when defining a **set** $A$, it is required that the relation of being equal canonical elements then specified be reflexive, symmetric, and transitive. From the explanation of the form of judgement $a = b : A$, it is then easy to see that the relation of the so-called judgemental identity, namely the relation expressed to hold between $a$ and $b$ by means of the judgement $a = b : A$, is also reflexive, symmetric, and transitive. Thus the following three rules are justified.

$$ \frac{a : A}{a = b : A} \qquad \frac{a = b : A}{b = c : A} $$

<footnote n="37">³⁷ This older terminology is retained for instance in *Homotopy Type Theory* (The Univalent Foundations Program, 2013); what is there called a set (The Univalent Foundations Program, 2013, p. Definition 3.1.1) is only a special case of a set in Martin-Löf's sense, namely a set over which every identity proposition has at most one proof.</footnote>

<footnote n="38">³⁸ For a further discussion of the difference between Martin-Löf's notion and other notions of set, see (Granström, 2011, pp. 53-63) and (Klev, 2014a, pp. 138-140).</footnote>
$$ \begin{array}{c} \mathcal{D}_1 \\ A \\ \hline A \wedge B \end{array} \quad \begin{array}{c} \mathcal{D}_2 \\ B \\ \hline \end{array} $$

where $\mathcal{D}_1$ is a proof of $A$ and $\mathcal{D}_2$ a proof of $B$. An example of a non-canonical proof is therefore

$$ \begin{array}{c} \mathcal{D}_1 \\ C \supset A \wedge B \\ \hline A \wedge B \end{array} \quad \begin{array}{c} \mathcal{D}_2 \\ C \\ \hline \end{array} $$

where $\mathcal{D}_1$ is a proof of $C \supset A \wedge B$ and $\mathcal{D}_2$ a proof of $C$.

The proofs occurring in the above illustration are in tree form. Proofs in the technical sense of CTT are not given in tree form, but rather as the subjects $a$ of judgements of the form $a : A$, where $A$ is a **prop**. Proofs in this sense are in effect terms in a certain rich typed lambda-calculus and they are often called *proof-objects* (this term was introduced by (Diller & Troelstra, 1984)).

We may introduce a new form of judgement ‘*A true*’ governed by the following rule of inference

$$ \begin{array}{c} a : A \\ A \text{ true} \end{array} $$

Thus, provided we have found a proof $a$ of $A$, we may infer $A$ true. The conclusion $A$ true can be seen as suppressing the proof $a$ of $A$ displayed in $a : A$.

### II.1.5 Forms of hypothetical judgement

One of the characteristic features of Constructive Type Theory is that it recognizes hypothetical judgements as a form of statement distinct from the assertion of the truth of an implicational proposition $A \supset B$. In fact, hypothetical judgements are fundamental to the theory. It is, for instance, hypothetical judgements that give rise to the various dependency structures in CTT, by virtue of which it is a dependent type theory.

Assume $A : \mathbf{set}$. Then we have the following four forms of hypothetical judgement with one assumption.

$$ x : A \vdash B : \mathbf{set} $$

$$ x : A \vdash B = C : \mathbf{set} $$

$$ x : A \vdash b : B $$

$$ x : A \vdash b = c : B $$

We have used the turnstile symbol, $\vdash$, to separate the antecedent, or assumption, of the judgement from the consequent. In (Martin-Löf, 1984) the notation used is

$$ B : \mathbf{set} (x : A) $$

for what we here write $x : A \vdash B : \mathbf{set}$. We read this judgement as “$B$ is a set under the assumption $x : A$”. Similar remarks apply to the other three forms of hypothetical judgement. Let us consider the more precise meaning explanations of these forms of judgement.

A judgement of the form $x : A \vdash B : \mathbf{set}$ means that
$B[a/x] : \mathbf{set}$ whenever $a : A$, and
$$B[a/x] = B[a'/x] : \mathbf{set} \text{ whenever } a = a' : A.$$

Here 'B[a/x]' signifies the result of substituting 'a' for 'x' in 'B'. Thus we may think of B as a function from A into set; or using a different terminology, B may be thought of as a family of sets over A. We are assuming that x is the only free variable in B and that A contains no free variables, hence that the judgement A : set holds categorically, that is, under no assumptions. It follows that B[a/x] is a closed term, hence that B[a/x] : set holds categorically; by the explanation given of the form of categorical judgement A : set we therefore know the meaning of B[a/x] : set. Thus we see that the meaning of a hypothetical judgement is explained in terms of the meaning of categorical judgements. It holds in general that the meaning explanation of hypothetical judgements is thus reduced to the meaning explanation of categorical judgements.

The explanation of the form of judgement $x : A \vdash B : \mathbf{set}$ justifies the following two rules.

$$\frac{a : A \qquad x : A \vdash B : \mathbf{set}}{B[a/x] : \mathbf{set}} \qquad \frac{a = a' : A \qquad x : A \vdash B : \mathbf{set}}{B[a/x] = B[a'/x] : \mathbf{set}}$$

Note that by the second rule here, substitution into sets is extensional with respect to judgemental identity. That is to say, if we think of $x : A \vdash B : \mathbf{set}$ as expressing that B is a set-valued function (a family of sets), then B has the expected property that for identical arguments $a = a' : A$ we get identical values $B[a/x] = B[a'/x] : \mathbf{set}$.

We note that the notion of substitution is here understood only informally and that the notation $B[a/x]$ belongs to the metalanguage. The notion of substitution can be made precise, and a notation for substitution introduced into the language of CTT itself; but it would take us too far afield to get into the details of that (cf. (Martin-Löf, 1992) and (Tasistro, 1993)).

A judgement of the form $x : A \vdash B = C : \mathbf{set}$ means that

$$B[a/x] = C[a/x] : \mathbf{set} \text{ whenever } a : A.$$

Hence, in this case we may think of B and C as identical families of sets over A. The explanation justifies the following rule.

$$\frac{a : A \qquad x : A \vdash B = C : \mathbf{set}}{B[a/x] = C[a/x] : \mathbf{set}}$$

A judgement of the form $x : A \vdash b : B$ means that

$b[a/x] : B[a/x]$ whenever $a : A$, and
$$b[a/x] = b[a'/x] : B[a/x] \text{ whenever } a = a' : A.$$

Here we are presupposing $x : A \vdash B : \mathbf{set}$, hence we know that $B[a/x] : \mathbf{set}$ whenever $a : A$, and therefore we also know the meaning of $b[a/x] : B[a/x]$ and $b[a/x] = b[a'/x] : B[a/x]$ whenever $a : A$ and $a = a' : A$. The judgement $x : A \vdash b : B$ can be understood as saying that $b$ is a function from $A$ into the family $B$; that is to say, $b$ is a function that for any $a : A$ yields an element $b[a/x]$ of the set $B[a/x]$. The explanation justifies the following two rules.

$$\frac{a : A \qquad x : A \vdash b : B}{b[a/x] : B[a/x]} \qquad \frac{a = a' : A \qquad x : A \vdash b : B}{b[a/x] = b[a'/x] : B[a/x]}$$
Note that by the second rule here, substitution into elements of sets is extensional with respect to judgemental identity. That is to say, if we think of $x: A \vdash b: B$ as expressing that $b$ is a function, then $b$ has the expected property that for identical arguments $a = a' : A$ we get identical values $b[a/x] = b[a'/x] : B[a/x]$.

A judgement of the form $x: A \vdash b: c: B$ means that

$$b[a/x] = c[a/x] : B[a/x] \text{ whenever } a: A.$$

Thus, in this case, $b$ and $c$ are identical functions into the family $B$. The explanation justifies the following rule.

$$\frac{a: A \qquad x: A \vdash b = c: B}{b[a/x] = c[a/x] : B[a/x]}$$

## II.1.6 Assumptions and other speech acts

The notions of proposition, categorical judgement, and hypothetical judgement can be seen all of them to be presupposed by what is arguably the most natural interpretation of natural deduction derivations (Sundholm, 2006). Consider the following natural deduction proof sketch:

$$\frac{
  \begin{array}{c}
    A \\
    \mathcal{D}_1 \\
    \hline
    B \\
    A \supset B
  \end{array}
}{
  \begin{array}{c}
    \mathcal{D}_2 \\
    \hline
    A
  \end{array}
}
\qquad B$$

Here $\mathcal{D}_1$ is a proof of $B$ from $A$, and $\mathcal{D}_2$ is a closed proof of $A$. Let us regard this natural deduction proof sketch as a representation of an actual mathematical demonstration and let us consider which speech acts the individual formulae here then represent.

* The topmost $A$ represents an assumption, namely the assumption that the proposition $A$ is true.

* The formula $A$ that is the conclusion of $\mathcal{D}_2$ is the conclusion of a closed proof; this formula therefore represents the categorical judgement, or assertion, that $A$ is true; the same considerations apply to $A \supset B$ and to the final conclusion $B$.

* The $B$ that is the conclusion of $\mathcal{D}_1$ represents neither an assumption nor a categorical assertion; it rather represents a hypothetical judgement, namely the judgement that $B$ is true on the hypothesis that $A$ is true.

* The formula $A$ occurring as a subformula in $A \supset B$ represents neither an assumption nor a categorical assumption nor a hypothetical judgement. It rather represents a proposition that is a part of a more complex proposition $A \supset B$, which in the given proof is asserted categorically to be true.

Thus we see that in order to make the semantics of natural deduction derivations explicit we should employ a notation that is able to distinguish not only propositions from judgements, but also categorical judgements from hypothetical judgements, and perhaps also assumptions from all of these. Assumptions can, however, be subsumed under hypothetical judgements, since we may regard the assumption of some categorical judgement $J$ as the assertion of $J$ on the hypothesis that $J$. In particular, the assumption of $a: A$ and the assumption that the proposition $A$ is true may be analyzed as respectively:
$a : A \vdash a : A$ and $A \text{ true} \vdash A \text{ true}$

In CTT one can therefore make the semantics of the above natural deduction proof sketch explicit as follows

$$ \begin{array}{ccc} & A \text{ true} \vdash A \text{ true} & \\ & \mathcal{D}_1 & \\ \frac{A \text{ true} \vdash B \text{ true}}{A \supset B \text{ true}} & \mathcal{D}_2 & \\ \cline{2-3} & B \text{ true} & \end{array} $$

From the meaning explanation of hypothetical judgements it is clear that the following rule is justified.

$$ \frac{A : \mathbf{set}}{x : A \vdash x : A} $$

Nordström et al. (1990, p. 37) call this the rule of assumption, since it in effect allows us to introduce assumptions.

### II.1.7 Hypothetical judgements with more than one assumption

The forms of hypothetical judgement where the number of hypotheses is $n > 1$ are explained by induction on $n$. We consider the case of $n = 2$ for illustration. We assume that $A_1 : \mathbf{set}$ and $x : A_1 \vdash A_2 : \mathbf{set}$. Thus $A_1$ is a set categorically, while $A_2$ is a family of sets over $A_1$. The four forms of judgement to be considered are the following.

$$ \begin{array}{l} x : A_1, x_2 : A_2 \vdash B : \mathbf{set} \\ x : A_1, x_2 : A_2 \vdash B = C : \mathbf{set} \\ x : A_1, x_2 : A_2 \vdash b : B \\ x : A_1, x_2 : A_2 \vdash b = c : B \end{array} $$

The first of these judgements means that $B[a_1/x_1, a_2/x_2] : \mathbf{set}$ whenever $a_1 : A_1$ and $a_2 : A_2[a_1/x_1]$ and that $B[a_1/x_1, a_2/x_2] = B[a'_1/x_1, a'_2/x_2] : \mathbf{set}$ whenever $a_1 = a'_1 : A_1$ and $a_2 = a'_2 : A_2[a_1/x_1]$. Note that $A_2$ here in general may be a family of sets over $A_1$. Which member of the family the second argument $a_2$ is taken from depends on the first argument $a_1$. Thus $B$ is a family of sets over $A_1$ and $A_2$, where $A_2$ itself may be a family of sets over $A_1$.

The meaning of the third judgement is that $b[a_1/x_1, a_2/x_2] : B[a_1/x_1, a_2/x_2]$ whenever $a_1 : A_1$ and $a_2 : A_2[a_1/x_1]$, and that $b[a_1/x_1, a_2/x_2] = b[a'_1/x_1, a'_2/x_2] : B[a_1/x_1, a_2/x_2]$ whenever $a_1 = a'_1 : A_1$ and $a_2 = a'_2 : A_2[a_1/x_1]$. Thus $b$ is a binary function whose first argument is an element of $A_1$; if this element is $a_1$, then the second argument is an element of $A_2[a_1/x_1]$; if the second argument is $a_2$, then the value $b[a_1/x_1, a_2/x_2]$ is an element of $B[a_1/x_1, a_2/x_2]$. Here one sees the complex dependency structures that can be expressed in CTT.

It should be clear how the explanation of the second and fourth forms of judgement above, as well as the explanation for arbitrary $n$, should go.

Let $J$ be any categorical judgement, that is, a judgement of one of the forms $B : \mathbf{set}, B = C : \mathbf{set}, b : B, b = b' : B$. In a hypothetical judgement

$$ x_1 : A_1, \dots, x_n : A_n \vdash J $$
we call the sequence of hypotheses $x_1 : A_1, ..., x_n : A_n$ a context. A judgement of the form

$$x_1 : A_1, ..., x_n : A_n \vdash B : \mathbf{set}$$

may thus be expressed by saying that $B$ is a **set** in the context $x_1 : A_1, ..., x_n : A_n$. Let $\Gamma$ be a context. From the meaning explanation of hypothetical judgements one sees that rules of the following kind are justified.

$$\frac{\Gamma \vdash J \qquad \Gamma \vdash B : \mathbf{set} \\ \Gamma, y : B \vdash J}{\Gamma, y : B \vdash J}$$

These rules may be called *rules of weakening*, in accordance with the terminology used in sequent calculus.

With the general hypothetical form of judgement explained we may introduce a notion of category in a wider sense, in effect what is called a category in (Martin-Löf, 1984, p. 21-23). Let us write the four general forms of judgement in the style of Martin-Löf, namely as follows.

$$\begin{array}{l} B : \mathbf{set} (x_1 : A_1, ..., x_n : A_n) \\ B = C : \mathbf{set} (x_1 : A_1, ..., x_n : A_n) \\ b : B (x_1 : A_1, ..., x_n : A_n) \\ b = c : B (x_1 : A_1, ..., x_n : A_n) \end{array}$$

In a grammatical analysis of the first of these it is natural to view not only **set** but everything that is to the right of the colon, namely

$$\mathbf{set} (x_1 : A_1, ..., x_n : A_n)$$

as the predicate. The relation between the notions of predicate and category thus suggests that we may regard this as a category. Indeed, this may be regarded as the category of families of **sets** in $n$ variables ranging over the **sets** or families of **sets** $A_1, ..., A_n$, among which there may be dependency relations as explained for the case of $n = 2$ above. Likewise we may regard

$$B (x_1 : A_1, ..., x_n : A_n)$$

as a category. It is the category of $n$-ary functions from $A_1, ..., A_n$ into the family $B$ (again keeping dependency relations in mind).

Thus we may extend the notion of category to include not only **set** and $A$ for any **set** $A$, but also $n$-ary families of **sets** and $n$-ary functions into a **set** $A$. Note that these are indeed categories in the present sense since they are associated with criteria of application and identity, namely through the explanation of the general forms of hypothetical judgement.

## II.2 Rules

So far we have only the frame of a language, namely an explanation of its basic forms of statement as well as explanations of the basic notions of **set**, proposition, element of a **set**, and proof of a proposition. The frame is filled by the introduction of symbols signifying **sets**, operations for forming **sets**, and operations for forming elements of **sets**. These symbols are not explained one by one, but rather in groups. The
meaning of the symbols in a given group is determined by rules of four kinds:

• Formation rules

• Introduction rules

• Elimination rules

• Equality, or computation, rules

The inclusion of formation rules in the language itself is a distinctive feature of CTT. The introduction and elimination rules are like those of Gentzen (1933), though generalized to the syntax of CTT so as also to cover the construction of proof objects. The equality rules correspond to the reduction rules of Prawitz (1965). The best way of getting a grip on these notions is by looking at concrete examples, which we now proceed to do.

In the following we shall in most cases write $A[b, c]$ and $a[b, c]$, etc., instead of $A[b/x, c/y]$ and $a[b/x, c/y]$, etc. That is, for ease of readability we shall usually not mention the variables for which $b, c$, etc. are substituted in $A, a$, etc. Which variables are replaced will usually be clear from the context. Although variables are not mentioned, square brackets will still stand for substitution and not for function application.

## II.2.1 Cartesian product of a family of sets

Given a **set** $A$ and a family $B$ of **sets** over $A$ we can form the product of $B$ over $A$. That is the content of the Π-formation rule:

$$ (\Pi\text{-form}) \qquad \frac{A : \mathbf{set} \quad x : A \vdash B : \mathbf{set}}{(\Pi x : A) B : \mathbf{set}} $$

This rule lays down when we may judge that $(\Pi x : A)B$ is a **set**. There is a second Π-formation rule that lays down when we may judge that two sets of the form $(\Pi x : A)B$ are identical:

$$ \frac{A = A' : \mathbf{set} \quad x : A \vdash B = B' : \mathbf{set}}{(\Pi x : A) B = (\Pi x : A') B' : \mathbf{set}} $$

All formation, introduction, and elimination rules are paired with identity rules of this kind, but we shall state these rules explicitly only in the present case of Π.

The conclusion of Π-formation says that $(\Pi x : A)B$ is a **set**. Since we have the right to judge that $C$ is a **set** only if we can say what the canonical elements of $C$ are, as well as what equal canonical elements of $C$ are, we see that the rule of Π-formation requires justification.

The required justification is provided by the Π-introduction rules:

$$ (\Pi\text{-intro}) \qquad \frac{x : A \vdash b : B}{\lambda x. b : (\Pi x : A) B} \qquad \frac{x : A \vdash b = b' : B}{\lambda x. b = \lambda x. b' : (\Pi x : A) B} $$

According to this rule a canonical element of $(\Pi x : A)B$ has the form $\lambda x. b$, where $b[a] : B[a]$ whenever $a : A$. Note that such a $b$ is of a category different from the category of $\lambda x. b$. Namely, $b$ is of category $B(x : A)$ whereas $\lambda x. b$ is of category $(\Pi x : A)B$. It was noted above that we may regard such a $b$ as a function from $A$ into the family $B$. We may think of $\lambda x. b$ as an individual that codes this function. The $\lambda$-operator is thus similar to Frege's course-of-values operator (cf. e.g. (Frege G., 1893, p. § 9)) which, given a function $f(x)$, yields an individual $\alpha f(\alpha)$. Note, however, that $\lambda x. b$
belongs to a separate **set** $(\Pi x : A)B$ and not to the domain $A$ of the function $b$; whence we cannot make sense of applying the function $b$ to $\lambda x.b$, hence a contradiction along the lines of Russell's Paradox cannot be derived.

The role of the elements of $(\Pi x : A)B$ as codes of functions is made clear by the Π-elimination rule:

$$ (\Pi\text{-elim}) \quad \frac{c : (\Pi x : A)B \qquad a : A}{\mathbf{ap}(c, a) : B[a]} \qquad \frac{c = c' : (\Pi x : A)B \qquad a = a' : A}{\mathbf{ap}(c, a) = \mathbf{ap}(c', a') : B[a]} $$

The conclusion of this rule asserts that $\mathbf{ap}(c, a)$ is an element of the set $B[a]$. Since we have the right to judge that $c$ is an element of a set $C$ only if we can specify how to compute $c$ to a canonical element of $C$, we see that the rule of Π-elimination requires justification.

The required justification is provided by the rule of Π-equality, which specifies how $\mathbf{ap}(c, a)$ is computed in the case where $c$ is of canonical form, namely $\lambda x.b$.

$$ (\Pi\text{-eq}) \quad \frac{x : A \vdash b : B \qquad a : A}{\mathbf{ap}(\lambda x.b, a) = b[a] : B[a]} $$

We can now justify Π-elimination as follows. By the assumption $c : (\Pi x : A)B$ we know how to evaluate $c$ to canonical form $\lambda x.b$, where $x : A \vdash b : B$; thus we have $c = \lambda x.b : (\Pi x : A)B$. But then also $\mathbf{ap}(c, a) = \mathbf{ap}(\lambda x.b, a) : B[a]$, so $\mathbf{ap}(c, a) = b[a] : B[a]$, whence the value of $\mathbf{ap}(c, a)$ is equal to the value of $b[a]$; by the assumption $x : A \vdash b : B$ we know how to find this value.

From the Π-equality rule we see that **ap** is an application operator; as such it is similar to the function $x \neg y$, satisfying the equation $\Delta \neg \alpha f(\alpha) = f(\Delta)$, defined by Frege (1893, p. § 34).

We have now seen that the Π-introduction rules enable us to justify the Π-formation rule and that the Π-equality rule enables us to justify the Π-elimination rule. These relations of justification hold in general and not only in the case of Π.

The advantage of the higher-order presentation of CTT is most readily seen when we ask about the categories of Π, λ, and **ap**. Intuitively we may think of Π as a certain higher-order function that takes a **set** $A$ and a family of **sets** $B$ over $A$ and yields a **set** $(\Pi x : A)B$. But we have no means of naming the category of such a function in the language frame introduced here. In the higher-order presentation such a name is easily constructed; indeed we then express the category assignment of Π by means of the judgement $\Pi : (X : \mathbf{set})((X)\mathbf{set})\mathbf{set}$. Similar remarks apply to λ and **ap**, and in fact to all of the various symbols that we are now in the process of introducing into the language (apart from the constant sets $\mathbb{N}_n$ and $\mathbb{N}$ to be introduced below—these are of category **set**).

### II.2.2 The logical interpretation of the Cartesian product

Recall that **prop** = **set**. Hence we may regard a family $B$ of **sets** over a **set** $A$ as a family of propositions over $A$. A family of propositions over $A$ is a function from $A$ into the category of propositions; it is thus a propositional function.

Let us consider $B$ as a propositional function over $A$ and $(\Pi x : A)B$ as a proposition, and let us ask what a canonical proof of this proposition looks like. Such a canonical proof has the form $\lambda x.b$, where $x : A \vdash b : B$, and is in effect a code of the function $b$. This function $b$ takes an element $a$ of $A$ and yields a proof $b[a]$ of the proposition $B[a]$. Keeping in mind the Brouwer–Heyting–Kolmogorov interpretation of the logical connectives (cf. e.g. (Troelstra & van Dalen, 1988, pp. 9-10)), we see thus that $(\Pi x : A)B$, when regarded as a proposition, is the proposition $(\forall x : A)B$, which
intuitively says that all elements of A have the property B. Note that this proposition is not written $\forall x B$ as in ordinary predicate logic; rather, the domain of quantification, A, is explicitly mentioned.

On the understanding of Π as ∀, we can recover the rule of ∀-introduction from the rule of Π-introduction by employing the form of judgement ‘C true’ as follows.

$$ \frac{x : A \vdash B \text{ true}}{(\forall x : A)B \text{ true}} $$

That is to say, if $B[a]$ is true whenever $a : A$, then $(\forall x : A)B$ is true. Let us also consider the version of ∀-introduction where the proof objects have not been suppressed:

$$ \frac{x : A \vdash b : B}{\lambda x. b : (\forall x : A)B} $$

Here we should think of $b$ as an open proof of $B$, a proof depending on a parameter $x : A$. For instance, $A$ may be the natural numbers, $N$, and $B$ may be the propositional function that for any element $n$ of $N$ yields the proposition that $n$ is either even or odd; $b$ is then a proof of the proposition that $x$ is either even or odd, where $x$ is a generic or arbitrary natural number. By binding $x$ we get a proof $\lambda x. b$ of $(\forall x : A)B$ where $x$ is no longer free; if $x$ is the only free variable in $b$, then $\lambda x. b$ is a closed proof of $(\forall x : A)B$.

Since the domain of quantification is explicitly mentioned in $(\forall x : A)B$, it also has to be mentioned in the ∀-elimination rule:

$$ \frac{(\forall x : A)B \text{ true} \quad a : A}{B[a]true} $$

Making the proof-objects explicit yields the following ∀-elimination rule.

$$ \frac{c : (\forall x : A)B \quad a : A}{\mathbf{ap}(c, a) : B[a]} $$

The rule says that if $c$ is a proof of $(\forall x : A)B$ and $a : A$, then $\mathbf{ap}(c, a)$ is a proof of $B[a]$. The Π-equality rule can now be seen to correspond to the ∀-reduction of Prawitz (1965, p. 37) at the level of proof-objects. We shall illustrate this in the case of ⊃, to which we now turn.

Suppose $B : \mathbf{set}$. Then, by weakening, $x : A \vdash B : \mathbf{set}$ holds. In this case an element of $(\Pi x : A)B$ codes a function from the set $A$ to the set $B$. Since $x$ is not free in $B$ in this case, we may write $A \to B$ instead of $(\Pi x : A)B$, thereby also indicating that this is the function space from $A$ to $B$. Regarding both $A$ and $B$ as propositions, and again keeping in mind the Brouwer-Heyting-Kolmogorov interpretation of the logical connectives, it is clear that $A \to B$ can be interpreted as the implication $A \supset B$.

The Π-introduction and elimination rules become ⊃-introduction and elimination in this case. A canonical proof-object of $A \supset B$ has the form $\lambda x. b$, where $b$ is an open proof from $A$ to $B$. Given a proof of $c : A \supset B$ and a proof $a : A$, then $\mathbf{ap}(c, a)$ is a proof of $B$.

The Π-equality rule yields the following rule of ⊃-equality.

$$ \frac{x : A \vdash b : B \quad a : A}{\mathbf{ap}(\lambda x. b, a) = b[a] : B} $$

Here $a$ is a proof of $A$; $b$ is an open proof of $B$ from $A$; $\lambda x. b$ is a proof of $A \supset B$ obtained by extending $b$ with one application of ⊃-introduction; $\mathbf{ap}(\lambda x. b, a)$ is the
proof of $B$ got by applying $\supset$-elimination to $\lambda x. b$ and $a$; and $b[a]$ is a proof of $B$ got from $b$ by supplying it in the suitable sense with the proof $a$ of $A$. The $\supset$-equality rule says that $\mathbf{ap}(\lambda x. b, a)$ and $b[a]$ are equal proofs of $B$. Using the standard notation of natural deduction this equality can be expressed as follows (where we write $\mathcal{D}_1$ instead of $b$ and $\mathcal{D}_2$ instead of $a$).

$$ \begin{array}{ccc} & \mathcal{D}_1 & \\ \mathcal{B} & = & \mathcal{D}_2 \\ & \mathcal{A} & \\ \mathcal{A} \supset \mathcal{B} & A & \mathcal{D}_1 \\ & & \mathcal{B} \end{array} $$

By replacing ‘=’ here with a sign for Prawitz’s reduction relation, one sees that what is displayed here is just the rule of $\supset$-reduction. Thus the rule of $\supset$-equality can be read as saying that a proof containing a “detour” like that in the proof on the left hand side above is identical to the proof got by deleting this detour by means of a $\supset$-reduction.

### II.2.3 Disjoint union of a family of sets

Given a **set** $A$ and a family $B$ of **sets** over $A$ we can form the disjoint union of the family $B$. That is the content of $\Sigma$-formation:

$$ (\Sigma\text{-form}) \qquad \frac{A : \mathbf{set} \quad x : A \vdash B : \mathbf{set}}{(\Sigma x : A) B : \mathbf{set}} $$

According to the rule of $\Sigma$-introduction, the canonical elements of $(\Sigma x : A)B$ are pairs:

$$ (\Sigma\text{-intro}) \qquad \frac{a : A \qquad b : B[a]}{\langle a, b \rangle : (\Sigma x : A)B} $$

Assume $A : \mathbf{set}$, $x : A \vdash B : \mathbf{set}$. Then we may form $(\Sigma x : A)B : \mathbf{set}$. Assume further that $C$ is a family of sets over $(\Sigma x : A)B$, that is, assume $z : (\Sigma x : A)B \vdash C : \mathbf{set}$. The rule of $\Sigma$-elimination is as follows:

$$ (\Sigma\text{-elim}) \qquad \frac{c : (\Sigma x : A)B \quad x : A, y : B \vdash d : C[\langle x, y \rangle]}{\mathbf{E}(c, xy, d) : C[c]} $$

We may think of the binary function $d$ as a unary function on the canonical elements of $(\Sigma x : A)B$—it takes $\langle a, b \rangle$, where $a : A$ and $b : B[a]$, and yields an element $d[a, b]$ of $C[\langle a, b \rangle]$. The $\Sigma$-elimination rule provides us with a function $c \mapsto \mathbf{E}(c, xy, d)$ defined for all elements $c$ (not only canonical ones) of $(\Sigma x : A)B$.

Two clarificatory remarks pertaining to $\Sigma$-elimination are in order here. The first remark concerns the premiss $x : A, y : B \vdash d : C[\langle x, y \rangle]$. By the preliminary assumption $z : (\Sigma x : A)B \vdash C : \mathbf{set}$, the variable $z$, ranging over $(\Sigma x : A)B$, occurs (or, is allowed to occur) in $C$. Since $x : A, y : B \vdash \langle x, y \rangle : (\Sigma x : A)B$ holds by $\Sigma$-introduction, the substitution of $\langle x, y \rangle$ for $z$ in $C$ in the context $x : A, y : B$ makes sense. The second remark concerns the conclusion $\mathbf{E}(c, xy, d) : C[c]$. The operation $\mathbf{E}$ is variable-binding: it binds the free variables $x$ and $y$ in $d$. This is symbolized by prefixing $d$ with $x$ and $y$ inside $\mathbf{E}(-, -)$.<fnref n="40" />

<footnote n="40">⁴⁰ In the higher-order presentation there is only one variable-binding operation, namely abstraction, by means of which higher-order functions are formed. The $\mathbf{E}$ above is then a higher-order function whose second argument is itself a higher-order function $d : (x : A)(y : B) C((x, y))$. To make the notation for</footnote>
The Σ-equality rule tells us how to compute $\mathbf{E}(c, xy. d)$ when $c$ is in canonical form.

$$ (\Sigma\text{-eq}) \qquad \frac{a : A \qquad b : B[a] \qquad x : A, y : B \vdash d : C[\langle x, y \rangle]}{\mathbf{E}(\langle a, b \rangle, xy. d) = d[a, b] : C\langle a, b \rangle} $$

The conclusion of Σ-elimination introduces a non-canonical element $\mathbf{E}(c, xy. d)$ in $C[c]$. To justify this rule we have to explain how to evaluate this non-canonical element to canonical form. This is done by reference to the Σ-equality rule. First evaluate $c : (\Sigma x : A)B$ to get a pair $\langle a, b \rangle$, where $a : A$ and $b : B[a]$. We have

$$ \mathbf{E}(c, xy. d) = \mathbf{E}(\langle a, b \rangle, xy. d) = d[a, b] : C[\langle a, b \rangle] $$

by Σ-equality. By the premiss $x : A, y : B \vdash d : C[\langle x, y \rangle]$ we know how to compute $d[a, b]$ to obtain a canonical element of $C[\langle a, b \rangle]$; since $C[c] = C[\langle a, b \rangle] : \mathbf{set}$, this will also be a canonical element of $C[c]$.

By means of $\mathbf{E}$ we can define projection operations, which justifies our speaking of the canonical elements of $(\Sigma x : A)B$ as pairs. For the first projection we put $C = A$ and $d = x$ in the rule of Σ-elimination, thereby obtaining:

$$ \frac{c : (\Sigma x : A)B \qquad x : A, y : B \vdash x : A}{\mathbf{E}(c, xy. x) : A} $$

By Σ-equality we have in this case:

$$ \mathbf{E}(\langle a, b \rangle, xy. x) = x[a/x, b/y] = a : A $$

We may therefore define the first projection **fst** as follows.

$$ c : (\Sigma x : A)B \vdash \mathbf{fst}(c) = \mathbf{E}(c, xy. x) $$

For the second projection we put $C = B[\mathbf{fst}(z)]$ and $d = y$ in the rule of Σ-elimination:

$$ \frac{c : (\Sigma x : A)B \qquad x : A, y : B \vdash y : B[\mathbf{fst}(\langle x, y \rangle)]}{\mathbf{E}(c, xy. y) : B[\mathbf{fst}(c)]} $$

The second premiss here is valid since $x : A, y : B \vdash B[\mathbf{fst}(\langle x, y \rangle)] = B[x] = B : \mathbf{set}$ holds. By Σ-equality we have

$$ \mathbf{E}(\langle a, b \rangle, xy. y) = y[a/x, b/y] = b : B[\mathbf{fst}(\langle a, b \rangle)] $$

But $\mathbf{fst}(\langle a, b \rangle) = a : A$, hence

$$ B[\mathbf{fst}(\langle a, b \rangle)] = B[a] : \mathbf{set} $$

We therefore define the second projection by

$$ c : (\Sigma x : A)B \vdash \mathbf{snd}(c) = \mathbf{E}(c, xy. y) $$

The following four rules are then justified

<footnote>$\lambda$ in the Π-introduction rule accord with the notation here used for $\mathbf{E}$ we should write $\lambda(x. b)$ instead of $\lambda x. b$. The latter, being more familiar, will be preferred here.</footnote>
$$ \frac{c : (\Sigma x : A)B}{fst(c) : A} $$

$$ \frac{a : A}{b : B[a]} \\ \mathrm{fst}((a, b)) = a : A $$

$$ \frac{c : (\Sigma x : A)B}{snd(c) : B[fst(c)]} $$

$$ \frac{a : A}{b : B[a]} \\ \mathrm{snd}((a, b)) = b : B[a] $$

### II.2.4 The logical interpretation of the disjoint union of a family of sets

If we regard $B$ as a propositional function over $A$, then $(\Sigma x : A)B$ can be regarded as the existentially quantified proposition $(\exists x : A)B$. A canonical proof of $(\exists x : A)B$ is a pair $\langle a, b \rangle$ where $a : A$ and $b : B[a]$; that is to say, $a$ is a witness and $b$ is a proof that $a$ indeed has the property $B$. When suppressing proof objects and employing the form of judgement $D$ true, the rule of $\Sigma$-elimination becomes $\exists$-elimination:

$$ \frac{\begin{array}{l} (\exists x : A)B \text{ true} \\ x : A, B \text{ true} \end{array} \quad \begin{array}{l} \vdash \quad C \text{ true} \\ C \text{ true} \end{array}}{A \wedge B : \mathbf{prop}} $$

In ordinary natural deduction the assumption $x : A$ in the second premiss is usually not made explicit.

If $B : \mathbf{set}$ holds categorically, then the rules for $\Sigma$ yield rules for ordinary Cartesian product. On the logical interpretation, the Cartesian product becomes conjunction. Indeed the $\Sigma$-formation and introduction rules then become:

$$ \frac{A : \mathbf{prop}}{A \wedge B : \mathbf{prop}} B : \mathbf{prop} $$

$$ \frac{a : A}{\langle a, b \rangle : A \wedge B} b : B $$

The $\Sigma$-elimination rule, with and without proof-objects, becomes:

$$ \frac{A \wedge B \text{ true} \qquad A \text{ true}, B \text{ true} \quad \vdash \quad C \text{ true}}{C \text{ true}} $$

$$ \frac{c : A \wedge B \qquad x : A, y : B \quad \vdash \quad d : C[\langle a, b \rangle]}{E(c, xy, d) : C[c]} $$

This is a generalization of the ordinary rules of $\wedge$-elimination also found in Schroeder-Heister (1984, p. 1294). The ordinary rules are obtained as a special case by letting $C$ be $A$ or $B$. We remark that in the higher-order presentation a generalized elimination rule in this sense can also be given for $\Pi$ Nordström et al. (Nordström, Petersson, & Smith, 1990, pp. 51-52); using this generalized elimination rule instead of the rule of $\Pi$-elimination presented above in fact yields a strictly stronger theory, as shown by Garner (2009).

### II.2.5 Disjoint union of two sets

Given two sets we may form their disjoint union. That is content of the rule of $+-$ formation.

$$ (+-\text{form}) \qquad \frac{A : \mathbf{set}}{A + B : \mathbf{set}} B : \mathbf{set} $$

A canonical element of $A + B$ is an element of $A$ or an element of $B$ together with the
information that it comes from A or B respectively. Thus there are two rules of +-introduction:

$$ (+-intro) \qquad \frac{a : A}{\mathbf{i}(a) : A + B} \qquad \frac{b : B}{\mathbf{j}(b) : A + B} $$

Assume $A : \mathbf{set}$, $B : \mathbf{set}$, and $z : A + B \vdash C : \mathbf{set}$. The rule of +-elimination is:

$$ (+-elim) \qquad \frac{c : A + B \qquad x : A \vdash d : C[\mathbf{i}(x)] \qquad y : B \vdash e : C[\mathbf{j}(y)]}{\mathbf{D}(c, x. d, y. e) : C[c]} $$

The rule can be glossed as follows. Assume that $C$ is a family of **sets** over $A + B$ and that we are given a function $d$ which takes an $a : A$ to an element $d[a]$ of $C[\mathbf{i}(a)]$ and a function $e$ which takes a $b : B$ to an element $e[b]$ of $C[\mathbf{j}(b)]$. Then $C[c]$ is inhabited for any $c : C$, namely by $\mathbf{D}(c, x. d, y. e)$. How to compute $\mathbf{D}(c, x. d, y. e)$ is determined by the +-equality rules. Since there are two +-introduction rules, there are also two +-equality rules.

$$ (+-eq) \qquad \frac{a : A \qquad x : A \vdash d : C[\mathbf{i}(x)] \qquad y : B \vdash e : C[\mathbf{j}(y)]}{\mathbf{D}(\mathbf{i}(a), x. d, y. e) = d[a] : C[\mathbf{i}(a)]} $$

$$ \frac{b : B \qquad x : A \vdash d : C[\mathbf{i}(x)] \qquad y : B \vdash e : C[\mathbf{j}(y)]}{\mathbf{D}(\mathbf{j}(b), x. d, y. e) = e[b] : C[\mathbf{j}(b)]} $$

In the logical interpretation + becomes disjunction ∨.

## II.2.6 Finite sets

We have introduced operations for constructing **sets** from other **sets** or families of **sets**; but so far we have no basic **set** to start from. We shall now provide a scheme of rules which, when specified for any particular natural number $n$, gives us a **set** with $n$ canonical elements.

In the following $n$ is a generic natural number. There is a set $\mathbb{N}_n$:

$$ (\mathbb{N}_n\text{-form}) \qquad \mathbb{N}_n : \mathbf{set} $$

The set $\mathbb{N}$ has $n$ canonical elements, each introduced by its own introduction rule; thus $\mathbb{N}_n$ has $n$ introduction rules:

$$ (\mathbb{N}_n\text{-intro}) \qquad m_1 : \mathbb{N}_n, \dots, m_n : \mathbb{N}_n $$

The $\mathbb{N}_n$-elimination rule can be seen as a principle of proof by $n$ cases. We assume that $C$ is a family of **sets** over $\mathbb{N}_n$; that is, we assume $z : \mathbb{N}_n \vdash C : \mathbf{set}$.

$$ (\mathbb{N}_n\text{-elim}) \qquad \frac{m : \mathbb{N}_n \qquad c_1 : C[m_1] \qquad \dots \qquad c_n : C[m_n]}{\mathbf{case}_n(m, c_1, \dots, c_n) : C[m]} $$

Thus, assume that for each canonical $m_k : \mathbb{N}_n$ we have an element $c_k : C[m_k]$. The $\mathbb{N}_n$-elimination rule allows us to infer that for any $m : \mathbb{N}_n$ there is an element, namely $\mathbf{case}_n(m, c_1, \dots, c_n)$, in $C[m]$. How to compute $\mathbf{case}_n(m, c_1, \dots, c_n)$ to canonical form is determined by the $\mathbb{N}_n$-equality rules. Since there are $n$ $\mathbb{N}_n$-introduction rules, there are
also $n \mathbb{N}_n$-equality rules, one for each introduction rule. We state the rule for a generic $k \le n$.

$$ (\mathbb{N}_n\text{-eq}) \qquad \frac{c_1 : C[m_1] \quad \dots \quad c_n : C[m_n]}{\mathbf{case}_n(m_k, c_1, \dots, c_n) = c_k : C[m_k]} $$

On the basis of this rule we may explain how to compute $\mathbf{case}_n(m, c_1, ..., c_n) : C[c]$. Evaluate $m : \mathbb{N}_n$, thereby obtaining a canonical element $m_k : \mathbb{N}_n$. Since $m = m_k : \mathbb{N}_n$, we have both $\mathbf{case}_n(m, c_1, ..., c_n) = c \ \mathbf{ase}_n(m_k, c_1, ..., c_n) : C[m_k]$ and $C[m_k] = C[m] : \mathbf{set}$. Therefore, $\mathbf{case}_n(m, c_1, ..., c_n) = c_k : C[m]$, by $\mathbb{N}_n$-equality. Hence the value of $\mathbf{case}_n(m, c_1, ..., c_n)$ equals the value of $c_k$, which we know how to compute by the premiss $c_k : C[m_k]$.

We may give $\mathbb{N}_2$ the name **bool**; the canonical elements of $\mathbb{N}_2$ the names **t** and **f**; and the expression $\mathbf{case}_2(m, c_1, c_2)$ may be written **if m then c else c_2**. Let $C$ be a family of sets over **bool**; that is, assume $z : \mathbf{bool} \vdash C : \mathbf{set}$. We have the following two rules of **bool**-elimination, which we here state as one rule with two conclusions:

$$ \frac{c : C[t] \qquad d : C[f]}{\mathbf{if t then c else d} = c : C[t] \qquad \mathbf{if f then c else d} = d : C[f]} $$

Familiar Boolean functions can be defined from **t**, **f**, and **if m then c else c_2** as follows.

$$ a : \mathbf{bool}, b : \mathbf{bool} \vdash a \text{ and } b = \mathbf{if a then b else f} : \mathbf{bool} $$

$$ a : \mathbf{bool}, b : \mathbf{bool} \vdash a \text{ or } b = \mathbf{if a then t else b} : \mathbf{bool} $$

$$ a : \mathbf{bool} \vdash \mathbf{not} a = \mathbf{if a then f else t} : \mathbf{bool} $$

The set $\mathbb{N}_0$ has 0, that is no, introduction rules; but it does have an elimination rule:

$$ \frac{m : \mathbb{N}_0}{\mathbf{case}_0(m) : C[m]} $$

Thus, in particular, if we are given $C : \mathbf{set}$ and $m : \mathbb{N}_0$, then we may infer that $C$ is inhabited, namely by $\mathbf{case}_0(m)$. Since there is no $\mathbb{N}_0$-introduction rule, neither is there a $\mathbb{N}_0$-equality rule. The justification of $\mathbb{N}_0$-elimination is therefore different in character from the justification of the other elimination rules. A rule of inference is justified if we can make the conclusion of the rule evident on the assumption that its premisses are known (cf. eg. (Sundholm, 2012)). Since $\mathbb{N}_0$ has no introduction rule and therefore no canonical elements, the premiss $m : \mathbb{N}_0$ of $\mathbb{N}_0$-elimination cannot be known. The rule of $\mathbb{N}_0$-elimination is therefore vacuously justified, for the assumption that its premiss is known cannot be fulfilled.

In the logical interpretation $\mathbb{N}_0$ becomes absurdity $\perp$. In CTT absurdity is thus the proposition that by definition has no introduction rule. The rule of $\perp$-elimination is the principle of *ex falso quodlibet*:

$$ \frac{\perp \quad \mathbf{true}}{C \quad \mathbf{true}} $$

We define the negation of a proposition $A$ to be the proposition $A \supset \perp$:<fnref n="41" />

<footnote n="41">⁴¹ In the higher-order presentation $\neg$ may be defined in the empty context, namely as follows.</footnote>

<footnote>$\neg = [A]A \supset \perp : (\mathbf{prop})\mathbf{prop}$</footnote>
$$A : \mathbf{prop} \vdash \neg A = A \supset \bot$$

The following rules are then derivable.

$$\frac{A : \mathbf{prop}}{\neg A : \mathbf{prop}}$$

$$\frac{x : A \vdash b : \bot}{\lambda x.b : \neg A}$$

$$\frac{b : \neg A}{\mathbf{ap}(b, a) : C} \qquad \frac{a : A}{\mathbf{ap}(b, a) : C}$$

## II.2.7 The natural numbers

We shall not need the natural numbers in later chapters, but it may nevertheless be useful to see that the primitive notions of arithmetic can be introduced by Gentzen-Prawitz style rules.

(N-form)

N : set

The canonical elements of $\mathbb{N}$ are 0 and $s(n)$, where $n$ is any $\mathbb{N}$, not necessarily of canonical form:

(N-intro)

0 : N

$$\frac{n : \mathbb{N}}{s(n) : \mathbb{N}}$$

The rule of N-elimination is simultaneously a principle of definition by recursion and proof by mathematical induction. Assume that $C$ is a family of sets over $\mathbb{N}$; that is, assume $z : \mathbb{N} \vdash C : \mathbf{set}$.

(N-elim)

$$\frac{n : \mathbb{N} \quad d : C[0] \quad x : \mathbb{N}, y : C[x] \vdash e : C[s(x)]}{\mathbf{R}(n, d, xy. e) : C[n]}$$

We are given an element $d : C[0]$ together with a function $e$ that takes $k : \mathbb{N}$ and $c : C[k]$ and yields $e[k, c] : C[s(k)]$. The rule tells us that for an arbitrary $n : \mathbb{N}$ the **set** $C[n]$ is then inhabited, namely by $\mathbf{R}(n, d, xy. e)$.

To see that N-elimination encapsulates the ordinary principle of proof by induction over the natural numbers, assume that $C$ is a propositional function over $\mathbb{N}$. Then $d$ is a proof of the base case $C[0]$ and $e$ is a proof of the induction step; that is, $e$ is an open proof from $C[k]$ to $C[s(k)]$. The conclusion of N-elimination says that $C[n]$ is inhabited, that is, true, for an arbitrary $n : \mathbb{N}$.

The rule of N-equality tells us how to compute $\mathbf{R}(n, d, xy. e)$ when $n$ is of canonical form. Since there are two N-introduction rules, there are also two N-equality rules, which we here state more simply without the premisses

$$\frac{\mathbf{R}(0, d, xy. e) = d : C[0]}{(\mathbf{N}\text{-eq}) \qquad \mathbf{R}(s(n), d, xy. e) = e[n, \mathbf{R}(n, d, xy. e)] : C[s(n)]}$$

This gives in particular:

$$\mathbf{R}(s(0), d, xy. e) = e[0, \mathbf{R}(0, d, xy. e)] = e[0, d] : C[s(0)]$$

$$\mathbf{R}(s(s(0)), d, xy. e) = e[s(0), \mathbf{R}(s(0), d, xy. e)] = e[s(0), e[0, d]] : C[s(s(0))]$$

$$\mathbf{R}(s(s(s(0))), d, xy. e) = e[s(s(0)), e[s(0), e[0, d]]] : C[s(s(s(0)))]$$

<footnote>Thus, $\neg$ is a function which takes a **prop** A as argument and yields a **prop** $\neg A$ as value. Similar considerations apply to the definitions of **fst** and **snd** above as well as to the definitions given below pertaining to $\mathbb{N}$.</footnote>
It should be clear from these few computations that **R** provides a means for defining
functions by recursion.

In general, to compute $\mathbf{R}(m, d, xy.e)$ first evaluate $m$ to canonical form. If the
value is 0, output $d$; if the value is $s(n)$, continue by computing $e[n, \mathbf{R}(n, d, xy.e)]$.

By letting $C$ be $\mathbb{N}$ and $e$ be $s(y)$ in $\mathbb{N}$-elimination, one can infer $a : \mathbb{N}, b : \mathbb{N} \vdash$ $\mathbf{R}(b, a, xy.s(y)) : \mathbb{N}$. The reader may check that we here have the definiens of the addition function, in other words, that addition can be defined as follows.

$$a : \mathbb{N}, b : \mathbb{N} \vdash a + b = \mathbf{R}(b, a, xy.s(y)) : \mathbb{N}$$

To define multiplication we let $C$ be $\mathbb{N}$, $d$ be 0, and $e$ be $y + a$.

$$a : \mathbb{N}, b : \mathbb{N} \vdash a \times b = \mathbf{R}(b, 0, xy.(y + a)) : \mathbb{N}$$

### II.2.8 Propositional identity

In the language developed so far we can express identities by means of judgements $a = b : C$. Judgements cannot, however, be operated on by the propositional operators, that is, for instance by conjunction or universal quantification. Since we want to be able to operate on identity statements with the propositional operations, it is clear that we need identity propositions. Thus, for each **set** $A$ we wish to introduce a binary propositional function $x =_A y$ of identity over $A$. Instead of $x =_A y$, we shall usually write **Id**($A, x, y$). The rule of **Id**-formation states that given a **set** $A$ and two elements $a, b$ of $A$, there is a proposition **Id**($A, a, b$).

$$ (\mathbf{Id}\text{-form}) \qquad \frac{A : \mathbf{set} \qquad a : A \qquad b : A}{\mathbf{Id}(A, a, b) : \mathbf{prop}} $$

Note that by this rule there is no identity proposition between $a$ and $b$ unless $a$ and $b$ belong to the same **set**. Hence, assuming that Julius Caesar and the number 7 do not belong to the same **set**, there is no proposition to the effect that Julius Caesar and 7 are identical.

It is only with the introduction of **Id** that we are able to define propositional functions in our language. Namely, given a **set** $A$ we now have a propositional function **Id**($A, x, y$) over $A$, by means of which other propositional functions can be defined. For instance, we may now define $x \le y$ over $\mathbb{N}$ by

$$x : \mathbb{N}, y : \mathbb{N} \vdash x \leq y = (\exists z : \mathbb{N}) \mathbf{Id}(\mathbb{N}, x + z, y) : \mathbf{prop}$$

Notice the use of judgemental identity $A = B : \mathbf{prop}$ here: the definition in effect identifies two propositions in the context $x : \mathbb{N}, y : \mathbb{N}$. It may be useful to see how one may define the propositional function $\mathbf{Pr}(x)$, saying that $x$ is a prime number, in CTT. In ordinary predicate logic with restricted quantifiers we may use a definition such as the following (for the purposes of this presentation let us assume that 0 and 1 are prime numbers).

$$\mathbf{Pr}(n) \equiv \forall x, y \le n (x \times y = n \supset (x = 1 \lor x = n))$$

In CTT restricted quantification may be defined as quantification over $(\exists z : \mathbb{N})z \le n$. Such quantification makes sense, since $(\exists z : \mathbb{N})z \le n$ is a set for any $n : \mathbb{N}$. An element of this set is a pair $\langle k, p \rangle$, where $k$ is a $\mathbb{N}$ and $p$ is a proof of $k \le n$. We may define $\mathbf{Pr}$ as follows.
$$ n : \mathbb{N} \vdash \mathbf{Pr}(n) = (\forall x, y : (\exists z : \mathbb{N})z \le n) \quad ((\mathbf{fst}(x) \times \mathbf{fst}(y)) = \mathbb{N} n) \supset (\mathbf{fst}(x) = \mathbb{N} 1 \lor \mathbf{fst}(x) = \mathbb{N} n) : \mathbf{prop} $$

Here we have used the notation $x = \mathbb{N} y$ instead of the official $\mathbf{Id}(\mathbb{N}, x, y)$, and we have contracted the two quantifiers by writing $(\forall x, y : (\exists z : \mathbb{N})z \le n)$.

To justify the rule of **Id**-formation we have to specify what is a canonical proof of $\mathbf{Id}(A, a, b)$. What, for instance, should be a canonical proof of the proposition $\mathbf{Id}(\mathbb{N}, 0, 0)$? The Brouwer–Heyting–Kolmogorov explanation will not help us in answering this question, since it is silent about identity propositions. Since we want $\mathbf{Id}(\mathbb{N}, x, y)$ to be the relation of identity over $\mathbb{N}$ and since a proposition is here taken to be true if it is inhabited as a **set**, it is clear that we simply have to introduce a proof of $\mathbf{Id}(\mathbb{N}, 0, 0)$ by stipulation; we call this proof **refl(\mathbb{N}, 0)**. The rule of **Id**-introduction is as follows.

$$ (\mathbf{Id}\text{-intro}) \qquad \frac{a : A}{\mathbf{refl}(A, a) : \mathbf{Id}(A, a, a)} $$

Thus, provided $a : A$, we stipulate that there is a proof $\mathbf{refl}(A, a) : \mathbf{Id}(A, a, a)$. We here emphasize the aspect of stipulation, but in fact, all introduction rules are purely stipulatory in nature. An introduction rule stipulates that the canonical elements of the **set** under consideration look such and such. The **Id**-introduction rule is in this regard no different from other introduction rules.

The **Id**-introduction rule is different from other introduction rules in that it does not immediately yield an answer to the question of what is a canonical element of $\mathbf{Id}(A, a, b)$, that is, of a **set** of the form introduced by **Id**-formation. It yields an answer only to the question of what is a canonical element of $\mathbf{Id}(A, a, a)$. Since no introduction rule has $\mathbf{Id}(A, a, b)$ as the predicate $C$ of its conclusion $c : C$, it is clear that the only way in which we can come to judge that $c$ is a canonical element of $\mathbf{Id}(A, a, b)$ is on the basis of an identity judgement of the form $C = \mathbf{Id}(A, a, b) : \mathbf{prop}$, where $c : C$ is the conclusion of an application of an introduction rule. It is, moreover, clear that any such $C$ must have the form $\mathbf{Id}(A', a', a')$, where $A = A' : \mathbf{set}$, $a = a' : A$ and $b = a' : A$. A canonical element of $\mathbf{Id}(A, a, b)$ is therefore of the form $\mathbf{refl}(A', a')$ where $A = A' : \mathbf{set}$, $a = a' : A$ and $b = a' : A$.

Martin-Löf (1971), in a paper concerned with natural deduction rather than Type Theory, provided a general scheme of introduction and elimination rules as well as reduction procedures for so-called inductively defined predicates. The rules provided above for $\mathbb{N}_n$ and $\mathbb{N}$ follow this scheme, although they are adapted to the syntax of CTT. Also the identity predicate of ordinary predicate logic is covered by this rule scheme (Martin-Löf, 1971, p. 190). The ordinary binary identity predicate, which Martin-Löf designates by $E$, is the predicate that has the introduction rule

$Exx$

with no premisses. It should be clear how the rule of **Id**-introduction above is an adaptation of this rule to the syntax of CTT. Martin-Löf's scheme yields the following elimination rule for $E$:

$$ \frac{\text{Etu} \qquad C[z/x, z/y]}{C[t/x, u/y]} $$

Here $C$ is any formula of the language, and $C[z/x, z/y]$ is the result of substituting the variable $z$ for both $x$ and $y$ in $C$. If we assume that $x$ and $y$ are all and only the free variables in $C$, then we may think of $C$ as defining a binary relation over the underlying
domain. That we can prove $C[z/x, z/y]$ means that the relation defined by $C$ is reflexive. The $E$-elimination rule allows us to infer that the relation defined by $C$ is true of $t$ and $u$ provided we have a derivation of Etu. Thus the rule says in effect that $E$ is the smallest reflexive relation over the underlying domain.

The rule of **Id-elimination** generalizes the $E$-elimination rule to the syntax of CTT; it generalizes the $E$-elimination rule also in allowing the relation $C$ occurring in the minor premiss to include as argument a proof-object of the identity proposition being eliminated. Assume $A : \mathbf{set}$, $a : A$, $b : A$, and $x : A$, $y : A$, $u : \mathbf{Id}(A, x, y) \vdash C : \mathbf{set}$.

$$ (\mathbf{Id}\text{-elim}) \qquad \frac{p : \mathbf{Id}(A, a, b) \quad z : A \vdash d : C[z, z, \mathbf{refl}(A, z)]}{J(p, z. d) : C[a, b, p]} $$

Thus, if we have a proof $p$ of the proposition $\mathbf{Id}(A, a, b)$ and a function $d$ taking any $a'$ of $A$ to a proof that the ternary relation $C$ holds of the triple $a', a', \mathbf{refl}(A, a')$; then $\mathbf{Id}$-elimination allows us to infer that there is a proof $J(p, z. d)$ of $C[a, b, p]$.

The rule of **Id-equality** tells us how to compute $J(p, z. d)$ when $p$ is of canonical form, $\mathbf{refl}(A, a)$.

$$ (\mathbf{Id}\text{-eq}) \qquad J(\mathbf{refl}(A, a), z. d) = d[a] : C[a, a, \mathbf{refl}(A, a)] $$

The rule of **Id-elimination** can now be justified as follows. To evaluate $J(p, z. d)$ first evaluate $p$ to get a canonical element of $\mathbf{Id}(A, a, b)$. As noted above, such a canonical element has the form $\mathbf{refl}(A', a')$, where $A = A' : \mathbf{set}$, $a = a' : A$ and $b = a' : A$. Hence,

$$ J(p, z. d) = J(\mathbf{refl}(A', a'), z. d) = d[a'] : C[a', a', \mathbf{refl}(A', a')]. $$

By the assumption $z : A \vdash d : C[z, z, \mathbf{refl}(z)]$ we know how to evaluate $d[a']$ to canonical form. It remains then only to see that $C[a', a', \mathbf{refl}(A', a')] = C[a, b, p] : \mathbf{set}$, but this follows from the judgemental identities

$$ A = A' : \mathbf{set}; a = a' : A; b = a' : A; p = \mathbf{refl}(A', a') : \mathbf{Id}(A, a, b) $$

together with the extensionality of substitution into **sets** with respect to judgemental identity.

In many applications of **Id-elimination** the family $C$ in its minor premiss does not depend on the set $\mathbf{Id}(A, a, b)$ of its major premiss. Thus, $C$ will then be a **set** already in the context $x : A, y : A$; that is, $C$ will then be a binary relation over $A$. What is required then for an application of **Id-elimination** is that we have a function $d$ witnessing that $C$ is a reflexive relation over $A$; more precisely, that $d[a]$ is a proof of $C[a, a]$ for any $a : A$. We shall now demonstrate how **Id-elimination** is used in practice by showing that the relation $\mathbf{Id}(A, x, y)$ is symmetric and transitive, and by showing that if $F[a]$ and $\mathbf{Id}(A, a, b)$ are true, then so is $F[b]$, that is, by showing the indiscernibility of elements related by $\mathbf{Id}(A, x, y)$. The main task in each case is to find a suitable $C$ and a suitable function $d$ taking $a : A$ and yielding a proof of $C[a, a]$.

For symmetry let $C$ be $\mathbf{Id}(A, y, x)$. It is clear that $z : A \vdash \mathbf{refl}(A, z) : \mathbf{Id}(A, z, z)$, so we let $d$ be $\mathbf{refl}(A, z)$. If we insert these data into **Id-elimination** we get:

$$ \frac{p : \mathbf{Id}(A, a, b) \quad z : A \vdash \mathbf{refl}(A, z) : \mathbf{Id}(A, z, z)}{J(p, z. \mathbf{refl}(A, z)) : \mathbf{Id}(A, b, a)} $$

Hence, from a proof $p : \mathbf{Id}(A, a, b)$ we get a proof $J(p, z. \mathbf{refl}(A, z)) : \mathbf{Id}(A, b, a)$.
Assuming that $p$ here is a closed term, one can argue, on the basis of the explanation of what a canonical proof of an identity proposition is, that $p$ is identical with the proof $\mathbf{J}(p, z. \mathbf{refl}(A, z))$. Namely, the judgement $p : \mathbf{Id}(A, a, b)$ means that $p$, since it is a closed term, evaluates to a proof of the form $\mathbf{refl}(A', a')$, where $A = A' : \mathbf{set}$, $a = a' : A$, and $b = a' : A$; hence, $p = \mathbf{refl}(A', a') : \mathbf{Id}(A, a, b)$. Therefore,

$$ \mathbf{J}(p, z. \mathbf{refl}(A, z)) = \mathbf{J}(\mathbf{refl}(A', a'), z. \mathbf{refl}(A, z)) = \mathbf{refl}(A, a') : \mathbf{Id}(A, b, a) $$

Since $A = A' : \mathbf{set}$, we get:

$$ p = \mathbf{refl}(A', a') = \mathbf{refl}(A, a') = \mathbf{J}(p, z. \mathbf{refl}(A, z)) : \mathbf{Id}(A, b, a) $$

It should be emphasized that this reasoning i) presupposes that $p$ is closed and ii) is not a computation in the theory itself; the computation in any particular case depends on what the given proof-object $p : \mathbf{Id}(A, a, b)$ looks like.

For transitivity we let $C$ be $\mathbf{Id}(A, y, c) \supset \mathbf{Id}(A, x, c)$ for an arbitrary $c : A$. We have $\lambda u. u : \mathbf{Id}(A, z, c) \supset \mathbf{Id}(A, z, c)$, so we let $d$ be $\lambda u. u$. Inserting these data into $\mathbf{Id}$-elimination yields:

$$ \frac{p : \mathbf{Id}(A, a, b) \qquad z : A \vdash \lambda u. u : \mathbf{Id}(A, z, c) \supset \mathbf{Id}(A, z, c)}{\mathbf{J}(p, \lambda u. u) : \mathbf{Id}(A, b, c) \supset \mathbf{Id}(A, a, c)} $$

Hence, from a proof $p : \mathbf{Id}(A, a, b)$ and a proof $q : \mathbf{Id}(A, b, c)$, we get a proof $\mathbf{ap}(\mathbf{J}(p, \lambda u. u), q) : \mathbf{Id}(A, a, c)$. Note that $\lambda u. u$ does not depend on $z : A$, hence no variable gets bound by this application of $\mathbf{Id}$-elimination. Assuming that $p$ is closed, we can argue as above that $p = \mathbf{refl}(A', a') : \mathbf{Id}(A, a, b)$, whence by $\mathbf{Id}$-equality and $\Pi$-equality we get:

$$ \mathbf{ap}(\mathbf{J}(p, \lambda u. u), q) = \mathbf{ap}(\mathbf{J}(\mathbf{refl}(A', a'), \lambda u. u), q) = \mathbf{ap}(\lambda u. u, q) = q : \mathbf{Id}(A, a, c) $$

Again it must be emphasized that this argument is not the same as an actual computation in the theory.

For the indiscernibility of elements $a, b$ for which $\mathbf{Id}(A, a, b)$ is true, let $F$ be a propositional function over $A$, that is $x : A \vdash F : \mathbf{prop}$. Let $C$ be $F[x] \supset F[y]$. Again we have $\lambda u. u : F[z] \supset F[z]$, hence $\mathbf{Id}$-elimination yields:

$$ \frac{p : \mathbf{Id}(A, a, b) \qquad z : A \vdash \lambda u. u : F[z] \supset F[z]}{\mathbf{J}(p, \lambda u. u) : F[a] \supset F[b]} $$

Hence, from a proof $p : \mathbf{Id}(A, a, b)$ and a proof $q : F[a]$, we get a proof

$$ \mathbf{ap}(\mathbf{J}(p, \lambda u. u), q) : F[b]. $$

As in the case of transitivity above we can argue that $\mathbf{ap}(\mathbf{J}(p, \lambda u. u), q) = q : F[b]$ on the assumption that $p$ is closed.

The second $\mathbf{Id}$-formation rule, the rule that governs when two sets of the form $\mathbf{Id}(A, a, b)$ are identical, is as follows.

$$ \frac{A = A' : \mathbf{set} \qquad a = a' : A \qquad b = b' : A}{\mathbf{Id}(A, a, b) = \mathbf{Id}(A', a', b') : \mathbf{set}} $$

Employing this rule together with the general rules governing judgemental identity, one
sees that the following rule is derivable:

$$ \frac{a = b : A}{\mathbf{refl}(A, a) : \mathbf{Id}(A, a, b)} $$

The rule of identity elimination employed in (Martin-Löf, 1984) lays down that one can also go the other way:

$$ \frac{p : \mathbf{Id}(A, a, b)}{a = b : A} $$

In the literature this rule is sometimes called extensional identity elimination, whereas the rule of **Id-elimination** is called intensional. Subsequent metamathematical work has shown that this extensional rule has several undesirable consequences, perhaps the strongest of which is that in the presence of this rule judgements of the form $a = b : A$ become undecidable in general (Hofmann, 1995, p. Theorem 3.2.1). From the normalization theorem of Martin-Löf (1975b) for the system employing the intensional **Id-elimination** rule it follows that judgements of the form $a = b : A$ are decidable in this system. For this and other reasons,<fnref n="42" /> most presentations of CTT prefer the intensional system.

It follows from Martin-Löf's normalization theorem that if $p : \mathbf{Id}(A, a, b)$ is demonstrable in the empty context, then so is $a = b : A$; hence if one can construct a closed proof $p$ of $\mathbf{Id}(A, a, b)$, then the judgemental identity $a = b : A$ is demonstrable (Martin-Löf, 1975b, p. Theorem 3.14). In a non-empty context, however, one can in general not infer $a = b : A$ from $p : \mathbf{Id}(A, a, b)$. For instance, using $\Sigma$-elimination one can prove

$$ z : A \times B \vdash \mathbf{E}(z, xy. \mathbf{refl}(A \times B, \langle x, y \rangle)) : \mathbf{Id}(A \times B, z, \langle \mathbf{fst}(z), \mathbf{snd}(z) \rangle) $$

But there is no way of demonstrating the corresponding judgemental identity

$$ z : A \times B \vdash z = \langle \mathbf{fst}(z), \mathbf{snd}(z) \rangle : A \times B $$

since $z$ and $\langle \mathbf{fst}(z), \mathbf{snd}(z) \rangle$ are different normal forms in the context $z : A \times B$ (this example is taken from (Martin-Löf, 1975a, pp. 103-104)). We see therefore that judgemental identity $a = b : A$ and propositional identity $\mathbf{Id}(A, a, b)$ do not only have different logical form, but also that they differ in logical strength. These are therefore two essentially different notions of identity.

<footnote n="42">⁴² In Homotopy Type Theory the main reason to prefer the intensional **Id-elimination** rule is that it does not entail</footnote>

<footnote>($\forall p, q : \mathbf{Id}(A, a, b)) \mathbf{Id}(\mathbf{Id}(A, a, b), p, q)$ true for arbitrary $A$ and $a, b : A$, a result that was established by (Hofmann & Streicher, 1998).</footnote>
# Exercises

The word ‘proof’ has been reserved for proof-objects. Derivations in Constructive Type Theory are often called *demonstrations*. Most exercises below ask the reader to demonstrate *A true* for a given proposition *A*. It is then intended that a demonstration be given whose conclusion has the form *a : A*.

1. Let A : **prop**, B : **prop**. Demonstrate the following judgements.

$$a) A \supset (B \supset A) \text{ true}$$

$$b) (A \wedge B) \supset (A \vee B) \text{ true}$$

$$c) \neg(A \vee B) \supset \neg A \text{ true}$$

2. Let $D$ : set, $x : D \vdash A : \mathbf{prop}$, and $x : D \vdash B : \mathbf{prop}$. That is to say, $A$ and $B$ are propositional functions over $D$. Demonstrate the following judgements.

$$a) (\exists x : D)(A \wedge B) \supset ((\exists x : D)A \wedge (\exists x : D)B) \text{ true}$$

$$b) (\forall x : D)(A \wedge B) \supset ((\forall x : D)A \wedge (\forall x : D)B) \text{ true}$$

$$c) (\exists x : D)(A \vee B) \supset ((\exists x : D)A \vee (\exists x : D)B) \text{ true}$$

3. Let $D$ : set and $x : D$, $y : D \vdash R : \mathbf{prop}$. That is to say, $R$ is a binary relation over $D$. Demonstrate

$$(\exists x : D)(\forall y : D)R[x, y] \supset (\forall y : D)(\exists x : D)R[x, y] \text{ true}$$

(Note that $R[x, y] \equiv R[x/x, y/y] \equiv R$.)

4. In its class-theoretic form, the syllogism of Barbara may be formulated as follows.

All A's are B.

All B's are C.

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

∴ All A's are C.

Formalize Barbara in CTT. Assume that you have been given proof-objects of the premises; construct a proof-object of the conclusion.

5. Formalize in CTT the following class-theoretical reasoning. “Everything is an A; whatever is an A is a B; hence, everything is a B.”

Given a proof-object of the two premises, construct a proof-object of the conclusion.

6. Let A : **set**, B : **set**, and assume $c : A \to B$. Demonstrate

$$\mathbf{Id}(A, a, a') \supset \mathbf{Id}(B, \mathbf{ap}(c, a), \mathbf{ap}(c, a')) \text{ true}$$

7. Let A : **set**, B : **set**. Assume $p : \mathbf{Id}(A, a, a')$ and $q : \mathbf{Id}(B, b, b')$. Demonstrate

$$\mathbf{Id}(A \times B, \langle a, b \rangle, \langle a', b' \rangle) \text{ true}$$

8. Demonstrate

$$a) (\forall x : \mathbf{bool})(\mathbf{Id}(\mathbf{bool}, x, f) \vee \mathbf{Id}(\mathbf{bool}, x, f)) \text{ true}$$

$$b) (\forall x : \mathbb{N})(\mathbf{Id}(\mathbb{N}, x, 0) \vee (\exists y : \mathbb{N})\mathbf{Id}(\mathbb{N}, x, s(y))) \text{ true}$$
# Solutions

1. In the solutions to these exercises we will include all the details. Each demonstration begins with the judgements A : prop and B : prop. These judgements could also be included in the demonstration as hypotheses, namely by placing them to the left of $\vdash$. Here we rather choose to regard these judgements as given. We may think of an interlocutor who has taken responsibility for these judgements, A : prop and B : prop, and consider it to be our task to make evident each of $A \supset (B \supset A)$ true, $(A \land B) \supset (A \lor B)$ true, and $\neg(A \lor B) \supset \neg A$ true.<fnref n="43" />

a)

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

b)

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

There is a similar demonstration having as conclusion

$$ \lambda x. j(\mathbf{snd}(x)) : (A \land B) \supset (A \lor B). $$

c)

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

<footnote n="43">⁴³ This dialogical view on demonstration has been developed in some recent lectures of Per Martin-Löf. This proposal, as communicated by Prof. Sundholm to the group of dialogicians in Lille, is one of the main motivations for the research documented in the following chapters of this book.</footnote>
$$ \lambda y. \lambda x. \mathbf{ap}(y, \mathbf{i}(x)) : \neg(A \lor B) \supset \neg A $$

2. Here we shall use the natural deduction style of presenting demonstrations. That means that we shall not exhibit the hypotheses, but take these to be implicitly understood. The reader may want to supply the missing hypotheses.

a) To save space we shall write **p** instead of **fst** and **q** instead of **snd**.

$$ \begin{array}{ccc} & y : (\exists x : D)(A \land B) & y : (\exists x : D)(A \land B) \\ \begin{array}{c} y : (\exists x : D)(A \land B) \\ \hline \mathbf{p}(y) : D \end{array} & \begin{array}{c} \mathbf{q}(y) : (A \land B)[\mathbf{p}(y)] \\ \hline \mathbf{p}(\mathbf{q}(y)) : A[\mathbf{p}(y)] \end{array} & \begin{array}{c} y : (\exists x : D)(A \land B) \\ \hline \mathbf{q}(y) : A \land B[\mathbf{q}(y)] \\ \hline \mathbf{p}(y) : D \end{array} \\ & <\mathbf{p}(y), \mathbf{p}(\mathbf{q}(y))> : (\exists x : D)A & <\mathbf{p}(y), \mathbf{q}(\mathbf{q}(y))> : (\exists x : D)B \\ \cline{3-3} & <<\mathbf{p}(y), \mathbf{p}(\mathbf{q}(y))>, <\mathbf{p}(y), \mathbf{q}(\mathbf{q}(y))>> : (\exists x : D)A \land (\exists x : D)B & \end{array} $$

b)

$$ \begin{array}{ccc} & z : (\forall x : D)(A \land B) & x : D \\ \begin{array}{c} z : (\forall x : D)(A \land B) \\ \hline \mathbf{ap}(z, x) : A \land B \end{array} & \begin{array}{c} z : (\forall x : D)(A \land B) \\ \hline \mathbf{ap}(z, x) : A \land B \end{array} & \begin{array}{c} x : D \\ \hline \mathbf{ap}(z, x) : A \land B \end{array} \\ \begin{array}{c} \mathbf{fst}(\mathbf{ap}(z, x)) : A \\ \hline \lambda x. \mathbf{fst}(\mathbf{ap}(z, x)) : (\forall x : D)A \end{array} & \begin{array}{c} \mathbf{snd}(\mathbf{ap}(z, x)) : B \\ \hline \lambda x. \mathbf{snd}(\mathbf{ap}(z, x)) : (\forall x : D)B \end{array} & \begin{array}{c} \mathbf{x} : D \\ \hline \mathbf{x} : D \end{array} \\ & <\lambda x. \mathbf{fst}(\mathbf{ap}(z, x)), \lambda x. \mathbf{snd}(\mathbf{ap}(z, x))> : (\forall x : D)A \land (\forall x : D)B \\ & \lambda z. <\lambda x. \mathbf{fst}(\mathbf{ap}(z, x)), \lambda x. \mathbf{snd}(\mathbf{ap}(z, x))> : (\forall x : D)(A \land B) \supset ((\forall x : D)A \land (\forall x : D)B) & \end{array} $$

c) In the solution to this exercise we use both Σ-elimination and +-elimination. To save space we define **Dis** = (∃x : D)A ∨ (∃x : D)B : **prop**.

$$ \begin{array}{ccc} & x : D & v : A \\ \begin{array}{c} x : D \\ \hline <x, v> : (\exists x : D)A \end{array} & \begin{array}{c} x : D \\ \hline <x, v> : (\exists x : D)B \end{array} & \begin{array}{c} v : A \\ \hline <x, v> : (\exists x : D)A \end{array} \\ \begin{array}{c} y : A \lor B \\ \hline \mathbf{i}(<x, v>) : \mathbf{Dis} \end{array} & \begin{array}{c} \mathbf{j}(<x, v>) : \mathbf{Dis} \\ \hline \mathbf{j}(<x, v>) : \mathbf{Dis} \end{array} & \begin{array}{c} \mathbf{v}(<x, v>) : \mathbf{Dis} \\ \hline \mathbf{v}(<x, v>) : \mathbf{Dis} \end{array} \\ & <\exists x : D>(A \lor B) & \begin{array}{c} \mathbf{D}(y, v. \mathbf{i}(<x, v>), w. \mathbf{j}(<x, w>)) : \mathbf{Dis} \\ \hline \mathbf{E}(z, xy. \mathbf{D}(y, v. \mathbf{i}(<x, v>), w. \mathbf{j}(<x, w>))) : \mathbf{Dis} \end{array} \end{array} $$

Note that since A and B are propositional functions over D, the judgement v : A is made in the context x : D, v : A; the judgement w : B is made in the context x : D, w : B; and the judgement y : A ∨ B is made in the context x : D, y : A ∨ B. The variables w and v get bound by the application of **D**, whereas x and y get bound by the application of **E**.

3. Again we use the natural deduction style of presenting demonstrations.
<figure><img src="image_7.png" /></figure>

4. The important observation is that the classes A, B and C are defined over a universe of discourse. The universe of discourse is made explicit in CTT. Thus we let $D$: **set** and we let A, B and C be propositional functions over D, that is, we assume $x$: $D \vdash A$: **prop**, $x$: $D \vdash B$: **prop**, and $x$: $D \vdash C$: **prop**. That all A's are B is *not* formalized as $(\forall x: D)(A \supset B)$. This proposition says that all D's have property of being "B-if-A". The formalization is rather $(\forall z: (\exists x: D)A)B[fst(z)]$. A **set** of the form $(\exists x: D)A$ may be understood as formalizing the idea of "the D's such that A" or "the D's that are A" (Ranta, 1995, p. 61-64). The proposition $(\forall z: (\exists x: D)A)B[fst(z)]$ can therefore be understood as expressing that all the D's that are A are B. Since B is a propositional function over D, $B[fst(z)]$ is a family over $(\exists x: D)A$ in the variable z. The formalization, then, is as follows.

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

Assume now that we are given

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

To save space we define

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

We construct a proof of $(\forall z: (\exists x: D)A)C[fst(z)]$ as follows.

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

5. Again we must be careful to remember the universe of discourse. Hence, when we say that everything is an A, we mean that everything in the universe of discourse is an A. We have the following formalization. We assume $D$: **set**, $x$: $D \vdash A$: **set**, and $x$: $D \vdash B$: **set**.
$$ (\forall x : D)A \text{ true} $$

$$ (\forall z : (\exists x : D)A)B[\text{fst}(z)] \text{ true} $$

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

$$ \therefore (\forall x : D)B \text{ true} $$

Now assume

$$ q : (\forall x : D)A $$

$$ p : (\forall z : (\exists x : D)A)B[\text{fst}(z)] $$

We construct a proof of $(\forall x : D)B$ as follows. We use $\mathbf{P}$ as in the previous exercise.

$$ q : (\forall x : D)A \qquad x : D $$

$$ x : D \qquad \mathbf{ap}(q, x) : A $$

$$ p : \mathbf{P} \qquad \langle x, \mathbf{ap}(q, x) \rangle : (\exists x : D)A $$

$$ \mathbf{fst}(\langle x, \mathbf{ap}(q, x) \rangle) = x : D $$
$$ B[\mathbf{fst}(\langle x, \mathbf{ap}(q, x) \rangle)] = B : \mathbf{set} $$

$$ \mathbf{ap}(p, \langle x, \mathbf{ap}(q, x) \rangle) : B[\mathbf{fst}(\langle x, \mathbf{ap}(q, x) \rangle)] $$

$$ \mathbf{ap}(p, \langle x, \mathbf{ap}(q, x) \rangle) : B $$

$$ \lambda x. \mathbf{ap}(p, \langle x, \mathbf{ap}(q, x) \rangle) : (\forall x : D)B $$

Note here the use of the extensionality of substitution into sets as well as the use of the principle that we can infer $a : B$ from $a : A$ and $A = B : \mathbf{set}$. We rely on the syntactic identity $B[x] \equiv B$.

6. We apply **Id-elimination**.

$$ x : A \vdash \mathbf{ap}(c, x) = \mathbf{ap}(c, x) : B $$

$$ p : \mathbf{Id}(A, a, a') \qquad x : A \vdash \mathbf{refl}(B, \mathbf{ap}(c, x)) : \mathbf{Id}(B, \mathbf{ap}(c, x), \mathbf{ap}(c, x)) $$

$$ \mathbf{J}(p, x.\mathbf{refl}(B, \mathbf{ap}(c, x))) : \mathbf{Id}(B, \mathbf{ap}(c, a), \mathbf{ap}(c, a')) $$

$$ \lambda p. \mathbf{J}(p, x) : \mathbf{Id}(A, a, a') \supset \mathbf{Id}(B, \mathbf{ap}(c, a), \mathbf{ap}(c, a')) $$

An alternative demonstration is the following.

$$ x : A \vdash \mathbf{ap}(c, x) = \mathbf{ap}(c, x) : B $$

$$ x : A \vdash \mathbf{refl}(B, \mathbf{ap}(c, x)) : \mathbf{Id}(B, \mathbf{ap}(c, x), \mathbf{ap}(c, x)) $$

$$ x : A, p : \mathbf{Id}(A, x, x) \vdash \mathbf{refl}(B, \mathbf{ap}(c, x)) : \mathbf{Id}(B, \mathbf{ap}(c, x), \mathbf{ap}(c, x)) $$

$$ q : \mathbf{Id}(A, a, a') \qquad x : A \vdash \lambda p. \mathbf{refl}(B, \mathbf{ap}(c, x)) : \mathbf{Id}(A, x, x) \supset \mathbf{Id}(B, \mathbf{ap}(c, x), \mathbf{ap}(c, x)) $$

$$ \mathbf{J}(q, x.\lambda p.\mathbf{refl}(B, \mathbf{ap}(c, x))) : \mathbf{Id}(A, a, a') \supset \mathbf{Id}(B, \mathbf{ap}(c, a), \mathbf{ap}(c, a')) $$

7. We apply **Id-elimination** twice.

$$ p : \mathbf{Id}(A, a, a') \qquad x : A, y : B \vdash \mathbf{refl}(A \times B, \langle x, y \rangle) : \mathbf{Id}(A \times B, \langle x, y \rangle, \langle x, y \rangle) $$

$$ q : \mathbf{Id}(B, b, b') \qquad y : B \vdash \mathbf{J}(p, x.\mathbf{refl}(\langle x, y \rangle)) : \mathbf{Id}(A \times B, \langle a, y \rangle, \langle a', y \rangle) $$

$$ \mathbf{J}(q, y.\mathbf{J}(p, x.\mathbf{refl}(\langle x, y \rangle))) : \mathbf{Id}(A \times B, \langle a, b \rangle, \langle a', b' \rangle) $$
8. a) We apply **bool-elimination** with **Id(bool, x, t) ∨ Id(bool, x, f)** as our C. Hence we need a proof-object of **Id(bool, t, t) ∨ Id(bool, t, f)** and a proof-object of **Id(bool, f, t) ∨ Id(bool, f, f)**. These are constructed as follows.

$t: \mathbf{bool}$

$\mathbf{refl}(t) : \mathbf{Id}(\mathbf{bool}, t, t)$

$\mathbf{i}(\mathbf{refl}(t)) : \mathbf{Id}(\mathbf{bool}, t, t) \lor \mathbf{Id}(\mathbf{bool}, t, f)$

$f: \mathbf{bool}$

$\mathbf{refl}(f) : \mathbf{Id}(\mathbf{bool}, f, f)$

$\mathbf{j}(\mathbf{refl}(f)) : \mathbf{Id}(\mathbf{bool}, f, t) \lor \mathbf{Id}(\mathbf{bool}, f, f)$

Continuing the demonstration, we write the three premises of **bool-elimination** below each other.

$x: \mathbf{bool}$

$\mathbf{i}(\mathbf{refl}(t)) : \mathbf{Id}(\mathbf{bool}, t, t) \lor \mathbf{Id}(\mathbf{bool}, t, f)$

$\mathbf{j}(\mathbf{refl}(f)) : \mathbf{Id}(\mathbf{bool}, f, t) \lor \mathbf{Id}(\mathbf{bool}, f, f)$

$\mathbf{if} \ x \ \mathbf{then} \ \mathbf{i}(\mathbf{refl}(t)) \ \mathbf{else} \ \mathbf{j}(\mathbf{refl}(f)) : \mathbf{Id}(\mathbf{bool}, x, t) \lor \mathbf{Id}(\mathbf{bool}, x, f)$

$\lambda x. \mathbf{if} \ x \ \mathbf{then} \ \mathbf{i}(\mathbf{refl}(t)) \ \mathbf{else} \ \mathbf{j}(\mathbf{refl}(f)) : (\forall x: \mathbf{bool})(\mathbf{Id}(\mathbf{bool}, x, t) \lor \mathbf{Id}(\mathbf{bool}, x, f))$

b) In this solution, we sometimes omit parentheses and write, for instance, $sx$ instead of $s(x)$. We aim to apply $\mathbb{N}$-elimination with $\mathbf{Id}(\mathbb{N}, x, 0) \lor (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, x, sy)$ as our C. Hence we need a proof-object $d$ of $\mathbf{Id}(\mathbb{N}, 0, 0) \lor (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, 0, sy)$ and a function $e$ which, given a proof-object

$w : \mathbf{Id}(\mathbb{N}, x, 0) \lor (\exists y : \mathbb{N})\mathbf{Id}(\mathbb{N}, x, y)$

yields a proof-object

$e[w] : \mathbf{Id}(\mathbb{N}, sx, 0) \lor (\exists y : \mathbb{N})\mathbf{Id}(\mathbb{N}, sx, y)$

The proof-object $d$ is easily constructed.

$0: \mathbb{N}$

$\mathbf{refl}(0) : \mathbf{Id}(\mathbb{N}, 0, 0)$

$\mathbf{i}(\mathbf{refl}(0)) : \mathbf{Id}(\mathbb{N}, 0, 0) \lor (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, 0, sy)$

To find the function $e$ requires more work. Since we are given

$w : \mathbf{Id}(\mathbb{N}, x, 0) \lor (\exists y : \mathbb{N})\mathbf{Id}(\mathbb{N}, x, y)$

it is natural to try to construct $e[w]$ by means of $\lor$-elimination. Assume, therefore, first that we are given $q: \mathbf{Id}(\mathbb{N}, x, 0)$.

$q: \mathbf{Id}(\mathbb{N}, x, 0)$

$\mathbf{refl}(sz) : \mathbf{Id}(\mathbb{N}, sz, sz)$

$\mathbf{J}(q, z.\mathbf{refl}(sz)) : \mathbf{Id}(\mathbb{N}, sx, s0)$

$<0, \mathbf{J}(q, z.\mathbf{refl}(sz))> : (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, sx, sy)$

$\mathbf{j}<0, \mathbf{J}(q, z.\mathbf{refl}(sz))> : \mathbf{Id}(\mathbb{N}, sx, 0) \lor (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, sx, sy)$

Next assume that we are given $p: (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, x, sy)$.

$p: (\exists y: \mathbb{N})\mathbf{Id}(\mathbb{N}, x, sy)$
$$ \mathit{sndp} : \mathit{Id}(\mathbb{N}, x, s(fstp)) $$

$$ \mathit{refl}(sz) : \mathit{Id}(\mathbb{N}, sz, sz) $$

$$ \mathbf{J}(\mathit{sndp}, z.\mathit{refl}(sz)) : \mathit{Id}(\mathbb{N}, sx, ss(fstp)) $$

$$ <s(fstp), \mathbf{J}(\mathit{sndp}, z.\mathit{refl}(sz))> : (\exists y : \mathbb{N})\mathit{Id}(\mathbb{N}, sx, sy) $$

$$ j<s(fstp), \mathbf{J}(\mathit{sndp}, z.\mathit{refl}(sz))> : \mathit{Id}(\mathbb{N}, sx, 0) \lor (\exists y : \mathbb{N})\mathit{Id}(\mathbb{N}, sx, sy) $$

With $w : \mathbf{Id}(\mathbb{N}, x, 0) \lor (\exists y : \mathbb{N})\mathbf{Id}(\mathbb{N}, x, sy)$ as major premiss, $\lor$-elimination then yields

$$ \mathbf{D}(w, q.j<0, \mathbf{J}(q, z.\mathit{refl}(sz)), p.j<s(fstp), \mathbf{J}(\mathit{sndp}, z.\mathit{refl}(sz))> : $$

$$ \mathit{Id}(\mathbb{N}, sx, 0) \lor (\exists y : \mathbb{N})\mathit{Id}(\mathbb{N}, sx, sy) $$

With the assumption $x : \mathbb{N}$ as major premiss, $\mathbb{N}$-elimination yields

$$ \mathbf{R}(x, i(\mathit{refl0}), w.\mathbf{D}(w, q.j<0, \mathbf{J}(q, z.\mathit{refl}(sz)), p.j<s(fstp), \mathbf{J}(\mathit{sndp}, z.\mathit{refl}(sz))>) : $$

$$ \mathit{Id}(\mathbb{N}, x, 0) \lor (\exists y : \mathbb{N})\mathit{Id}(\mathbb{N}, x, sy) $$

Note that $w$ has become bound here, so only $x$ is free. A proof-object of

$$ (\forall x : \mathbb{N})(\mathit{Id}(\mathbb{N}, x, 0) \lor (\exists y : \mathbb{N})\mathit{Id}(\mathbb{N}, x, sy)) $$

is then constructed by means of $\Pi$-introduction.
### III. BASIC NOTIONS FOR DIALOGICAL LOGIC

The dialogical approach to logic is not a specific logical system; it is rather a general framework having a rule-based approach to meaning (instead of a truth-functional or a model-theoretical approach) which allows different logics to be developed, combined and compared within it. The main philosophical idea behind this framework is that meaning and rationality are constituted by argumentative interaction between epistemic subjects; it has proved particularly fruitful in history of philosophy and logic. We shall here provide a brief overview of dialogues in a more intuitive approach than what is found in the rest of the book in order to give a feeling of what the dialogical framework can do and what it is aiming at.

#### III.1 The general framework

##### Dialogues and interaction

As hinted by its name, this framework studies dialogues; but it also takes the form of dialogues. In a dialogue, two parties (players) argue on a thesis (a certain statement that is the subject of the whole argument) and follow certain fixed rules in their argument. The player who states the thesis is the Proponent, called *P*, and his rival, the player who challenges the thesis, is the Opponent, called *O*. By convention, we refer to *P* as he and to *O* as she. In challenging the Proponent's thesis, the Opponent is requiring of the Proponent that he defends his statement.

The interaction between the two players *P* and *O* is spelled out by challenges and defences, implementing Robert Brandom's take on meaning as a game of giving and asking for reasons (see the introduction, section I.2). Actions in a dialogue are called moves; they are often understood as speech-acts involving declarative utterances (*statements*) and interrogative utterances (*requests*).<fnref n="44" /> The rules for dialogues thus never deal with expressions isolated from the act of uttering them.

The rules in the dialogical framework are divided into two kinds of rules: particle rules, and structural rules.

###### Particle rules

Particle rules (*Partikelregeln*), or rules for logical constants, determine the legal moves in a play and regulate interaction by establishing the relevant moves constituting *challenges*: moves that are an appropriate attack to a previous move (a statement) and thus require that the challenged player play the appropriate defence to the attack. If the challenged player defends his statement, he has answered the challenge.

Particle rules determine how reasons are asked for and are given for each kind of statement, thus providing the meaning of that statement. In other words, the appropriate attacks and defences—that is, the appropriate ways of asking for and giving reasons—for

<footnote n="44">⁴⁴ Litterature pertaining to the dialogical framework also uses the terms posits and assertions to designate what we will here call statements, that is, the act of stating a proposition within a game of giving and asking for reasons; the meaning of a statement is defined by an appropriate challenge and defence, or, in other words, how reasons for this statement can be requested, what constitutes reasons for this statement and how these reasons can be provided.</footnote>
each statement (or move) gives the meaning of these statements: a conjunction, a disjunction, or a universal quantification, for instance, receive their meaning through the appropriate interaction in a dialogical game, spelled out by the particle rules.

The particle rules provide the meaning of the different logical connectives, which they provide in a dynamic way through appropriate challenges and answers. This feature of dialogues is fundamental for immanent reasoning: the meaning of the moves in a dialogue does not lie in some external semantic, but is immanent to the dialogue itself,<fnref n="45" /> that is, in the specific and appropriate way the players interact; we here join the Wittgensteinian conception of meaning as use. The particle rules are spelled out in an anonymous way, that is, without mentioning if it is **P** or **O** who is attacking or defending: the rules are the same for the two players; the meaning of the connectives is therefore independent of who uses them.<fnref n="46" />

An essential aspect of the meaning of logical constants in the dialogical framework pertains to the actions, such as choices, the particle rules associate to the use of such constants. In this regard, since the interaction constitutes the meaning, all the actions involved in the constitution of the meaning of an expression should be made explicit; — otherwise part of the meaning would be left implicit. These essential aspects must therefore be part of the object language in order to figure explicitly. This is the main reason for importing in the dialogical framework many Constructive Type Theory features (and will be presented in chapters VI-VII). The roots of this kind of perspective can be found in Wittgenstein's *Unhintergehbarkeit der Sprache*:<fnref n="47" /> language games are supposed to show this internal feature of meaning.

## Structural rules

Structural rules (*Rahmenregeln*) on the other hand determine the general course of a dialogue game, such as how a game is initiated, how to play it, how it ends, and so on. The point of these rules is not so much to spell out the meaning of the logical constants by specifying how to act in an appropriate way—this is the role of the particle rules—; it is rather to specify according to what structure interactions will take place. It is one thing to determine the meaning of the logical constants as a set of appropriate challenges and defences, it is another to define whose turn it is to play and when a player is allowed to play a move. One could thus have the same local meaning and change a structural rule, saying for instance that one of the players is allowed to play two moves at a time instead of simply one: this would considerably change the game without changing the local meaning of what is said.

One of the most important structural rules for the present study on immanent reasoning is the Copy-cat rule (or Socratic rule when introducing CTT features in the

<footnote n="45">⁴⁵ Göran Sundholm (1997; 2001) voiced some criticism against metalogical frameworks for meaning: standard model-theoretic semantics convert semantics in a formal metamathematical object for which the syntax is linked to the meaning by attributing truth values to each sign that is uninterpreted (formula). The language thus does not express any content but is rather conceived as a system of signs *speaking of* the world, provided that a metalogical adequation between the signs and the world has been defined. For more on this issue, see section VI.</footnote>

<footnote n="46">⁴⁶ In this sense, the particle rules are said to be *symmetric*, see section IV.3. This is imperative to preserve the dialogical framework from connectives as Prior’s (1960) *tonk*. See (Redmond & Rahman, 2016).</footnote>

<footnote n="47">⁴⁷ This is a Wittgensteinian principle that Hintikka explicitely adopted. The reasons for linking the dialogical framework to CTT, allowing a greater explicitation of the meaning in the object-language, are thus analogous to Hintikka’s vindication for the fecundity of game-theoretic semantics (GTS) in the epistemic framework for logic, semantics, and the foundations of mathematics.</footnote>
dialogical context). This rule is not anonymous, it is a restriction on the moves the Proponent is allowed to play: the Proponent is allowed to assert an elementary judgement only if the Opponent has already asserted it. So the Opponent is not concerned by the same exact rules as the Proponent.

The Copy-cat rule accounts for analyticity: the Proponent, who brings forward the thesis, will have to defend it without bringing any element of his own in the play: his defence of the thesis will have to rely only on what the Opponent has conceded, and everything the Opponent concedes comes only from the meaning of the thesis. The Opponent will be challenging the thesis, and challenging and defending the subsequent moves made by the Proponent in reaction to her initial challenge of the thesis; but all these challenges and defences are made according to the particle rules. So everything the Opponent will concede during a play stems from an application of the particle rules starting with the thesis. The only elements whose meaning is left unspecified, in formal plays, are the elementary statements (specifying their meaning is the point of material plays, see chapter X). The Copy-cat rule makes sure that the Proponent is not bringing in any elementary statement to back his thesis that the Opponent might not agree with: the Proponent can only back his thesis with elementary statements that the Opponent herself has already conceded.

## III.2 The rules at the play level

### III.2.1 Particle rules

Here are the particle rules for propositional logic in a standard framework. We use anonymous players, X and Y, so that the meaning of the logical constants stays player-independent. The exclamation mark after the player indicates that the player states the following proposition (utterance), the question mark indicates that the player is making a request.

**Conjunction : X ! A ∧ B**

The meaning of logical constants are not defined in the dialogical framework by their truth-values, but by the appropriate challenges and defences: a conjunction is a statement that is challenged by asking one of the two conjuncts, the choice lying with the challenger (Y). The challenge is answered by providing the conjunct asked, so the defender (X) does not have the choice in a conjunction:

* if the challenger asks for the left conjunct (Y ? L^) then the defender must provide the left conjunct (X ! A) to defend his initial conjunction;

* if the challenger asks for the left conjunct (Y ? R^) then the defender must provide the left conjunct (X ! B) to defend his initial conjunction.

<table><caption>Table 1: particle rules for conjunction</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Conjunction</th><td>X ! A ∧ B</td><td>Y ? L<sup>^</sup><br>or<br>Y ? R<sup>^</sup></td><td>X ! A<br>(respectively)<br>X ! B</td></tr></tbody></table>

**Properties of conjunction:**

* the challenge is a request;

* the challenger has the choice;

* the defender must provide the conjunct requested.
**Disjunction: $X!A \lor B$**

A disjunction is a statement that is challenged by asking one of the two disjuncts, but the challenger (Y) does not have the choice. The challenge is answered by providing either of the two disjuncts, the choice lying with the defender (X).

<table><caption>Table 2: particle rules for disjunction</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Disjunction</th><td>$X!A \lor B$</td><td>$Y?_v$</td><td>$X!A$<br>or<br>$X!B$</td></tr></tbody></table>

**Properties of disjunction:**

* the challenge is a request;

* the defender has the choice;

* the defender provides the disjunct he wants.

**Implication: $X!A \supset B$**

An implication is a statement that is challenged by stating the antecedent. The challenge is answered by stating the consequent. So to challenge an implication stated by the other player $X!A \supset B$, the challenger must state the antecedent $Y!A$; the defender must then state the consequent $X!B$.

Notice that by challenging an implication, the challenger himself is making a statement, which can be challenged if it is not elementary. Implication in this sense can be considered as distributing the burden of proof.

<table><caption>Table 3: particle rules for implication</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Implication</th><td>$X!A \supset B$</td><td>$Y!A$</td><td>$X!B$</td></tr></tbody></table>

**Properties of implication:**

* the challenge is the stating of the antecedent;

* the defence is the stating of the consequent;

* there is no choice involved.

**Negation: $X!\neg A$**

A negation is a statement that is challenged by stating the negated proposition ($Y!A$). It cannot be answered.

In the table presentation of dialogues, to distinguish the cells that are empty because the defence is still pending from the cells that will remain empty because a challenge on a negation cannot be defended, we insert the sign “—” in the cell for the defence of negation.

<table><caption>Table 4: particle rules for negation</caption><thead><tr><th></th><th>Move</th><th>Challenge</th><th>Defence</th></tr></thead><tbody><tr><th>Negation</th><td>$X!\neg A$</td><td>$Y!A$</td><td>—</td></tr></tbody></table>

**Properties of negation:**

* the challenge is the stating of the negated proposition;

* there is no defence;
* there is no choice involved.

## Summing up the particle rules for propositional classical logic

<table><caption>Table 5: particle rules</caption><thead><tr><th></th><th>Conjunction</th><th>Disjunction</th><th>Implication</th><th>Negation</th></tr></thead><tbody><tr><th>Move</th><td>X!A∧B</td><td>X!A∨B</td><td>X!A⊃B</td><td>X!¬A</td></tr><tr><th>Challenge</th><td>Y?L<sup>∧</sup><br>or<br>Y?R<sup>∧</sup></td><td>Y?<sub>v</sub></td><td>Y!A</td><td>Y!A</td></tr><tr><th>Defence</th><td>X!A<br>(resp.)<br>X!B</td><td>X!A<br>or<br>X!B</td><td>X!B</td><td>—</td></tr></tbody></table>

### III.2.2 Structural rules

Here are the structural rules for standard classical logic in the dialogical framework. They define how a play unravels, that is how a statement (the thesis) can generate a certain dialogue. There are four basic structural rules (SR) specifying: 1. how to start; 2. how to play; 3. how to preserve formality (Copy-cat rule); 4. how to win.

Each of these rules can be modified, producing variants in the dialogical framework: adding for instance a condition on 3—called “last duty first”—will yield intuitionistic logics. Some variants will be introduced in the next section for more advanced dialogues.

#### SR 1: starting the play

A play starts with a player stating a proposition called the *thesis*; that player becomes the Proponent (P) and the move is labelled move 0.

The other player—the Opponent (O)—chooses a *repetition rank* determining how many times she is allowed to challenge or defend any move in a play. It is usually enough for O to choose a repetition rank of 1 ($m := 1$), it is move 1.

P then chooses a repetition rank: 2 is usually enough ($n := 2$); it is move 2.

#### SR 2: how to play

Each player in turn plays one move: once the repetition ranks have been chosen, each move is either a challenge on a previous statement or a defence of a previous challenge.

#### SR 3: Copy-cat rule

P cannot play an elementary statement if O has not stated it previously.

#### SR 4: winning rule

The play ends when it is a player's turn to make a move but that player has no available move left. That player loses, the other player wins.
### III.3 Building a dialogue: step-by-step instructions

#### Setting up the game

In order to build a dialogue, first start with a large table with two columns, one for the Opponent (on the left) and one for the Proponent (on the right).

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

Add a column:

* on the *outer side* of your two columns (A cells); this column will specify the number of the move played;

* on the *inner side* of your two columns (B cells); this column will specify the number of the move challenged, if applicable.

<table><thead><tr><th>O</th><th>P</th></tr></thead><tbody><tr><td>A</td><td>B B</td><td>A</td></tr><tr><td>A</td><td>B B</td><td>A</td></tr></tbody></table>

Write the *thesis* as **P**'s first move, that is move 0 (see the structural rule for initializing the play, SR0).

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

Each player (**O** first, then **P**) now choose their repetition rank. For convenience, we usually choose rank 1 for **O** and rank 2 for **P**.<fnref n="48" /> Repetition ranks determine how many times a player is allowed to attack or to defend each and every move.

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

#### Playing the game

* Each player *in turn* will play a move,<fnref n="49" /> that is, he will either *attack* a move made by the other player, or *defend* against an attack.

* If the player attacks: write the attack *on a new line*, and specify the number of the attacked move in the inner column.<fnref n="50" />

<footnote n="48">⁴⁸ These ranks are enough for propositional logic: **P** can attack the two sides of a conjunction and defend the two sides of a disjunction. If the players are playing at their best (no mistakes), then 1 is enough for **O**: if she has a move allowing her to win, she will choose it straightaway.</footnote>

<footnote n="49">⁴⁹ Since the players will play alternately, all of **O**'s moves will be *uneven* numbers, whereas all of **P**'s moves will be *even* numbers. There are no exceptions.</footnote>

<footnote n="50">⁵⁰ Expressions are not listed by following the order of the moves, but by writing an attack on a new line and the defence on the same line as the corresponding attack, thus showing when a challenge is answered.</footnote>
Elementary statements cannot be attacked.<fnref n="51" />

* If the player defends: write the defence on the same line as the attack.

An attack on a negation cannot be defended, though the player can attack or defend some other move, if there are any available.

## Ending the game

A play stops when one of the two players has no move left (attack or defence).

In order to be sure that every possible move has been played, ask yourself, for the player whose turn it is to play:

* if there are any non-elementary statements played by the adversary that has not been attacked (or that has been attacked only once if the repetition rank is 2).

If there are, then the player can attack it (except if there is a restriction by the Copy-cat rule).

* If there are any attacks left undefended (or defended only once if the repetition rank is 2). You can see this easily by the empty case in the player's column. Remember: attacks on negations cannot be defended, so cells with "—" are left empty.

If it is a player's turn and everything that could be attacked has already been attacked, and everything that could be defended has already been defended, then, and then only, has the play ended and that player has lost.

## III.4 Commented construction of a play: $(A \land B) \supset A$

The thesis to be tested will be $(A \land B) \supset A$.

0. The play starts with the Proponent (P) stating the thesis. It is move 0.

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

1. It is now the Opponent's (O's) turn to play. She must choose her repetition rank, that is, the number of times she can attack or defend any move. We will in general use a repetition rank of 1 ($m := 1$) for O, and of 2 ($n := 2$) for P.

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

2. Now it is P's turn to choose his repetition rank.

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

<footnote n="51">⁵¹ This would bring us into material plays. See the introduction, section I.2 and chapter **错误!** Source du renvoi introuvable..</footnote>
<table><tr><td></td><td></td><td></td><td></td></tr></table>

3. It is O's turn, and she has only one available move: attacking the thesis (move 0). Since it is an implication, she must state the antecedent ($A \land B$).

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

4. P has two available moves: either he defends his thesis against O's challenge (move 3), or he attacks O's move 3.

O's challenge being on an implication, the defence must be to state the consequent, here A. But A is an elementary statement, so P is not allowed to state A if O has not played it beforehand—according to the Copy-cat (structural) rule. So P cannot defend his thesis (move 0) as long as he has not found a way of making O assert A.

P must therefore attack. His move is written on a new line (each new challenge is written on a new line, so that the corresponding defence can be written on the same line: at a glance one should see if challenges are left unanswered).

P has to challenge O's move 3 which is a conjunction. So P has the choice as to which of the conjuncts to ask for. Since P wants to be able to defend his thesis, he chooses to ask for the first conjunct.

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

5. It is now O's turn to play, and she has only one available move: she must defend her conjunction (move 3) from P's challenge (move 4).

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

6. Since O has stated A, P is now allowed to state A: he can defend his thesis (move 0) against O's still unanswered challenge (move 3).

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

7. It is now **O**'s turn, but she has no available move: every **P**-challenge has been answered and every non-elementary statement of **P** has been challenged. Therefore the play is over and **O** has lost.

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

**P** wins.

## Exercises

Build a play for the following theses:

1. $(A \lor B) \supset (B \lor A)$

2. $A \lor \neg A$

3. $\neg\neg A \supset A$

4. $\neg\neg(A \lor \neg A)$

## Solutions

The solution for 1 is given in the next section (III.5) as the first step in building a winning strategy.

The other solutions are given as examples at the end of the next chapter (IV). See the following passages:

* p. 71 for the third excluded: $A \lor \neg A$;

* p. 72 for the double negation elimination: $\neg\neg A \supset A$;

* p. 73 for the double negation of the third excluded: $\neg\neg(A \lor \neg A)$.

The examples in the next section compare the intuitionistic (structural) rules and the classical ones; in this section we have only presented the classical (structural) rules.

## III.5 Approaching the strategy level

Up to now we have only looked at individual plays; that is, we have stayed at the play level, which is a distinctive feature of the dialogical framework. The strategy level on the other hand converges with other logical frameworks, for a winning strategy can be turned into a demonstration in a non-dialogical framework (and reversely): such an algorithm will be provided in chapter IX.

The strategy level allows to compare different plays on the same thesis. A winning strategy is always defined in relation to a specific player, either **O** or **P**, though it must be noted that *strategies* are not actually carried out by the players, they are only a *perspective* on the possible plays for a given thesis. Usually (and by default), we consider **P**-winning strategies. A **P**-winning strategy determines if **P** has a way to win a play regardless of **O**'s choices during the play: whatever be **O**'s choice, **P** will be able to
find a way to win. **P**-strategies are therefore built on **O**'s choices: each possible choice of **O** must be taken into account and dealt with in order to determine if **P** is able to win in all the different cases stemming from **O**'s possible choices.

A **P**-strategy is constructed first like a normal play, which must end with **P** winning (otherwise we will not be constructing a **P**-winning strategy). Then we proceed from the last move up to the first move and we stop when we come across a choice made by **O**. At that point, we branch the play: on the first branch we leave the initial play and on the second branch we do as if **O** had chosen her other option at that point, that is with exactly the same previous moves of the play. This play also needs to be won by **P** in order to continue building the **P**-strategy. We then proceed again by going up the moves until we find another **O**-choice and make another branching, up to the thesis. Once all of **O**'s choices have been dealt with, we can determine whether or not **P** has a winning strategy for this thesis: if somewhere **O** won a play, then **O** has a way of playing that will allow her to win; but if for each and every choices of **O**, **P** has a way to play allowing him to win, he has a winning strategy. Winning strategies are analogous in chess to saying "checkmate in *x* moves": whatever the opponent will play, the other player has a way to win in maximum *x* moves.

With the particle rules given in this didactic section, **O** has a choice only when:

* Challenging a conjunction and

* Defending a disjunction.

## Building a P-winning strategy step-by-step

In order to illustrate how to build a winning strategy, let us consider the thesis $P!(A \lor B) \supset (A \lor B)$.

1. First build a play for this thesis.

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td>!(A ∨ B) ⊃ (A ∨ B)</td><td>0</td></tr><tr><td>3</td><td>! A ∨ B</td><td>0</td><td>$n := 2$</td><td>2</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td>! A ∨ B</td><td>4</td></tr><tr><td>7</td><td>! A</td><td></td><td>! A</td><td>8</td></tr><tr><td></td><td></td><td>3</td><td>?<sub>v</sub></td><td>6</td></tr></tbody></table>

**P** wins.

2. Proceed backwards from the last move up and stop at the first **O** choice encountered.

<table><thead><tr><th></th><th>O</th><th></th><th>P</th><th></th></tr></thead><tbody><tr><td>1</td><td>$m := 1$</td><td></td><td>!(A ∨ B) ⊃ (A ∨ B)</td><td>0</td></tr><tr><td>3</td><td>! A ∨ B</td><td>0</td><td>$n := 2$</td><td>2</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td>! A ∨ B</td><td>4</td></tr><tr><td>7</td><td>! A</td><td></td><td>! A</td><td>8</td></tr><tr><td></td><td></td><td>3</td><td>?<sub>v</sub></td><td>6</td></tr></tbody></table>

**P** wins.

Here it is move 7, in which **O** had a choice because she had to defend a disjunction. The other option that was available to her was to choose the other disjunct, **O**!**B**. We need to branch the plays so that both options are considered. We therefore copy the play up to move 7 and leave this move blank; we draw two branches and copy the first play on one branch and continue the other play with move 7 being the other option, that is **O**!**B**.
<table><caption>Play 1: left option</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!(A ∨ B) ⊃ (A ∨ B)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>! A ∨ B</td><td>0</td><td>4</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td></td></tr><tr><td>7</td><td></td><td>3</td><td>?<sub>v</sub></td></tr></tbody></table>

<table><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!(A ∨ B) ⊃ (A ∨ B)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>! A ∨ B</td><td>0</td><td>4</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td>8</td></tr><tr><td>7</td><td>! A</td><td>3</td><td>?<sub>v</sub></td></tr></tbody></table>

P wins

<table><caption>Play 2: right option</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!(A ∨ B) ⊃ (A ∨ B)</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr><tr><td>3</td><td>! A ∨ B</td><td>0</td><td>4</td></tr><tr><td>5</td><td>?<sub>v</sub></td><td>4</td><td>8</td></tr><tr><td>7</td><td>! B</td><td>3</td><td>?<sub>v</sub></td></tr></tbody></table>

P wins.

3. Proceed backwards: we fall on the thesis without any other O-choice; so we have considered all the relevant cases for a P strategy. Since P can win in every case, P has a winning strategy for $(A \lor B) \supset (A \lor B)$.

## Exercise

Build a P-winning strategy for the following thesis, with the repetitions ranks O
$m := 1$ and P $m := 2$:

$$1. ((A \lor B) \land \neg A) \supset B$$

## Solution

The branching is here triggered by O's repetition rank $m := 1$: she cannot defend twice against the same attack (move 8), so her two options yield two different plays (play 2 and play 3) in which she chooses each time one of the two options (right option in play 2 and left option in play 3).

<table><caption>Play 1: $((A \lor B) \land \neg A) \supset B$</caption><thead><tr><th colspan="2">O</th><th colspan="2">P</th></tr></thead><tbody><tr><td></td><td></td><td>!( (A ∨ B) ∧ ¬A ) ⊃ B</td><td>0</td></tr><tr><td>1</td><td>m := 1</td><td>n := 2</td><td>2</td></tr></tbody></table>
<table><tr><td>3</td><td>! (A ∨ B) ∧ ¬A</td><td>0</td><td></td><td></td></tr><tr><td>5</td><td>!¬A</td><td></td><td>3</td><td>? R<sup>∧</sup></td><td>4</td></tr><tr><td>7</td><td>!A ∨ B</td><td></td><td>3</td><td>? L<sup>∧</sup></td><td>6</td></tr><tr><td></td><td></td><td></td><td>7</td><td>?<sub>V</sub></td><td>8</td></tr></table>

Play 2: right option

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

P wins (intuitionistic rules, see section IV.4.2, p. 69)

Play 3: left option

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

P wins (intuitionistic rules)

### III.6 Rounding up some key notions

Considering what has been said up to now, the following points are essential to the dialogical approach:

1. The distinction between *local* meaning (particle rules for logical constants) and *global* meaning (structural rules determining how to play).

2. The player independence of local meaning.

3. The distinction between the play level (local winning, or winning of a play) and the strategic level (existence of a winning strategy).

4. A notion of demonstration that amounts to building a winning strategy.

5. The distinction between *material* dialogues, *formal* dialogues that include a rule allowing Copy-cat moves, and dialogues combining both.
### III.7 Further reading

#### Textbook presentations

For a textbook presentation of the dialogical framework, see (Clerbout, 2014b), (Redmond & Fontaine, 2011) or (Rückert, 2011a).

#### Logical studies in dialogic

* The main original papers on the dialogical approach to logic are collected in (Lorenzen & Lorenz, 1978).

* For a historical overview of the transition from operative logic to dialogical logic see (Lorenz, 2001).

* For a presentation about the initial role of the dialogical framework as a foundation for intuitionistic logic, see (Felscher, 1985);

* for its bearings with argumentation theory and everyday dialogues see (Krabbe, 1982; 1985; 2006).

* Other papers have been collected more recently in (Lorenz, 2010a; 2010b).

* An account of developments since (Rahman, 1993) can be found in (Rahman & Keiff, 2005; 2010), (Keiff, 2007; 2009), (Beirlaen & Fontaine, 2016) and (Cardascia, 2016).

* For the underlying metalogic see (Clerbout, 2014a; 2014b; 2014c).

#### On the use of the dialogical framework in epistemology, philosophy and history of ideas

The dialogical framework has proven a powerful tool in logic, but it also has further ambitions: the fact that meaning in entirely provided by the interaction that makes a dialogue (even, in a large part, the material aspect of meaning; see chapter 1) and that this dialogical framework allows for multiple levels of consideration (the play level and the strategy level are the most important ones) makes this framework a very flexible and adaptable tool useful in history of philosophy, deontics, epistemology, and many other fields of inquiry that are not primarily logical. Here are a few studies showing the range of possible applications of the dialogical framework; many more are currently under progress, exploring the gamut of immanent reasoning.

* For the key role of the dialogical framework in linking dialectics, games, and logic, see (Rahman & Tulenheimo, 2009), (Rahman & Keiff, 2010) and (Marion & Rückert, 2015).

* (Clerbout, Gorisse, & Rahman, 2011) studied Jain Logic in the dialogical framework.

* (Popek, 2012) develops a dialogical reconstruction of medieval *obligationes*.

For other books see

* (Redmond, 2010) and (Rahman & Redmond, 2015) on fiction and the dialogical framework;

* (Fontaine, 2013) on intentionality, fiction, and dialogues;

* (Magnier, 2013) on dynamic epistemic logic and legal reasoning in a dialogical framework;

* and (Nzokou, 2013) on the dialogical framework and non-monotonic reasoning in legal debates within oral traditions.
# IV. ADVANCED DIALOGUES: PLAY LEVEL

This chapter will provide a more technical approach to the standard (non-CTT) dialogical framework at the play level. The next chapter (V) will do the same at the strategy level. It will then be possible to introduce local reasons in the dialogues and thus start making it explicit that dialogues are games of giving and asking for reasons;<fnref n="52" /> in this sense, the elements contributing to the meaning as use will appear in the object language. The link to equality in action will then be spelled out in the following two chapters (VI-VII), based on what will be presented in the next two chapters (IV-V).

In the previous chapter (III), we have introduced less formally the standard dialogical framework and have given step-by-step instructions as how to proceed in building a dialogue. We shall here be presenting the same material, but in a more technical way. First (section IV.1), we will provide some preliminary notions. Then (section IV.2) we will deal with local meaning (provided by the particle rules) with a more extended language than the propositional logic presented in the previous chapter. Third (section IV.3), we will expound briefly on the distinction between harmony at the global and the strategy level on the one hand, which defines dynamic identity, and a kind of harmony at the local level on the other hand, which we call symmetry and is player-independent, a feature essential to the particle rules. Then (section IV.4) we will provide the structural rules and the global meaning these rules convey, and provide different variants for games in this framework, giving in particular the rules for intuitionistic logic (as opposed to classical logic). Last (section IV.5), we will carry out three examples of plays and insist on the difference between classical and intuitionistic logic.

## IV.1 Preliminary notions

### The language

Let $L$ be a first-order language built as usual upon the propositional connectives, the quantifiers, a denumerable set of individual variables, a denumerable set of individual constants and a denumerable set of predicate symbols (each with a fixed arity).

We extend the language $L$ with two labels **O** and **P**, standing for the players of the game, and the two symbols ‘!’ and ‘?’ standing respectively for statements and requests. When the identity of the player does not matter, we use the variables **X** or **Y** (with $X \neq Y$).<fnref n="53" />

### Plays

A *play* is a legal sequence of moves, that is, a sequence of moves which observes the game rules. Particle rules are not the only rules which must be observed in this respect: the second kind of rules, the *structural rules*, are the rules providing the precise conditions under which a given sequence is a play.

<footnote n="52">⁵² This idea will remain implicit until then, appearing only when we stress that the particle rules as provide the meaning of logical constants through appropriate challenges and defences</footnote>

<footnote n="53">⁵³ This aspect (player independence) is fundamental for the symmetry of the rules. See section IV.3.</footnote>
# Dialogical games

The dialogical game for a statement is the set of all plays from a given thesis (initial statement, see below the Starting rule, SR0).

## A move in a play

A move $M$ is an expression of the form ‘X-e’, where $e$ is either

* of the form ‘! A’ (read: *the player X states A*), for some proposition $A$ of L; we say it is an elementary statement, or

* of one of the forms specified by the particle rules (see below).

## Challenges and defences

The words ‘attack’ and ‘defence’ are convenient to name certain moves according to their relation to other moves which can be defined in the following way.

* Let $\sigma$ be a sequence of moves. The function $\rho_\sigma$ assigns a position to each move in $\sigma$, starting with 0.

* The function $F_\sigma$ assigns a pair $[m, Z]$ to certain moves $M$ in $\sigma$, where $m$ denotes a position smaller than $\rho_\sigma(M)$ and $Z$ is either $A$ or $D$, standing respectively for ‘attack’ and ‘defence’. That is, the function $F_\sigma$ keeps track of the relations of attack and defence as they are given by the particle rules.

Let us point that at the local level (the level of the particle rules), this terminology should be bereft of any strategic undertone.

## Terminological note: challenge, attack and defence

The standard terminology uses the terms *challenge*, or *attack*, and *defence* (sometimes *answer* in respect of challenges). We shall here make a (subtle) distinction between challenge and attack: a challenge is initiated by an attack and needs this attack to be defended against in order to be answered to. So a challenge requires a defence to be settled, whereas an attack is simply the move that opens the challenge. For instance, using the particle rules exposed below, an attack on an implication will be simply to state the antecedent, and challenging an implication will be to attack it and thus demanding that the player who stated the implication defends her posit by positing the consequent, knowing that the challenger stated the antecedent. As one can see, the difference between challenge and attack is slim, and they may oftentimes be taken as synonymous.

# IV.2 Local meaning of logical constants

## Particle rules:

In the dialogical framework, the particle rules state the *local semantics*: only challenges and the corresponding defences for a given logical constant are at stake here, that is, we only take the main logical constant of the proposition into account.

Particle rules provide a decontextualized description of how the game can proceed locally: they specify the way a statement can be challenged and defended according to its main logical constant. In this way the particle rules govern the local level of meaning.

The table for the propositional connectives has already been presented in the previous