# An exegesis of transcendental syntax

Boris Eng

► To cite this version:

Boris Eng. An exegesis of transcendental syntax: A journey into the logical machinery. Logic in Computer Science [cs.LO]. Université Sorbonne Paris Nord, 2023. English. NNT: tel-04179276

HAL Id: tel-04179276

https://hal.science/tel-04179276

Submitted on 9 Aug 2023

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
# An Exegesis of Transcendental Syntax

## A journey into the logical machinery

*Thèse de doctorat pour le diplôme de*
*Docteur en informatique de l'Université Sorbonne Paris Nord*

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

Boris Eng

Thèse soutenue le 20 juin 2023 devant le jury composé de :

<table><tr><td>Thomas SEILLER</td><td>CNRS – Université Sorbonne Paris Nord</td><td>Directeur de thèse</td></tr><tr><td>Damiano MAZZA</td><td>CNRS – Université Sorbonne Paris Nord</td><td>Co-directeur de thèse</td></tr><tr><td>Lionel VAUX</td><td>Aix-Marseille Université</td><td>Rapporteur</td></tr><tr><td>Lorenzo TORTORA DE FALCO</td><td>Università Roma Tre</td><td>Rapporteur</td></tr><tr><td>Claudia FAGGIAN</td><td>CNRS – Université Sorbonne Paris Cité</td><td>Examinatrice</td></tr><tr><td>Jean-Baptiste JOINET</td><td>Université Lyon III</td><td>Président du jury</td></tr></table>

Octobre 2019 – Juin 2023
Abstract

This thesis provides a clarification of Girard's recent work entitled "transcendental syntax". Girard suggests a reorganisation and a reinterpretation of concepts of mathematical logic coming from his previous works on linear logic, proof-nets, ludics and geometry of interaction. Unlike the approaches of semantic explanations based on the linguistic nature of logical entities and their evaluation, transcendental syntax suggests to start from the notion of computation as primitive in order to reconstruct mathematical logic, by starting with the proof-nets of linear logic. The Curry-Howard correspondence, now well-known among theoretical computer scientists, already established a formal correspondence between logic and computation. However, the links between logic and computation are still unclear. Are they two faces of the same thing? Are they different but intersecting notions? Or are they completely distinct? This thesis agrees with the last point of view: one is antique and almost mystical, the other is rather modern and pragmatic. In order to understand their differences and their role, transcendental syntax proposes a radical point of view: no primitive notion of mathematical proof, truth or formula is assumed. Only computation, through the model of computation called "stellar resolution" in this thesis, constitutes the elementary bricks from which logical concepts will be shaped. This model of computation, close to logic programming, uses asynchronous and very free mechanisms of term unification. The main problem that this thesis tackles is that Girard's proposal is rather informal and cryptic. A big objective is to clarify and to provide formal definitions. A particular effort is put in the accessibility of these ideas by suggesting a journey through the old and elementary roots of logic and computation to later reach the most modern works. Girard's works will then be put into context in both a historical and technical ways. The model of stellar resolution will be formally defined, illustrated and commented. The thesis concludes with a technical contributions realised with Thomas Seiller: a new interpretation of the multiplicative fragment of linear logic and a sketch of how it could be extended.

Résumé

Cette thèse apporte un éclaircissement sur le travail récent de Jean-Yves Girard intitulé "syntaxe transcendantale". Girard propose une réorganisation et une relecture des concepts de la logique mathématique venant de ses travaux précédents sur la logique linéaire, les réseaux de preuve, la ludique et la géométrie de l'interaction. À l'inverse des approches d'explications sémantiques reposant sur le caractère linguistique des entités logiques et leur évaluation, la syntaxe transcendantale propose de partir de la notion de calcul comme primitive afin de reconstruire la logique mathématique, en commençant par les réseaux de preuves de la logique linéaire. La correspondance de Curry-Howard, maintenant connue dans la recherche en informatique théorique, établissait déjà une correspondance formelle entre logique et calcul. Cependant, les liens entre logique et calcul sont encore mal compris. Sont-ils deux facettes de la même notion ? Deux notions différentes qui s'intersectent ? Ou alors deux choses complètement distinctes ? Cette thèse est en accord avec le dernier point de vue : l'une est antique et presque mystique, l'autre est plutôt moderne et pragmatique. Pour comprendre leurs différences et leur rôle, la syntaxe
transcendantale propose un point de vue radical : aucune notion primitive de preuve mathé-
matique, de vérité ou de formule n'est supposée. Seul le calcul, à travers un modèle de calcul,
appelé “résolution stellaire” dans cette thèse, constitue le matériau élémentaire à travers lequel
s'incarnent les concepts logiques. Ce modèle de calcul, proche de la programmation logique,
utilise des mécanismes asynchrones et très libres d'unification de termes. Le principal problème
auquel s'attaque cette thèse est que la proposition de Girard est plutôt informelle et cryptique.
Un grand objectif est donc de clarifier et de proposer des définitions formelles. Un effort par-
ticulier est mis dans l'accessibilité de ces idées en proposant un voyage à travers les racines les
plus vieilles et élémentaires de la logique et du calcul pour arriver aux questionnements les plus
modernes. Les travaux de Girard seront ainsi historiquement et techniquement contextualisés.
Le modèle de résolution stellaire sera formellement défini, illustré et commenté. La thèse se con-
clut par une contribution technique réalisée avec Thomas Seiller : une nouvelle interprétation
du fragment multiplicatif de la logique linéaire et une esquisse de comment elle pourrait être
étendue.
# Preface

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

Source: https://abstrusegoose.com/206.

## What led to the existence of this document

When I began to learn computer programming for the first time, it was not especially out of intellectual curiosity or the (direct) consequence of some influence. What I wanted was very simple: to make video games. At the end of high school, I decided that I wanted to do computer programming because I enjoyed it (note that I was not aware of the existence of academic research in computer science and thought computer science was mostly about programming). I later became fascinated by how computation could be related to the “human mind”. If I remember correctly, my first (superficial) interests were computational linguistics and computational neurosciences. How come that the
same things which make video games could be related to human thinking and language? My questions led me to Jérémy Ledent (student at École Normale Supérieure de Lyon at that time) and this was how I discovered the “Curry-Howard correspondence”; a formal correspondence in theoretical computer science relating computer programming and mathematical logic. This correspondence guided me for the following years as I was convinced that it was one of the current most important and overlooked scientific subjects. All my internships were chosen in order to pursue the understanding of this topic.

At one point, Jérémy mentioned Girard's book "The blind spot", which was apparently not a recommended course about logic. I tried to read it and decided that I wanted to work on linear logic (without even seriously knowing what it was really about).

At the end of university, I considered that computational complexity and Girard’s “geometry of interaction” were the most profound subjects relating logic and computation. The only person I knew who was working on both (and that Paul-André Melliès suggested to me) was Thomas Seiller. Thomas proposed several subjects on computational complexity but I felt confident with none of them (I had a weak background in mathematics). He then suggested either to work on the “transcendental syntax” (Girard’s most recent work) or linear dependent types. I chose transcendental syntax as I was more interested in fundamental questions. I actually did not know much about the transcendental syntax, barely read about it and could not understand a single paragraph that Girard wrote about it. For that reason, I never thought that it was worth considering and initially focussed on the geometry of interaction and computational complexity.

**The design of this document**

This long thesis has a chronological structure designed for the exploration of the roots of logic and computation and how they have led to Girard's transcendental syntax. We start from the premises of logic and computation that I associate with the intuition of space and time. I dare to start from the most natural intuitions of logic with Aristotle. Motivated by a search for a contextualisation of modern works in computer science, I then suggest to travel through time with the development of formal logic until Girard's linear logic. This logic, generally understood as a logic of resources or actions, is thought to be more primitive than the intuitive conception we had of logic in the 20th century. It seems to me that linear logic has not been adopted enough in the world-wide study of logic: it often appears that there are seminars of mainstream logic not mentioning linear logic at all. For that reason, I wrote most of what I know about linear logic in the simplest way I could. I mainly focus on intuition and pedagogy, forgetting technical details. I then tried to provide a simple presentation of Girard's geometry of interaction, a work of Girard which has only been partially accepted in the field of linear logic. At the end, this whole logico-computational journey should lead to a better understanding of the
transcendental syntax, which I consider the most conceptually mature (but technically immature) understanding of logic.

This thesis is qualified as “exegesis” mainly because that is how Lionel Vaux called my work with Thomas Seiller and I thought that it was a very accurate description since Girard’s works are known to be very cryptic.

This thesis has been written with the following points in mind:

* *completeness*, justifying the length of the document. During my PhD thesis, I have met various people interested in Girard's recent ideas without being especially invested in the mathematics related to it. I found it necessary to provide resources so that the document would be as much accessible and self-sufficient as possible, even for philosophers or curious minds. I tried to provide a lot of external references as well for people willing to learn more;

* *pedagogy*, because I remarked that what was problematic in Girard's recent works was not really their technical difficulty but the lack of pedagogy and efficient communication. In particular, I tried to put efforts in the bridge between geometry of interaction (which is already known in the field of linear logic and some parts of theoretical computer science) and transcendental syntax;

* *accessibility*, as I initially wanted to write this document in French (my mother tongue, that I prefer over English) but after receiving few messages from non-French speakers interested in the transcendental syntax, I decided to write it in English instead;

* *entertainment* (probably odd for a PhD thesis), as I wanted to write something interesting and thought-provoking. For that reason, I included a lot of unknown or forgotten (mainly historical) facts. In most sections, a “discussion” part is included at the end in order to suggest non-technical comments on what has been written in the section.

## How to read

Only the two first chapters are (almost) independent. The other chapters should be read in order until the end but not necessary from the beginning. Depending on your knowledge, you can choose to start from a specific point until the end.

All technical prerequisites are given at the end of this document, in the appendix.

Have a nice read!

Boris Eng.
Acknowledgements (in French)

Mon travail de thèse est le fruit d'un long parcours fait de rencontres et d'interactions. Cette partie de ma thèse est dédiée aux personnes qui m'ont apporté plus qu'elles ne le pensent et aux personnes qui ont indirectement contribué à ma thèse.

Je remercie mes directeurs de thèse Thomas Seiller et Damiano Mazza, que j'admirais déjà scientifiquement. Ils ont tous deux été successivement mes encadrants de stage de recherche en première et seconde année de master. Ils m'ont permis de satisfaire ma curiosité avec une grande liberté sur des sujets dont je ne savais en fait pas grand-chose.

Je remercie mes rapporteurs Lionel Vaux et Lorenzo Tortora de Falco pour leur exigence concernant la qualité technique de ma thèse et leur relecture particulièrement attentive et approfondie de mon manuscrit.

Je remercie les autres membres de mon jury: Jean-Baptiste Joinet pour son intérêt sincère envers mon sujet de thèse et Claudia Faggian pour ses conseils durant ma thèse. Claudia a notamment influencé mon choix de rediriger mon manuscrit en avance avec un parcours en largeur à moment où je ne savais pas où situer mon sujet. Un conseil que j'ai probablement poussé à l'extrême.

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

Je souhaite maintenant remercier, dans l'ordre chronologique, les personnes qui m'ont construit scientifiquement jusqu'à ma soutenance de thèse.

Ces premiers remerciements vont vers Monsieur Blot, mon professeur de mathématiques en terminale au lycée Dorian (filière technologique). Il a été le premier enseignant à croire en moi alors que j'avais toujours été un étudiant très moyen. Il avait remarqué et suivi mon intérêt pour la programmation mais aussi éveillé mon intérêt pour l'informatique théorique.

Je remercie Kostia Chardonnet, un de mes camarades de lycée qui m'a accompagné dans la programmation et mon humour le plus absurde. Je lui dois mon admission en DUT Informatique. Nous avons le point commun étonnant d'avoir suivi, ensemble, le même parcours jusqu'au doctorat en informatique théorique.

Je remercie Jérémy Ledent, rencontré par hasard sur un forum de programmation (mais jamais rencontré en personne !), qui a énormément guidé le lycéen naïf que j'étais et qui
m'a fait découvrir la recherche en informatique théorique et la passionnante correspondance de Curry-Howard. Il a influencé ma décision de poursuivre mes études en licence puis au Master de Recherche Parisien en Informatique (MPRI).

Je remercie Yannis Juglaret et Cătălin Hrițcu (qui était son directeur de thèse), qui m'ont très bien accueilli à l'Inria de Paris dans l'équipe Prosecco pour un stage avec l'assistant de preuve Coq en fin de DUT Informatique. Ils ont été tous deux particulièrement investis dans la confirmation de mon intérêt pour la recherche scientifique et ont été un moteur dans mon parcours.

Je remercie Michele Pagani et Delia Kesner qui m'ont accueilli en stage de L3 informatique sur la logique linéaire, sujet sur lequel je voulais travailler sans vraiment savoir de quoi il s'agissait. Ce stage m'a confronté à un mélange entre formalités techniques et théories abstraites qui est nécessaire dans la recherche en informatique théorique.

Je remercie Olivier Laurent (que je n'ai en fait jamais rencontré et qui ne me connaît probablement que de nom) qui a répondu, par e-mail, à mes questions techniques de la L3 Informatique jusqu'au doctorat (probablement sans le remarquer). J'ai toujours été impressionné et inspiré par son sens du détail et de la précision.

Je remercie Tito que j'ai considéré comme mon “grand-frère scientifique”. Il m'a guidé en master et en thèse sur la logique linéaire, la géométrie de l'interaction et bien d'autres sujets de l'informatique théorique voire du monde académique en général.

Je remercie toutes les personnes qui ont accepté d'échanger avec moi concernant ma thèse : Matteo Acclavio, Benjamin Hellouin, Mccolm Gregory et Natasha Jonoska, Alexander Leitsch, Carlos Olarte, Félix Castro, Paolo Pistone, Arnaud Valence, Aleksey Gonus, François-René Rideau alias Fare (qui influencera la suite de mon parcours), Rémi Nollet ainsi que d'autres anonymes et personnes extérieures au monde académique.

Mes derniers remerciements vont au groupe de travail ReFL (Réflexions sur les Fondements de la Logique, et initialement “nouvelle église girardienne” puis “cercle transcendantaliste”) que j’ai co-fondé avec Davide Barbarossa, Valentin Maestracci et Pablo Donato. Parmi les contributeurs principaux de ReFL figurent : Adrien Ragot, Ambroise Lafont, Baptiste Chanus, Jérémy Hervé, Kostia Chardonnet, Julien Marquet, Paul Séjourné, Sidney Congard, Tito et Xavier Denis. Ils m’ont tous permis de sortir de ma solitude de scientifique mais m’ont aussi apporté une grande stimulation intellectuelle : de nombreux passages de mon manuscrit viennent en fait de conversations avec des membres de ReFL. J’ai trouvé dans ReFL des personnes à la pensée profonde, sceptique et audacieuse. Parmi ces membres, Pablo Donato et Paul Séjourné ont particulièrement suivi mes réflexions sur la syntaxe transcendantale et j’ai beaucoup échangé avec eux sur les idées les plus expérimentales et spéculatives.
# Contents

Preface 4

Acknowledgements (in French) 7

1 Logical traditions 16

1 The experience of regularity 16

2 Logical dreams and mathematical realisations of reasoning 20

3 Paradoxes and the jails of the Format 23

4 The location of certainty: the mind or the paper? 25

5 Syntax and semantics / Language and reality 27

6 Propositional calculus 30

7 Predicate calculus 33

8 Second-order logic 36

9 Natural deduction 38

– Intuitionistic natural deduction 39

– Classical natural deduction 44

– Proof reduction 44

10 Sequent calculus 46

– Classical sequent calculus 46

11 Monolateral sequent calculus 50

– Cut-elimination procedure 52

12 Discussion: doubting traditions 55

2 Computational panorama 60

13 The experience of procedurality 60

14 Realisation of machines 64

15 Computation as functional process 66

– The notion of function 66

– Functional foundations for logic 68

– Mathematical functions as a model of computation 70

– The notion of (simple) type 73

16 Computation as state machine 75

– The mathematician-machine 75

– A bit of hacking with Turing machines 78

– Undecidable problems 80

– Towards programming 81
<table>
  <tbody>
    <tr>
      <td>17</td>
      <td>Computation as tiling construction</td>
      <td>83</td>
    </tr>
    <tr>
      <td>18</td>
      <td>Computation as flow of information</td>
      <td>86</td>
    </tr>
    <tr>
      <td>19</td>
      <td>Discussion: a single materialisation of computation?</td>
      <td>89</td>
    </tr>
    <tr>
      <td><b>3</b></td>
      <td><b>Linking logic and computation</b></td>
      <td><b>92</b></td>
    </tr>
    <tr>
      <td>20</td>
      <td>The different traditions of logic and computation</td>
      <td>92</td>
    </tr>
    <tr>
      <td>21</td>
      <td>Curry-Howard-Lambek correspondence</td>
      <td>94</td>
    </tr>
    <tr>
      <td></td>
      <td>- Natural deduction and Lambda-calculi</td>
      <td>94</td>
    </tr>
    <tr>
      <td></td>
      <td>- The functional interpretation of classical logic</td>
      <td>97</td>
    </tr>
    <tr>
      <td></td>
      <td>- The functional interpretation of quantification</td>
      <td>98</td>
    </tr>
    <tr>
      <td>22</td>
      <td>Realisability</td>
      <td>99</td>
    </tr>
    <tr>
      <td></td>
      <td>- Kleene realisability</td>
      <td>99</td>
    </tr>
    <tr>
      <td></td>
      <td>- Krivine realisability</td>
      <td>101</td>
    </tr>
    <tr>
      <td></td>
      <td>- Reconstruction of simple types</td>
      <td>103</td>
    </tr>
    <tr>
      <td>23</td>
      <td>Logic programming</td>
      <td>103</td>
    </tr>
    <tr>
      <td></td>
      <td>- Reasoning with programs</td>
      <td>103</td>
    </tr>
    <tr>
      <td></td>
      <td>- Normal forms</td>
      <td>104</td>
    </tr>
    <tr>
      <td></td>
      <td>- First-order resolution</td>
      <td>107</td>
    </tr>
    <tr>
      <td></td>
      <td>- Reasoning with Horn clauses</td>
      <td>109</td>
    </tr>
    <tr>
      <td>24</td>
      <td>Discussion: the limits of the proof-program correspondence</td>
      <td>110</td>
    </tr>
    <tr>
      <td><b>4</b></td>
      <td><b>Linear logic</b></td>
      <td><b>115</b></td>
    </tr>
    <tr>
      <td>25</td>
      <td>The emergence of linear logic</td>
      <td>115</td>
    </tr>
    <tr>
      <td>26</td>
      <td>Seizing the means of production</td>
      <td>116</td>
    </tr>
    <tr>
      <td>27</td>
      <td>Classical linear logic sequent calculus</td>
      <td>119</td>
    </tr>
    <tr>
      <td></td>
      <td>- Multiplicative fragment</td>
      <td>120</td>
    </tr>
    <tr>
      <td></td>
      <td>- Neutral elements</td>
      <td>123</td>
    </tr>
    <tr>
      <td></td>
      <td>- Additive fragment</td>
      <td>123</td>
    </tr>
    <tr>
      <td></td>
      <td>- Exponential fragment</td>
      <td>126</td>
    </tr>
    <tr>
      <td>28</td>
      <td>Some applications and intuitive interpretations</td>
      <td>129</td>
    </tr>
    <tr>
      <td>29</td>
      <td>Proof-structures and proof-nets</td>
      <td>131</td>
    </tr>
    <tr>
      <td></td>
      <td>- Multiplicative unit-free proof-nets</td>
      <td>133</td>
    </tr>
    <tr>
      <td></td>
      <td>- Multiplicative unit proof-nets</td>
      <td>139</td>
    </tr>
    <tr>
      <td></td>
      <td>- Additive proof-nets</td>
      <td>140</td>
    </tr>
    <tr>
      <td></td>
      <td>- Exponential proof-nets</td>
      <td>142</td>
    </tr>
    <tr>
      <td>30</td>
      <td>Correctness criteria</td>
      <td>145</td>
    </tr>
    <tr>
      <td></td>
      <td>- Girard's long trip criterion</td>
      <td>146</td>
    </tr>
    <tr>
      <td></td>
      <td>- Danos-Regnier criterion for MLL+MIX</td>
      <td>151</td>
    </tr>
    <tr>
      <td></td>
      <td>- Criteria for multiplicative units</td>
      <td>154</td>
    </tr>
    <tr>
      <td></td>
      <td>- Criteria for additive proof-structures</td>
      <td>155</td>
    </tr>
    <tr>
      <td></td>
      <td>- Criteria for exponential proof-structures</td>
      <td>156</td>
    </tr>
    <tr>
      <td>31</td>
      <td>Discussion: the structure of normative constraints</td>
      <td>156</td>
    </tr>
  </tbody>
</table>
5 The geometry of interaction 159

32 Towards a geometry of interaction 159

33 Multiplicative proofs with permutations 160

– Long-trip criterion with cyclic permutations 162

– General interaction of permutation and cut-elimination 164

– Interpretation of types/formulas 167

34 Infinitary extension towards full linear logic 170

35 Danos and Regnier's algebra of paths for MLL 175

– Paths in a proof-structure 175

– Weight of a multiplicative path 176

36 Token machine for the geometry of interaction 179

37 Alternative approaches 182

– Flows and wirings 182

– Seiller's interaction graphs 185

– Proofs as partitions of a set 187

– Ludics 191

38 Discussion: new insights on the notion of proof 193

6 Towards a transcendental syntax 197

39 Learning from the past 198

40 The logical avant-gardism of computer science 204

41 A new architecture for logic 207

42 Analytic space / Answers 208

– Constat and performance 208

– The chosen one: stellar resolution 209

43 Synthetic space / Questions 211

– Usage / Curry typing 211

– Usine / Church typing 212

– Adequacy and certainty / Cut-elimination 214

– Towards a justification of logical rules 215

44 Derealism / Animism 216

– Logic and computation entangled 216

– Globality and locality in logical systems 217

– Apodictics / First-order 219

– Epidictics / Second-order 219

– An original proposal: epidictic and apodictic models of computation 220

45 Illustration: Transcendental Syntax applied to lambda-calculus 221

46 Discussion: is it a right understanding of logic? 222

7 Stellar resolution 224

47 Intuition behind stellar resolution 225

48 Stars and constellations 227

49 Abstract execution 230

– Evaluation of diagrams 231
<table><tr><td></td><td>- Execution of constellations</td><td>243</td></tr><tr><td></td><td>- The dynamics of subjective rays</td><td>244</td></tr><tr><td>50</td><td>Concrete execution</td><td>247</td></tr><tr><td>51</td><td>Interactive execution</td><td>250</td></tr><tr><td>52</td><td>Difference with Girard's stars and constellations</td><td>258</td></tr><tr><td>53</td><td>Discussion: comparison with other notions</td><td>259</td></tr></table>

## 8 Illustrating stellar resolution 262

<table><tr><td>54</td><td>Flows, wirings and graphs</td><td>262</td></tr><tr><td>55</td><td>Encoding of logic programs with Horn clauses</td><td>265</td></tr><tr><td>56</td><td>State machines</td><td>267</td></tr><tr><td></td><td>- Non-deterministic finite automata (NFA)</td><td>267</td></tr><tr><td></td><td>- Non-deterministic pushdown automata (NPDA)</td><td>270</td></tr><tr><td></td><td>- Finite sequential transducers (NFST)</td><td>271</td></tr><tr><td></td><td>- Non-deterministic Turing machines (NTM)</td><td>272</td></tr><tr><td>57</td><td>More advanced machines</td><td>275</td></tr><tr><td></td><td>- Alternating Turing machines (ATM)</td><td>275</td></tr><tr><td></td><td>- Non-deterministic finite tree automata (NFTA)</td><td>278</td></tr><tr><td></td><td>- Krivine Abstract Machine (KAM) with call/cc</td><td>280</td></tr><tr><td>58</td><td>Generalised circuits</td><td>282</td></tr><tr><td>59</td><td>Tile systems with the abstract tile assembly model</td><td>285</td></tr><tr><td>60</td><td>Discussion: a common language for classical computation?</td><td>287</td></tr></table>

## 9 Properties of execution for objective constellations 292

<table><tr><td>61</td><td>Computability of stellar resolution</td><td>292</td></tr><tr><td>62</td><td>Classes of constellations</td><td>293</td></tr><tr><td></td><td>- (Non-)Terminating constellations</td><td>293</td></tr><tr><td></td><td>- Graph-structural classification of constellations</td><td>294</td></tr><tr><td>63</td><td>Stellar transformations</td><td>298</td></tr><tr><td>64</td><td>Partial pre-execution and confluence</td><td>299</td></tr><tr><td>65</td><td>Discussion: the sufficient conditions for logical emergence</td><td>303</td></tr></table>

## 10 Stellar interpretation of multiplicative linear logic 304

<table><tr><td>66</td><td>Proofs as constellations</td><td>304</td></tr><tr><td>67</td><td>Simulation of cut-elimination</td><td>307</td></tr><tr><td>68</td><td>Simulation of Danos-Regnier correctness test</td><td>314</td></tr><tr><td>69</td><td>Construction of multiplicative formulas</td><td>322</td></tr><tr><td></td><td>- Usine interpretation</td><td>323</td></tr><tr><td></td><td>- Usage interpretation</td><td>327</td></tr><tr><td>70</td><td>Soundness and completeness</td><td>331</td></tr><tr><td></td><td>- Adequacy between Usine and Usage</td><td>331</td></tr><tr><td></td><td>- A complete model of MLL+MIX</td><td>333</td></tr><tr><td></td><td>- A complete model of MLL</td><td>337</td></tr><tr><td>71</td><td>The case of multiplicative units</td><td>338</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>72</td>
      <td>Discussion: what is a multiplicative proof?</td>
      <td>340</td>
    </tr>
    <tr>
      <td>11</td>
      <td>Interpretation of intuitionistic implication</td>
      <td>342</td>
    </tr>
    <tr>
      <td>73</td>
      <td>MLL with intuitionistic implication (MLL2I)</td>
      <td>342</td>
    </tr>
    <tr>
      <td></td>
      <td>- MLL2I sequent calculus</td>
      <td>343</td>
    </tr>
    <tr>
      <td></td>
      <td>- MLL2I proof-structures</td>
      <td>344</td>
    </tr>
    <tr>
      <td>74</td>
      <td>Simulation of cut-elimination</td>
      <td>347</td>
    </tr>
    <tr>
      <td>75</td>
      <td>Girard's original correctness criterion</td>
      <td>351</td>
    </tr>
    <tr>
      <td>76</td>
      <td>Discussion: what is a non-linear proof?</td>
      <td>355</td>
    </tr>
    <tr>
      <td>12</td>
      <td>Apodictic experiments</td>
      <td>357</td>
    </tr>
    <tr>
      <td>77</td>
      <td>Logical constants</td>
      <td>357</td>
    </tr>
    <tr>
      <td></td>
      <td>- Objective constant</td>
      <td>358</td>
    </tr>
    <tr>
      <td></td>
      <td>- Subjective constant</td>
      <td>360</td>
    </tr>
    <tr>
      <td></td>
      <td>- Shape specification</td>
      <td>361</td>
    </tr>
    <tr>
      <td></td>
      <td>- Order 0 multiplicative linear logic</td>
      <td>362</td>
    </tr>
    <tr>
      <td>78</td>
      <td>Expansional connectives</td>
      <td>362</td>
    </tr>
    <tr>
      <td>79</td>
      <td>Visibility and non-classical truth</td>
      <td>364</td>
    </tr>
    <tr>
      <td>80</td>
      <td>System-free arithmetic on relative numbers</td>
      <td>368</td>
    </tr>
    <tr>
      <td>81</td>
      <td>Discussion: anarchy</td>
      <td>369</td>
    </tr>
    <tr>
      <td>13</td>
      <td>Epidictic experiments</td>
      <td>371</td>
    </tr>
    <tr>
      <td>82</td>
      <td>Genericity of proof-structures</td>
      <td>371</td>
    </tr>
    <tr>
      <td>83</td>
      <td>Usage interpretation of second-order linear logic</td>
      <td>373</td>
    </tr>
    <tr>
      <td>84</td>
      <td>Usine in the case of predicate calculus: a sketch</td>
      <td>375</td>
    </tr>
    <tr>
      <td>85</td>
      <td>Discussion: the theory of epidictic architectures</td>
      <td>378</td>
    </tr>
    <tr>
      <td colspan="2">Conclusion</td>
      <td>380</td>
    </tr>
    <tr>
      <td>86</td>
      <td>Summary and contributions</td>
      <td>380</td>
    </tr>
    <tr>
      <td>87</td>
      <td>Horizons</td>
      <td>381</td>
    </tr>
    <tr>
      <td>88</td>
      <td>Limits of the current presentation of transcendental syntax</td>
      <td>387</td>
    </tr>
    <tr>
      <td>A</td>
      <td>Mathematical conventions</td>
      <td>389</td>
    </tr>
    <tr>
      <td>A.1</td>
      <td>General notations</td>
      <td>389</td>
    </tr>
    <tr>
      <td>A.2</td>
      <td>Set theory</td>
      <td>390</td>
    </tr>
    <tr>
      <td>A.3</td>
      <td>Language theory</td>
      <td>392</td>
    </tr>
    <tr>
      <td>B</td>
      <td>Term unification</td>
      <td>394</td>
    </tr>
    <tr>
      <td>B.1</td>
      <td>Elementary definitions</td>
      <td>394</td>
    </tr>
    <tr>
      <td>B.2</td>
      <td>Unification algorithm</td>
      <td>398</td>
    </tr>
    <tr>
      <td>C</td>
      <td>Graph theory</td>
      <td>402</td>
    </tr>
    <tr>
      <td>C.1</td>
      <td>Non-directed hypergraphs</td>
      <td>402</td>
    </tr>
    <tr>
      <td>C.2</td>
      <td>Directed hypergraphs</td>
      <td>405</td>
    </tr>
    <tr>
      <td>C.3</td>
      <td>Special cases of hypergraphs</td>
      <td>407</td>
    </tr>
  </tbody>
</table>
<table><tr><td>D Transcendental aesthetics</td><td>410</td></tr></table>
“Tout commence en mystique et tout finit en politique.

– Charles Péguy (Notre Jeunesse)

”
# Chapter 1

## Logical traditions

In this chapter, instead of exposing the usual folklore of logic, I suggest a personal reading of the Western tradition of mathematical logic. This revision of logic is deeply influenced by modern works on Girard's linear logic and its connexions with computation. Despite these rather technical inspirations, I would like this chapter to be very accessible but I also wrote it so that it can be interesting for people who already received an education on formal logic.

I start with a historical background coming from a personal little investigation. My reference for the formal presentations of logic is Hedman's introduction to logic [Hed04]. I decided to modify a bit the usual definitions and notations according to my personal taste.

### 1 The experience of regularity

This section is inspired by Paolo Pistone's great presentation (in French) “Aristote et l'électricien : le branchement des idées” for *Treize Minutes Marseille* and Alain Lecomte's course on philosophy of language.

§1.1 We all have a vague idea of what logic is, as if it was either hard-wired in our brain or part of nature itself. Imagine that I say:

"All humans are mortal" and "all Greeks are human", hence "all Greeks are mortal".

"All humans are mortal" and "all French are human", hence "all French are mortal".

"All unicorns are cool" and "all turtles are unicorns", hence all "turtles are cool".

§1.2 These three sentences produce new knowledge from two premises (preceding the word "hence"). In the first two statements, we can feel that the words "Greek" and "French" are interchangeable and unimportant. No matter what word we replace these words with, the statement seems to hold. If we look at the more extreme third sentence,
<table><caption>Figure 1.1: Types of assertion in Aristotelian syllogisms.</caption><thead><tr><td>Code</td><td>Name</td><td>Constructor</td></tr></thead><tbody><tr><td>A</td><td>Universality</td><td>All S are P</td></tr><tr><td>E</td><td>Existence</td><td>Some S are P</td></tr><tr><td>I</td><td>Negative universality</td><td>No S are P</td></tr><tr><td>O</td><td>Negative existence</td><td>Some S are not P</td></tr></tbody></table>

the subjects and properties (called *predicates*) are replaced by pure nonsense and the whole sentence still makes sense. In each case, the two premises are only *hypothetically* considered valid but are not necessarily valid themselves. What matters is whether or not the conclusion follows from the two premises, hence validity is actually independent from our understanding of words or of any external reference. This is what we call *deductive reasoning*. These statements go without saying and we would simply say “it’s logical!” to justify them.

§1.3 Notice that the three sentences above have the same *shape*, hence exhibiting some regularities in the production of knowledge. They are instance of a *pattern*. The concepts can be replaced by generic symbols, hence only the *spatial* arrangement of concepts matters and not the concepts themselves. We obtain the following more general statement:

“All *M* are *P*” and “all *S* are *M*”, therefore “all *S* are *P*”.

§1.4 **Aristotle's syllogism.** The letter “*M*” stands for *major premise*, “*P*” for *predicate* (a property of a subject) and “*S*” for *subject*. This type of deductive reasoning having two premises and a unique conclusion is what Aristotle called a *syllogism* in his work *Prior Analytics* (part of the *Organon*), during Ancient Greece. By analysing all the possible syllogisms constructible with the assertions of Figure 1.1, it is possible to create categories of logical patterns. At the time of Aristotle 19 valid types<fnref n="1" /> of syllogisms were extracted from 256 logical combinations. In particular, our syllogism above has been given the mnemonic name<fnref n="2" /> of **BARBARA** for the three occurrences of universal assertions (code *A* in Figure 1.1).

§1.5 Deduction does not come from nowhere. How can such rules exist and how can they produce valid knowledge? A modern hint would be that assertions such as “All *M* are *P*” are *usable entities* with an input and an output allowing connexion with other assertions. It is a machine producing *P* from *M*. In order to *prove* “all *S* are *P*”, we connect the two premises seen as tools: I have “*S*” and know that it leads to “*M*” (second premise), itself leading to “*P*” (first premise). It is illustrated by the path of Figure 1.2 between the two occurrences of “*P*”. This gives a *spatial* criterion for logical correctness.

<footnote n="1">¹Leibniz added up to 25 types in his *De arte combinatoria* (1666).</footnote>

<footnote n="2">²Mnemonic names and the notations *A*, *E*, *I* and *O* were given by medieval scholars [KKPS82] (associated with what we call *scholasticism*). The idea was to associate syllogisms with Latin names (Barbara, Cesare, Darii, Barbari, ...) so that vowels correspond to types of assertion.</footnote>
"All *M* are *P*" and "all *S* are *M*", therefore "all *S* are *P*".

<table><caption>Figure 1.2: Path in the reasoning of an instance of syllogism.</caption><thead><tr><td>Name</td><td>Constructor</td><td>Modern notation</td></tr></thead><tbody><tr><td>Conditional</td><td>If A then B</td><td>A ⇒ B, A ⊃ B, A → B</td></tr><tr><td>Disjunction</td><td>Either A or B (but not both)</td><td>A ∨ B, A + B</td></tr><tr><td>Conjunction</td><td>A and B</td><td>A ∧ B, A ⋅ B</td></tr><tr><td>Negation</td><td>not A</td><td>¬A, Ā</td></tr></tbody></table>

<caption>Figure 1.3: Logical connectives in stoic logic where *A* and *B* are assertibles.</caption>

§1.6 **Stoic logic.** Still in Ancient Greece, the *stoics* [GW04, Volume I] (and Chrysippus in particular) developed a different (and more modular) point of view on logic where a whole sentence such as “it’s raining today” is a single object called *assertible*. Assertibles are either *true* or *false* and can be connected with *logical connectives* presented in Figure 1.3. In this case, the focus is not on the *structure of reasoning* but on the treatment and preservation of truth during the evaluation of a sentence. For instance, given two assertibles *A* and *B*, if *A* is true but *B* is false then “*A* and *B*” must be false. It suggests that logical validity is ruled by some mechanisms underlying logical connectives. Reasoning then relies on five indemonstrable arguments given in Figure 1.4.

§1.7 Although the study of logic can take several form, in the two cases described above (Aristotelian logic and stoic logic), logic takes place in the very specific and concrete space of *language*. Logic was thought to be about what could be expressed with written or spoken words. During Ancient Greece, syllogism was correlated with discussion, public speaking and the art of persuasion. If there are valid ways of reasoning, there are also wrong ways known as (*logical*) *fallacies*, which can be used on purpose to trick or convince people (about skills or politics for instance). Such wrong arguments look like valid ones but exploit the ambiguity of consequence:

"A better product is usually more expensive" and "this product is expensive",

<table><caption>Figure 1.4: Indemonstrable arguments in stoic logic.</caption><thead><tr><td>Name</td><td>Constructor</td></tr></thead><tbody><tr><td>Modus ponens</td><td>(A implies B) and A, therefore B</td></tr><tr><td>Modus tollens</td><td>(A implies B) and not B, therefore not A</td></tr><tr><td>Conjunctive syllogism</td><td>Not (both A and B) and A, therefore not B</td></tr><tr><td>Modus tollendo ponens</td><td>(Either A or B) and not A, therefore B</td></tr><tr><td>Modus ponendo tollens</td><td>(Either A or B) and B, therefore not A</td></tr></tbody></table>
therefore “it must be of a better quality”.

§1.8 Using this argument, I can make you buy something at an unfair price. The art of “unreal wisdom” which was criticised during Ancient Greece is usually called sophism<fnref n="3" />. In “On Sophistical Refutations” (part of the Organon), Aristotle described several categories of fallacies and how to react to it. The list has later been developed several times by several authors [BC06, Sch31] and is now considered as a sort of intellectual self-defence<fnref n="4" />.

§1.9 **Medieval logic.** Something I have rarely seen mentioned in logic is the medieval world<fnref n="5" /> [GW04, Volume II]. Medieval schools were mainly interested in the study of Aristotle’s syllogisms as if they were sort of multiplication tables we learn by heart (each valid syllogism is associated with a mnemonic Latin name). Medieval works on logic includes additional linguistic features such as plurality, tense and modality in the context of Aristotelian logic or theories about terms and predicates [Rea02, Spa02, Knu99]. Succeeding Greek’s *Dialectic* (the discourse between several opponents wishing to establish truth through valid arguments, thus relating logic and dialogue) was considered part of logic in medieval schools [Abe06]. But beside this Aristotelian legacy, medieval logic was not void of innovation: interestingly, the first proof of the *principle of explosion*<fnref n="6" /> is attributed to a French logician of the 12th century named William of Soissons [Mar86]. This principle states that from a contradiction such that “A and not A”, it is possible to infer any statement, which should sound very surprising.

§1.10 It is generally agreed that Western logic mainly originates from Aristotle, stoics and medieval schools. However, something we do not always realise is that, despite the objective appearance of logic, our understanding of it is strongly influenced by seemingly insignificant things such as culture and geography. Indian logic [GW04, Volume I] (itself correlated with Buddhist logic [Fac83]) and Chinese logic [Chm09] (with the *School of Names*) were especially old forms of logic which were developed independently of Greek logic. In particular, Indian logic later had a direct influence on Western logic between the 18th and 19th century [Col58]. Something else which is notable is that Arabic logic [Bla98, Res64] had early forms of syllogisms which actually influenced Islamic law and theology, but also had an early access to Greek logic through Arabic translations, even before the Christian scholars of medieval schools. This led to Avicenna’s alternative to Aristotelian logic including novelties such as *temporal modalities* [Res12]. Despite all those traditions of logic, this thesis will only be another brick in the story of Western logic, but I believe that it would be very nice to study old alternative traditions of logic in the light of the modern works that I will present in this thesis.

<footnote n="3">³Although it originally referred to the teaching of eloquence and the art of persuasion.</footnote>

<footnote n="4">⁴Especially on social networks. Unfortunately, debates do not only evolve in the logical dimension.</footnote>

<footnote n="5">⁵Which suffers from a lot of unfortunate prejudices.</footnote>

<footnote n="6">⁶Although it seems to have been rejected at first [Mar86].</footnote>
<table><thead><tr><td>Syllogism</td><td>Boolean equation</td></tr></thead><tbody><tr><td>All A is B</td><td>AB = B or A(1 - B) = 0</td></tr><tr><td>No A is B</td><td>AB = 0</td></tr><tr><td>Some A is B</td><td>V = AB</td></tr><tr><td>Some A is not B</td><td>V = A(1 - B)</td></tr></tbody></table>

Figure 2.1: Algebraisation of Aristotle’s syllogisms. Saying that all A is B is the same as saying that the concept of being both A and B is the same as the concept B (inclusion of A within B), written AB = B, or equivalently that being A but not B is a nonsense (A(1 - B) = 0). Saying that no A is B is the same as saying that being both A and B is a nonsense (AB = 0). Saying that some A is B is the same as saying that there is some concept V equal to the concept of being both A and B. This works if concepts are non-empty (which is also the case in Aristotle’s point of view). From these interpretations, it is then easy to understand the last syllogism.

## 2 Logical dreams and mathematical realisations of reasoning

§2.1 Between the 17th and 18th century, Gottfried Leibniz was a prominent scientific figure which contributed to several fields such as mathematics, philosophy, theology, ethics and more. However, it seems that his works on logic did not attract much attention at his time. For that reason, it is often considered that he foresaw the future developments of formal logic. Leibniz had the very ambitious project of designing a universal symbolic language called *characteristica universalis* [Jae96], which would be relevant for any rational discussions whether it be in metaphysics, physics, mathematics, music, or even everyday life conversations. Such a language would be based on an *alphabet of human thoughts* [WGRO93] which constitute rational thinking. Although this idea has been mentioned several times by Leibniz, it seems that it has never fully flourished and has even be considered too naive by its creator<fnref n="7" />. This great ambition resuscitated again after Leibniz, during the 19th century with a different philosophy.

§2.2 **Algebraic logic.** Still in this idea of a calculus of logic, the English mathematician George Boole initiated an algebraisation of logic<fnref n="8" /> in “*The Laws of thought*” which aimed at giving a mathematical foundation to Aristotle’s logic which would be simple and as close as possible to “high school algebra”<fnref n="9" /> [Bur00]. In his algebra of logic, variables x, y, z, ... represent classes or concepts over which we use arithmetic operations +, -, × and a symbol = for equality. The intersection of concepts is written $x \times y$ or $xy$. This allows to express the fact that “good man” is the intersection of “good” and “man”. In particular, logic has to satisfy $xx = x$ (which can also be written $x^2 = x$), illustrating

<footnote n="7">⁷According to an informal discussion with David Rabouin, Leibniz himself later considered this universal alphabet to be probably impossible to realise.</footnote>

<footnote n="8">⁸Which is actually different from what we call *Boolean algebra* today.</footnote>

<footnote n="9">⁹Which I never studied in high school.</footnote>
the fact that being “good and good” is the same as being “good”. Remark that the
only numbers satisfying this equation are 0 (0 × 0 = 0) and 1 (1 × 1 = 1), which is
coherent with the truth values *false* (concept of *emptiness*) and *true* (concept of *the
whole universe*). Boole was able to represent Aristotle’s assertions in this system: “all x
are y” becomes *xy* = x (all things such are both x and y are also x, hence the concept of
x is contained in y) and “no x is y” becomes *xy* = 0 (it is impossible to be both x and
y). Other syllogisms are presented in Figure 2.1. Interestingly, Aristotle’s A (universal)
statements looks like sort of *functions* taking A and producing B by associating a new
“category” to a given individual coming from a given category. As for E statements,
they are like *pairs* (*A*, *B*) reuniting an individual and the category it is part of. This
intuition will actually be essential in modern developments of logic such as (*dependent*)
*type theory*. Finally notice that subjects and predicates are of the same kind (unlike
Aristotelian’s syllogisms which distinguishes the two)<fnref n="10" />.

§2.3 In this “algebraic period” [Boc61], several mathematicians such as Ernst Schröder, Augustus De Morgan, Hugh MacColl, Charles Sanders Peirce and John Venn contributed to the establishment of relations between an algebraic presentation of logic and other fields such as set theory, order theory or lattice theory. Works on algebraic logic were updated, extended and developed actively in that direction. At this time, Indian philosophy started to have an influence on Western scholars (especially English): Aristotelian logic and Indian logic were compared with the conclusion that they were not equivalent [Gan13]. De Morgan himself was also aware of Indian logic and even mentioned it explicitly:

> “The two races which have founded the mathematics, those of the Sanskrit and Greek languages, have been the two which have independently formed systems of logic.”

– Augustus De Morgan [DM60]

§2.4 **Ideography.** Following these first mathematical presentations of logic and Leibniz's initial ideal of a universal language<fnref n="11" />, Gottlob Frege invented a graphical language for logical sentences called *Begriffsschrift*<fnref n="12" /> [F+79] (1879) or *ideography* in English. The construction of sentences is presented in Figure 2.2. Frege wanted it to be what Leibniz hoped for: a sort of microscope allowing the analysis of the relations between concepts. I would personally call it the “circuits of thought”. This graphical language for logic constitutes the first known occurrence of *universal quantification* (expressing “for all” in logical sentences) with bounded variables. Something which is a bit less known is that

<footnote n="10">¹⁰Actually, this shared space for subjects and predicates is unusual. Even in more modern formal logic (including dependent type theory), they are usually distinguished.</footnote>

<footnote n="11">¹¹Although Frege places himself in Leibniz's scientific lineage, it seems that Frege's philosophy does not reflect Leibniz's philosophy. This relation to Leibniz apparently produced an exaggerated image of Leibniz as a logicist. See David Rabouin's works for more details.</footnote>

<footnote n="12">¹²I was very fascinated by it when I started to learn logic.</footnote>
<table><caption>Figure 2.2: Sentences written in Frege's Begriffsschrift. The representation of the formula $\forall x.P(x) \Rightarrow P(x)$ stated as a tautology is presented at the end as an example. A tautology is a statement which is always true whatever the content of its subformulas. A contradiction is always false.</caption><thead><tr><th>Name</th><th>Frege's Begriffsschrift</th><th>Modern notation</th></tr></thead><tbody><tr><td>Assertion</td><td>— A</td><td>A</td></tr><tr><td>Negation</td><td>— A</td><td>¬A</td></tr><tr><td>Tautology</td><td>— A</td><td>|= A</td></tr><tr><td>Contradiction</td><td>— A</td><td>≠= A</td></tr><tr><td>Equality (≠ logical equivalence)</td><td>— A ≡ B</td><td>A = B</td></tr><tr><td>Universal quantification</td><td>— P(x)</td><td>∀x.P(x)</td></tr><tr><td>Conditional</td><td>— P(x)</td><td>A ⇒ B<br/>|= ∀x.P(x) ⇒ P(x)</td></tr></tbody></table>

Peirce<fnref n="13" /> actually invented independently a graphical language called *existential graphs* [Pei79], which includes both *universal* and *existential* (“there exists”) quantifications. Both these systems are anticipations of what we call *predicate calculus* or *first-order logic* [Fer01] in today’s mathematical logic and which is now standard.

§2.5 **Frege's calculus.** Frege does not content himself only with a contemplative graphical language for logical sentences. In his article on Begriffsschrift [F+79, §6], he already presented how to write inferences by stacking formulas. However, in order to do inferences, we need rules of inference to know what can follow from what, and we also need hypotheses left unproven (at the top on the inference). These statements are called *axioms*. Frege justifies them informally by their *self-evidence* and how they appear in the practice of mathematics. For instance, this is how Frege justifies the axiom $A \Rightarrow (B \Rightarrow A)$:

> This is evident, since A cannot at the same time be denied and affirmed. We can also express the judgment in words thus, "If a proposition A holds, then it also holds in case an arbitrary proposition B holds". Let A, for example, stand for the proposition that the sum of the angles of the triangle A BC is two right angles, and B for the proposition that the angle ABC is a right angle. Then we obtain the judgment "If the sum of the angles of the triangle A BC is two right angles, this also holds in case the angle A BC is a right angle."

> — Gottlob Frege [F+79, §14]

Another notable axiom is the statement $c = c$ stating that all statements are equal

<footnote n="13">¹³You can ask Pablo Donato about it, he likes to talk about Peirce.</footnote>
to themselves (because they refer to the same concept). All statements which are not
axioms are inferred by using the following inference rules (in modern notations):

◇ **Modus ponens.** From *A* and *A* ⇒ *B*, we can infer *B*;

◇ **Generalisation.** From *A* ⇒ *P(x)* where *x* does not occur in *A*, we can infer *A* ⇒ ∀*x*.*P(x)*.

§2.6 Formal consideration of linguistic features led to several new notations for logic. It is not so clear how these notations were introduced, how they have been propagated and how they evolved. The most common notations have already been presented in Figure 1.3. Hence, a sentence such as “Either *A* is true or it is not” would be written *A* ∨ ¬*A*. The quantified formulas of Frege are written ∀*x*.*A* for “for all *x*, *A* holds” and ∃*x*.*A* for “there exists some *x* such that *A* holds”, although these notations were introduced by different people at different times. Properties are expressed with *predicate symbols* which are used like function symbols. For instance, we write *P(t)* to say that the property *P* holds for some term *t* and it produces a statement which is either true or false. Frege also had a notion now called *second-order quantification* [F+79, §27] which corresponds to a quantification over predicates or formulas (which are predicates with no argument). For instance, ∀*A*.*A* ∨ ¬*A* would be a second-order formula.

§2.7 **Logicism.** Frege’s philosophical project is called *logicism*. Logicism’s hope was to reduce some (or if possible, all) parts of mathematics (especially arithmetic) to logic, which is understood as “pure relations between concepts”. This cold-hearted point of view sees logic as connexions between evidences. It attracted a great attention from mathematicians such as Giuseppe Peano, Richard Dedekind and Alfred North Whitehead which became active contributors but it is usually considered that the project has been mainly carried by Bertrand Russell. Logicism is also related to *analytic philosophy* which studies philosophy with an emphasis on linguistics and the use of mathematical tools.

§2.8 Logic turned into syntax. At this point, logic is defined as if humans were somehow able to experience logic and materialise intuitions of it into syntactic objects. Unfortunately, this approach is far from being trouble-free. What logicians have done was trying to frame the practice of mathematics into syntax. We will see that mathematical practice is not so obedient and can escape from the jails we design.

**3 Paradoxes and the jails of the Format**

§3.1 An antinomy is a mutual incompatibility between two rules. It is probably the most pathological phenomenon in logic. Several antinomies began to appear when trying to capture some parts of mathematics with formal logic. An early appearance of antinomy, even before these considerations is the Burali-Forti<fnref n="14" /> paradox (1897) which came to the

<footnote n="14"><sup>14</sup>It's actually one person and not two.</footnote>
conclusion that a naive formalisation of set theory leads to antinomies [BF97]. This
paradox<fnref n="15" /> concerns a generalisation of numbers called *ordinals*. Assuming the existence
of a set of all ordinals leads to the existence of an ordinal greater than itself, which is
absurd. It is thought that Cantor, considered as the inventor of set theory, was informally
aware of this fact.

§3.2 The most famous example of antinomy is probably Russell's paradox [Rus03, Chapter X] which can be seen as a simpler version of the Burali-Forti paradox (it seems that it has even been suggested by Burali-Forti himself). We write $x \in y$ to formalise the fact that the entity $x$ is contained in the entity $y$ and $x \notin y$ when it is not the case. Sets can be written *extensively* as a collection of elements, such as $\{1, 3, 7\}$. We can for instance write $1 \in \{1, 3, 7\}$, $2 \notin \{1, 3, 7\}$ or even $\{1\} \in \{\{2\}, \{1\}\}$ (if we would like to base mathematics on set theory, then numbers have to be encoded as sets). It is then technically possible to write $x \notin x$ (although it seems absurd, it holds for the set $\{1\}$ as we do not have $\{1\} \in \{1\}$). Now, it is possible to collect all such elements not containing themselves, written $y = \{x \mid x \notin x\}$, to be read “the set of $x$ such that $x \notin x$”. The contradiction appears when we are trying to ask the forbidden question “Does $y$ contain itself?” written “$y \in y''$”. If $y \in y$ holds, then $y$ is part of the sets which do not contain themselves by definition of $y$. It is contradictory! Then $y \notin y$ must hold. However, if it is the case, it should have been part of the collection of sets not containing themselves. Which is also contradictory with our hypothesis... This formulation of set theory is known as *naive set theory*.

§3.3 An immediate and natural solution to that antinomy, provided very early by Russell himself in his *The principles of mathematics* (1903), which has been then developed with Whitehead in *Principia Mathematica* (1910), is to say that our definitions were too permissive and that we need to put constraints on them. It makes sense because such contradictions do not reflect the practice of mathematics. These different ways of constraining the use of syntactic entities (typically, forcing categories to prevent some syntactic manipulations or inferences) led to different branches of logic with their own culture and practices.

§3.4 **Type theory.** This solution suggested by Russell corresponds to what is now called *type theory*. We classify entities so that unexpected uses are prevented. In this approach, the root of evil is the notion of *impredicative definition*. The Russell's paradox contains a vicious circle related to self-reference. The variable $x$ in {$x \mid x \notin x$} is a generic variable referring to the set of all sets, including itself. In order to avoid this illicit contact, Russell classified the entities of set theory with a hierarchy of types so that some entities cannot interact which each other. Russell's idea was to design a hierarchy of levels so that, when writing $x \in y$, $x$ must be at level $n$ and $y$ at level $n+1$. It is then impossible to write $x \in x$ because $x$ cannot be both at level $n$ and $n+1$. Another way to understand this approach is that Russell's paradox can also be understood as the fact that there is

<footnote n="15">¹⁵As Girard exposed very often in his writings, we could say antinomy instead since it is a contradiction with the definitions and not something simply “out of dogma” as the name suggests.</footnote>
no set of all sets. This hierarchy of levels actually has a consequence on mathematical
definitions since several definitions are impredicative but used without problems (such
as the definition of greatest lower bound) but also because the use of predicate becomes
limited by our restrictions (we do not have access of all predicates anymore). Several
attempts at having a more nuanced approach to those constraints came later, such as
Russell's *ramified hierarchy* motivated by a fear of these vicious cycles rather than the
initial need to avoid a leakage caused by antinomies.

§3.5 **Axiomatic.** Another solution for a logical foundations of set theory is to rely on axioms (cf. Paragraph 2.5) to clearly express what is allowed or not, which is indeed a quite *military* solution<fnref n="16" />. Axiomatic systems existed for a long time (e.g. Euclid's axioms for geometry) but they were given a greater importance at the time of the crisis of mathematical foundations. Also as early as Russell (1908), Ernst Zermelo suggested an axiomatic theory for set theory known as Z which has later been extended to ZF, then to the so-called ZFC axiomatic system. By choosing axioms in a clever way and on which mathematicians agree, it is possible to produce a trustworthy foundation for set theory and some (if not all) parts of mathematics. For instance, the first axiom is the *axiom of extensionality*, written $\forall x.\forall y.(\forall z.(z \in x \Leftrightarrow z \in y)) \Rightarrow (x = y)$ with modern notations of formal logic. It means that if two sets contain the same elements, then they are equal. The use of axioms forbids unwanted statements such as Russell's paradox. Adding more axioms allows to express more complex mathematical theory but coherence of the new set of axioms must be ensured. Actually, although axiomatic is interesting for foundational purposes, it barely affects mathematical practice.

4 The location of certainty: the mind or the paper?

§4.1 The appearance of paradoxes challenged the logicist project of capturing parts of (or all) mathematics with formal logic. This period of the early 20th century, known as the *foundational crisis of mathematics*, gave rise to *metamathematics* which is the study of mathematics by using mathematical methods. Two important schools of thought (both opposing the previous logicist project) appeared during this crisis: the *formalists* (often represented by Hilbert) and the *intuitionists* (often represented by Brouwer). Those two schools of thought, together with logicism, represented by Russell, were the most important schools of logic at that time.

§4.2 One thing on which those two schools of thought did not agree was the nature of mathe-
matics and the *location* of certainty. Logicism is often associated with *semantic realism*
which considers an external reality of mathematical meaning, independent from us and
to which we can refer. For instance *x* = *y* when *x* and *y* "refer to the same meaning".
Intuitionism and formalism are two rivals opposing logicism and returning to Kant's
seeking for an immanent logical meaning. A way to understand the difference between

<footnote n="16">¹⁶As often pointed out by Girard.</footnote>
formalism and intuitionism is to ask whether the nature of mathematics is to be found
in our mind or our paper.

**§4.3 Intuitionism.** For intuitionists, mathematics is a purely mental activity; a production of the human mind [BP84, Chapter 2]. Language is used as a way to communicate mental constructions. Certainty lies in what is accessible by the human mind and which can be constructed and communicated. Although innocent, this conception of logic has important consequences such as the doubt of some logical statements which were considered valid. Typically, the excluded middle "A or not A" which states that any statement is either true or false. If we are able to prove that A is false (by assuming it and showing that it leads to a contradiction), A must be true. In the particular case of existential statements "either there exists x such that P or there is no x such that P" for a property P, it happens that using the excluded middle allows us to infer the existence of some mathematical entities although they are mentally out of reach: we cannot construct them and yet we assert their existence. What we need is an explicit construct that we call an *existential witness* which is an intelligible proof of existence. This leads to serious doubts about all statements logically equivalent to the excluded middle. This divides logic into two categories: *intuitionistic logic* excluding these statements and *classical logic* which allows them.

**§4.4 Formalism.** Hilbert thought of logic as a *formula game*. His approach is more procedural and perhaps more *conventionalist*. All philosophical questions aside, mathematical practice mainly involves syntactic operations related to "fixed rules known to all mathematicians" [BP84, Chapter 3]. Certainty lies in the *purity of syntax* (the paper, in some sense). The idea of Hilbert's programme was to prove and verify statements by finite and mechanical means<fnref n="17" />. In formalism, there is no strong reason to reject the problematic classical statements which were rejected by intuitionism. These statements are part of mathematical practice. What is important are not the statements but the methods of proofs and then mathematics becomes a "combinatorial game" [BP84, Chapter 3]. Contradiction can be represented with a symbol $⊥$. Formalists are then especially interested in the property of *coherence* stating that we cannot produce the symbol $⊥$ with a given system. In some sense, formalists' logic is only about syntax and conventions.

**§4.5 Proof systems.** Frege's calculus of Paragraph 2.5 constitutes an example of proof system which is able to *prove* statements from previously assumed statements. Proof systems are the key for the Hilbertian ideal of a finite and mechanical verification of statements. Logic would then be *procedural* and *bureaucratic*. In its modern form, using modern notations for formulas instead of Frege's Begriffsschrift, Frege's calculus is called *Hilbert system*. A *proof* becomes a mathematical object which can be studied by itself. It is simply defined as a sequence of formulas following some given rules and which starts with a given set of axioms. It is also possible to begin with more axioms depending on the mathematical theory we would like to consider (which also allows for hypothetical

<footnote n="17">¹⁷In particular, he also had the ambition of reducing infinitary mathematics to finitary ones (one can argue that in some cases infinitary reasoning is not necessary).</footnote>
<table><caption>Figure 4.1: Proof of $A \Rightarrow A$ from the two axioms $A_1 := A \Rightarrow (B \Rightarrow A)$ and $A_2 := (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))$ together with the modus ponens (MD) as only rule (from $A$ and $A \Rightarrow B$, we can infer $B$). These rules are taken from a proof system called $H_1$ which is presented in a course of Stony Brook University (https://www3.cs.stonybrook.edu/~cse541/chapter8.pdf).</caption><thead><tr><th>Line</th><th>Statement</th><th>Justification</th></tr></thead><tbody><tr><td>1</td><td>((A ⇒ ((A ⇒ A) ⇒ A))) ⇒ ((A ⇒ (A ⇒ A)) ⇒ (A ⇒ A)))</td><td>by A<sub>1</sub></td></tr><tr><td>2</td><td>A ⇒ ((A ⇒ A) ⇒ A)</td><td>by A<sub>2</sub></td></tr><tr><td>3</td><td>(A ⇒ (A ⇒ A)) ⇒ (A ⇒ A)</td><td>by MD(1,2)</td></tr><tr><td>4</td><td>A ⇒ (A ⇒ A)</td><td>by A<sub>1</sub></td></tr><tr><td>5</td><td>A ⇒ A</td><td>by MD(3, 4)</td></tr></tbody></table>

statements assumed to be true). An example of a proof of $(A \Rightarrow A)$ from a minimal set of axioms and rules is given in Figure 4.1. Representing mathematical proofs as mathematical objects allows for an analysis of reasoning but also allows results about proofs themselves (cf. Paragraph 4.1 for metamathematics). Several proof systems have been developed afterwards such as Gentzen's natural deduction and sequent calculus [Gen35a, Gen35b]. As we will see later in this thesis, proof systems became essential for their connexion with (typed) programming in computer science.

# 5 Syntax and semantics / Language and reality

§5.1 A dominant point of view in today's logic is to explain the logical activity by a separation between syntax (what we write) and semantics (what we mean). In a lot of beginner books or in university courses, logical systems are presented from their syntax then from their semantics. It became so systematic that it is now quite cliché. When I studied logic, I identified mathematical logic and *logic* in general but we should keep in mind that mathematical logic is *one possible implementation of logic which is dependent of some traditions and history*. Hence, mathematical logic is a *part of logic*, far from a definitive answer to the (philosophical) nature of logic. This dominant conception of mathematical logic assumes a direct access to reality (semantics) by language (syntax) but also an identification of reality with some mathematical semantic theories (typically, truth interpretation).

§5.2 It is possible to do logic both in the syntax and the semantic world. In the syntax, we typically have proof systems and axiomatic systems. We have formulas and infer other formulas according to some given rules. We write $\Gamma \vdash_S A$ when $A$ can be inferred from a set of formulas $\Gamma = \{B_1, ..., B_n\}$ in some system $S$. We can write $\vdash_S A$ when $A$ is provable without any assumptions (for instance simply from the axioms of $S$). In semantics, we are interested in the meaning of symbols by evaluating expressions. For instance, the expression $A \lor \neg A$ where $A$ is true can be evaluated to the truth value 1
(representing truth). The evaluation gives value of the whole expression by computing
the truth value of its components. We write $\Gamma \models A$ when the truth of formulas in $\Gamma$
implies the truth of $A$. We simply write $\models A$ when $A$ is a tautology (vacuously true for
any truth value of its components). Mathematical theorems correspond to tautologies.
Several semantic theories with more complex mathematical interpretations also exist
such as having three truth values, theory of all possible worlds (Kripke semantics) etc.

**§5.3 Soundness and Completeness.** Now that we can do logic in two different worlds, we need results about the correspondence between them: that the logic of syntax exactly corresponds to what we mathematically mean.

* The first property we usually require is *soundness* which states that $\Gamma \vdash_S A$ implies $\Gamma \models A$ or in other words that our procedural system of symbols is correct (sound) *w.r.t.* our conception of meaning.

* The second property is *completeness* which says that $\Gamma \models A$ implies $\Gamma \vdash_S A$, or in other words that all what we mean is faithfully captured by syntactic operations.

These properties appear in a lot (if not most) papers about logic. As for the *consistency* property of Paragraph 4.4, it is indeed a syntactic property: the fact that we cannot infer a special symbol $\perp$ representing contradiction, or more formally $\not\vdash_S \perp$.

**§5.4 First incompleteness.** Despite the ambitions of formalism and logicism, it is considered that Gödel's *incompleteness theorems* [Göd31] made these two projects almost obsolete. There are often confusions about what Gödel's theorems really say. The informal idea is that Gödel's result is a sophisticated version of the *liar paradox* (explicitly mentioned by Gödel). In natural language, we can assert that "the statement X is false". In the space of all statements which can replace X, there is... the previous statement itself! We obtain "*this* statement is false". If it is true then it is contradictory because it says it is false. But if it is false then it is consistent with what the statement says, then it must be true. There is a mismatch between the external commentary on sentences and the meaning associated with syntactic expressions.

**§5.5** I refer to Smith's book for more technical details [Smi13]. To give more context, there was hopes at giving logical foundations to arithmetic for natural numbers. Peano's arithmetic was an attempt at providing a finite set of axioms from which all valid arithmetic statements would be inferred. Let $T$ be a set of axioms capturing arithmetic. By only using natural numbers, it is possible to encode various statements. For instance, it is known that there is a bijection between $\mathbb{N}$ and $\mathbb{N} \times \mathbb{N}$, hence natural numbers can encode pair of natural numbers. With this idea of encoding, Gödel managed to construct a statement $G_T$ of $T$ stating "$G_T$ is unprovable in $T$". Gödel's first incompleteness theorem is the following:

1. neither $G_T$ nor $\neg G_T$ are provable in $T$. Hence, there exist statements for which provability is impossible to decide with a finite and mechanical procedure. This ends Hilbert's formalist ambition;
2. if $T$ is consistent then $G_T$ is true (the contradiction $\perp$ cannot follow from the rules of $T$).

If we assume $T$ to be consistent, then $G_T$ is true (2) but not provable (1). Hence there exists at least one statement in $T$ which is true and not provable. This exhibit a gap between truth and provability. In some sense, $T$ is *incomplete* (hence the term “incompleteness”). But more than incomplete, it is *incompletable* (to quote Smith) because providing $T$ is expressive enough to express arithmetic, it is always possible to construct such unprovable formulas even if we extend it with more axioms. Although it sounds serious, it mostly affects the logical foundations of arithmetic and not mathematical practice (since we usually do not end up with those weird problematic statements).

**§5.6 Second incompleteness.** We write $C_T$ for “$T$ is consistent”. The second condition of Gödel’s first incompleteness theorem says that $C_T$ implies $G_T$. The reasoning behind the proof of the implication $C_T \Rightarrow G_T$ can actually be encoded in arithmetic. It appears that $C_T \Rightarrow G_T$ is provable in $T$ (by using arguments we do not detail but which are given by Smith [Sm13]). When $T$ is assumed to be consistent, then by the second condition of Gödel’s first incompleteness, $G_T$ cannot be proven. It follows by $C_T \Rightarrow G_T$, that $C_T$ cannot be proven as well, otherwise we would be able to prove $G_T$ (notice that this does not affect the provability of the implication). Gödel’s second incompleteness theorem is a corollary coming from this reasoning, which says that if $T$ is consistent then it cannot prove its own consistency (the statement $C_T$). This is again a barrier against the total, mechanical and finitistic justification of mathematics hoped by formalists.

**§5.7 Gödel's hierarchy.** It would be exaggerated to say that this is the end of formalism. If Hilbert's ideal cannot be fully realised, some parts of it can still be saved. Even though the consistency of a formal system cannot be shown inside it (if it is expressive enough), it can be shown in stronger systems. There is a hierarchy of systems: we say that $T < T'$ when the consistency of $T$ can be shown in $T'$. It is then possible to design several variant of arithmetic or axiomatic theories and form a whole hierarchy of formal systems. Reverse mathematics, founded by Harvey Friedman [Fri75, Fri76], searches for the sufficient axioms to express some mathematical theories (it is a *reverse* approach in the sense that it starts from mathematical practice to reach axioms instead of starting from given axioms). From this new approach, it is possible to study the mathematics which are “finitistically” meaningful or reducible to finite mathematics [Sim88]. In particular, a system known as PRA (Primitive Recursive Arithmetic) embodies all of finitistic mathematics [Tai81].

**§5.8** This is the end of this historical introduction. Now, I suggest formal presentations of the ideas described until now. These presentations are strongly influenced by my own education on logic. I start from a modern formalisation of stoic logic known as *propositional calculus* and extend it to obtain richer logical systems. Then proof systems for these systems are formally presented.
# 6 Propositional calculus

§6.1 The propositional calculus can be understood as turning stoic logic (cf. Paragraph 1.6) into a system of symbols. We fix a set **Atoms** of atomic statements called **atoms** (these are stoics' assertibles), written with lower case letters **a**, **b**, **c**, **d** etc. From propositions, it is possible to construct more complex statements called **formulas** or **propositions**:

* if $a \in \text{Atoms}$, then $a$ is a formula;
  ◇ **Example of sentence:** "the sky is blue".

* if $A$ is a formula, then $\neg A$ is a formula (negation);
  ◇ **Example of sentence:** "the sky is not blue".

* if $A$ and $B$ are formulas, then $A \wedge B$ is a formula (conjunction);
  ◇ **Example of sentence:** "the sky is blue and the grass is green".

* if $A$ and $B$ are formulas, then $A \vee B$ is a formula (inclusive<fnref n="18" /> disjunction);
  ◇ **Example of sentence:** "the sky is blue or the grass is green" (both can be true).

* if $A$ and $B$ are formulas, then $A \Rightarrow B$ is a formula (implication).
  ◇ **Example of sentence:** "if the glass falls then it breaks".

§6.2 This description of formulas is often compactly described by what computer scientists call a *grammar* (cf. Appendix A.3), defining how a formula (written $A$ or $B$) can be constructed:

$$ A, B ::= \quad a \mid \neg A \mid A \wedge B \mid A \vee B \mid A \Rightarrow B \quad \text{(Formulas)} $$

where $a$ is an atom.

§6.3 The problem now is that formulas such as $\neg A \vee B$, $A \Rightarrow B \Rightarrow C$ or $A \vee B \wedge C$ are ambiguous and can be read in different non-equivalent ways. It is then common to proceed to a *militarisation* of syntax by specifying exactly what string of characters are considered well-formed formulas. We will simply allow to put parentheses around connectives to write clearer presentations of formulas and define priorities between connectives:

* If $A$ and $B$ are formulas, then $(\neg A)$, $(A \wedge B)$, $(A \vee B)$ and $(A \Rightarrow B)$ are formulas.

* The order of priority is: $\neg$, $\wedge$, $\vee$, $\Rightarrow$ (for instance $\neg A \vee B$ is equivalent to $(\neg A) \vee B$).

* Binary connectives are *right-associative*, meaning that $A \Rightarrow B \Rightarrow C$ is equivalent to $A \Rightarrow (B \Rightarrow C)$ and idem for the connectives $\wedge$ and $\vee$.

<footnote n="18">¹⁸Stoics’ original “or” connective was *exclusive*, meaning that only one statement has to be true and not both. With the *inclusive* disjunction, both can be true.</footnote>
<table><caption>Figure 6.1: Truth table defining the values of $\neg A$, $A \wedge B$, $A \vee B$ and $A \Rightarrow B$ with respects to the value of A and B.</caption><thead><tr><th>A</th><th>B</th><th>¬A</th><th>A ∧ B</th><th>A ∨ B</th><th>A ⇒ B</th></tr></thead><tbody><tr><td>0</td><td>0</td><td>1</td><td>0</td><td>0</td><td>1</td></tr><tr><td>0</td><td>1</td><td></td><td>0</td><td>1</td><td>1</td></tr><tr><td>1</td><td>0</td><td>0</td><td>0</td><td>1</td><td>0</td></tr><tr><td>1</td><td>1</td><td></td><td>1</td><td>1</td><td>1</td></tr></tbody></table>

§6.4 Now that we have symbols, we have to interpret them (and thus define their semantics). A proposition is expected to be either true or false (respectively represented by the numbers 1 and 0). Formulas are evaluated by a function $\llbracket \cdot \rrbracket$ providing the meaning of symbols. For instance, if both $a$ and $b$ are true, we expect $a \wedge b$ to be true as well. Let $\Omega: \text{Atoms} \to \{0,1\}$ be a function called *valuation* associating a truth value to propositions.

§6.5 **Definition** (Interpretation of propositional formulas). We define the *interpretation* of a formula with respects to its components as follows:

• $\llbracket a \rrbracket_\Omega = \Omega(a)$ with $a \in \text{Atoms}$ (we directly access the truth value of the atom);

• $\llbracket \neg A \rrbracket_\Omega = 1 - \llbracket A \rrbracket_\Omega$ (the value is inverted);

• $\llbracket A \wedge B \rrbracket_\Omega = \min(\llbracket A \rrbracket_\Omega, \llbracket B \rrbracket_\Omega)$ (true only when both values are true);

• $\llbracket A \vee B \rrbracket_\Omega = \max(\llbracket A \rrbracket_\Omega, \llbracket B \rrbracket_\Omega)$ (only false when everything is false);

• $\llbracket A \Rightarrow B \rrbracket_\Omega = \llbracket \neg(A \wedge \neg B) \rrbracket_\Omega$.

§6.6 There is an alternative way to describe the meaning of formulas called *truth tables* (Figure 6.1). It is a mechanical way to compute the truth of a formula from the truth values of its components. However, if you have $n$ variables in a formula $A$, then you need $2^n$ steps to compute $\llbracket A \rrbracket_\Omega$. If you have only 8 variables, it is already 256 steps! Fortunately, there are now several ways to evaluate formulas more efficiently for a computer (SAT solvers).

§6.7 **Implication.** The case of implication has to be made clear because it looks quite mysterious (and very confusing for beginners). The intended meaning for $A \Rightarrow B$ is that it is a law of causality from $A$ to $B$. It is expected that $A \Rightarrow B$ is false only when this causality is violated. If both $A$ and $B$ are true then the causality holds. If $A$ is false then it does not violate the fact that $A$ being true must implies the truth of $B$ follows. The only possible violation of causality is that $A$ is false but $B$ is true. Hence, the meaning of $A \Rightarrow B$ is that it is impossible to have both $A$ true and $B$ false, which can be written as the incompatibility $\neg(A \wedge \neg B)$.
§6.8 From this simple presentation of logic, it is possible to exhibit some interesting equivalences appearing in logic (for instance, the fact that $\neg\neg A$ is equivalent to $A$, which should not be too surprising):

◇ **Involution of negation.** $[\neg\neg A]_{\Omega} = 1 - (1 - [A]_{\Omega}) = 1 - 1 + [A]_{\Omega} = [A]_{\Omega}$;

◇ **De Morgan law I.** $[\neg(A \lor B)]_{\Omega} = 1 - \max([A]_{\Omega}, [B]_{\Omega}) = \min(1 - [A]_{\Omega}, 1 - [B]_{\Omega}) = \min(\neg A, \neg B) = [\neg A \land \neg B]_{\Omega}$;

◇ **De Morgan law II.** $[\neg(A \land B)]_{\Omega} = 1 - \min([A]_{\Omega}, [B]_{\Omega}) = \max(1 - [A]_{\Omega}, 1 - [B]_{\Omega}) = \max(\neg A, \neg B) = [\neg A \lor \neg B]_{\Omega}$;

◇ **Commutativity.** $[A \land B]_{\Omega} = [B \land A]_{\Omega}$ (and same for $\lor$);

◇ **Associativity.** $[(A \land B) \land C]_{\Omega} = [A \land (B \land C)]_{\Omega}$ (and same for $\lor$);

◇ **Contraposition.** $[A \Rightarrow B]_{\Omega} = [\neg B \Rightarrow \neg A]_{\Omega}$;

§6.9 A question which naturally comes to mind is “do we capture all possible functions on truth values?” How can we express more complex formulas such as exclusive disjunction or equivalence between formulas? Actually, our system is already powerful enough to speak about any combination of truth we wish. For instance, we could also define:

◇ **Exclusive disjunction.** $A \oplus B := (A \lor B) \land \neg(A \land B)$;

◇ **Equivalence.** $A \Leftrightarrow B := (A \Rightarrow B) \land (B \Rightarrow A)$.

§6.10 Restricting connectives to few ones (for instance negation and conjunction) is sufficient to retrieve the other connectives. Such set of connectives are said to be *functionally complete*. Here are some examples of functionally complete sets of connectives:

• From $\{\neg, \land\}$: $A \lor B := \neg(\neg A \land \neg B)$ and $A \Rightarrow B := \neg(A \land \neg B)$;

• From $\{\neg, \lor\}$: $A \land B := \neg(\neg A \lor \neg B)$ and $A \Rightarrow B := \neg A \lor B$;

• From $\{\neg, \Rightarrow\}$: $A \land B := \neg(A \Rightarrow \neg B)$ and $A \lor B := \neg A \Rightarrow B$.

It is even possible to have a unique connective: $\{\uparrow\}$ is functionally complete for $A \uparrow B := \neg(A \land B) \equiv \neg A \lor \neg B$ called “Scheffer stroke”. Such functions are usually attributed to Henry M. Sheffer in 1913 [Sch65] although Peirce<fnref n="19" /> had similar (unpublished) results in 1880.

§6.11 Formulas true for any valuations are called *tautologies*, *theorems* or *valid formulas*, and the ones which are always false are called *antilogies* or *contradictions*. For instance, it is easy to check with a truth table that $a \Rightarrow a$ or $\neg\neg a \Leftrightarrow a$ are tautologies, and that $\neg(a \Rightarrow a)$ which is equivalent to $\neg a \land a$ is an antiology. In particular, $a \Rightarrow a$ which states that a statement implies itself, is equivalent to $\neg a \lor a$ stating that any statement is either true or false. We write $|\models A$ when A is a tautology and $|\nvDash A$ when it is not (note that it does not necessarily mean that it is an antiology).

<footnote n="19">¹⁹It seems that Peirce independently anticipated a lot of things.</footnote>
§6.12 If $\not\models A$, then we must have some valuation which makes the formula $A$ false. This corresponds to the idea of *counter-example*. To show that a statement is not true, we have to provide a situation for which it is false. For instance, $\not\models a \Rightarrow b$ because if $a$ is true but $b$ is false, it makes the whole formula $a \Rightarrow b$ false.

§6.13 Tautologies are actually generic statements which are true whatever the truth values we put on the atoms. Actually, for that reason, it is even possible to replace atoms by *any formula* and it would still hold. Mathematically speaking, if $\models A$ then $\models A\{a := B\}$ where $a$ is an atom of $A$ and $A\{a := B\}$ is $A$ after replacing all occurrences of $a$ by some formula $B$. This is called the *substitution lemma*. This shows that there is a slight confusion about the generic nature of tautologies. Although we state tautologies about specific atoms, they actually holds for any statements replacing the atoms. This idea of genericity will only be clear later, in second-order logic.

§6.14 **Logical constants.** A common extension of the propositional calculus is to turn the truth values into constants of the language of formulas itself. We consider two constants 1 (true) and 0 (false) such that $[1]_\Omega = 1$ and $[0]_\Omega = 0$ for any $\Omega$. Truth values behaves like neutral elements: we have $[A \lor 0]_\Omega = [A]_\Omega$ and $[A \land 1]_\Omega = [A]_\Omega$. This allows to consider *closed formulas* which are independent of an interpretation of variables and which can be interpreted as such.

# 7 Predicate calculus

§7.1 Predicate calculus is the logic underlying Frege's Begriffsschrift (cf. Paragraph 2.4) and it embodies the paradigm of Frege's philosophy in the sense that we distinguish a class of *individuals* represented by *terms* with which we associate a *meaning* in some given *universe*. For instance, the symbol *a* may represent *Aristotle* and *f(a)* may refer to Aristotle's father. We then reason about properties on individuals with symbol called *predicates* associated with a boolean function. For instance, we can define a predicate *H* to represent the property of being human, which returns either *true* or *false* when given an individual as argument. The formula *H(a)* then expresses the fact that Aristotle is a human.

§7.2 **Definition (Relational signature).** A *relational signature* is a tuple $\mathbb{R} = (V, PR, F, \mathbf{ar})$ where $(V, F, \mathbf{ar})$ is a signature (cf. Appendix B) and $PR$ is a set of function symbols called *predicate symbols* such that $\mathbf{ar}$ is defined on $PR \uplus F$.

§7.3 **Definition (Formula of predicate calculus).** Let $\mathbb{R} = (V, PR, F, \mathbf{ar})$ be a relational signature. Formulas are defined by the following grammar where $t_1, ..., t_n$ are terms (cf. Appendix B), $P \in PR$ is a predicate symbol such that $\mathbf{ar}(P) = n$ and $x \in V$ is a variable:

$$ A, B ::= P(t_1, ..., t_n) \mid \neg A \mid A \land B \mid A \lor B \mid A \Rightarrow B \mid \forall x.A \mid \exists x.A \quad (\text{Formulas}) $$
§7.4 **Example.** The term $f(a)$ presented above can be defined in a signature $\mathcal{S} = (V, F, \mathbf{ar})$ where $V = \emptyset$, $F = \{f, a\}$, $\mathbf{ar}(f) = 1$ and $\mathbf{ar}(a) = 0$. The formula $H(a) \Rightarrow H(f(a))$ is defined on relational signature $\mathbb{R} = (V, PR, F, \mathbf{ar})$ where $V = \emptyset$, $PR = \{P\}$, $F = \{f\}$, $\mathbf{ar}(H) = 1$, $\mathbf{ar}(f) = 1$ and $\mathbf{ar}(a) = 0$.

§7.5 Because of the presence of variables, it can happen that a variable is not related to a quantifier such as in $\forall x.P(x, y)$. Such variables are said to be *free*. It is still possible to interpret these formulas by providing an interpretation of free variables but to keep things simple, we will simply exclude formulas containing free variables. Such formulas are called *closed formulas*.

§7.6 **Definition (Free variables and closed formulas).** Let $A$ be a formula. We define inductively the set $fv(A)$ of its free variables:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
fv(P(t_1, \dots, t_n)) = \bigcup_{i=1}^{n} \mathbf{vars}(t_i) & fv(\neg A) = fv(A) & fv(A \land B) = fv(A) \cup fv(B) \\
fv(A \lor B) = fv(A) \cup fv(B) & fv(A \Rightarrow B) = fv(A) \cup fv(B) & \\
fv(\forall x.A) = fv(A) - \{x\} & fv(\exists x.A) = fv(A) - \{x\} &
\end{array}
$$

We say that $A$ is *closed* when $fv(A) = \emptyset$.

§7.7 What we do in predicate calculus is turning some linguistic features into symbols in a more articulate way than in propositional calculus. For instance, the expression “*all flowers are beautiful*” would be represented by a single atom in propositional calculus but could be represented by the more accurate $\forall x.F(x) \Rightarrow B(x)$ in predicate logic. Reality is thought to be accessed by putting into words what we can express by language. Accordingly to Frege’s philosophy, symbols refer to some reality. This is represented by the notion of *structure* which interprets symbols in a specific universe (e.g. the universe of numbers, humans etc).

§7.8 **Definition (Structure).** Let $\mathbb{R} = (V, PR, F, \mathbf{ar})$ be a relational signature. An $\mathbb{R}$-structure $S$ (or simply a *structure* when the signature is implicit) is a tuple $(U, I)$ where $U$ is a non-empty set of elements called the *universe* (or *domain*) and $I$ is an *interpretation function* defined on $PR \uplus F$ such that it associates a function $I(f) : U^n \to U$ for function symbols $f \in F$ such that $\mathbf{ar}(f) = n$ and a relation $I(P) : U^n \to \{0, 1\}$ for predicate symbols $P \in PR$ such that $\mathbf{ar}(P) = n$.

§7.9 **Example.** The atom $H(a)$ can be interpreted in the structure $S = (U, I)$ where $U = \{\mathbf{Aristotle}, \mathbf{Plato}, \mathbf{Rock}\}$ and the interpretation is defined by $I(a) = \mathbf{Aristotle}$ and $I(H)(x) = 1$ when $x \in \{\mathbf{Aristotle}, \mathbf{Plato}\}$ and 0 otherwise. It can also be interpreted in a structure $S' = (U', I')$ where $U' = \mathbb{N}$, $I'(a) = 0$ and $I'(H)$ is the parity predicate.
§7.10 We usually consider formulas implicitly closed since they are the only ones which will be considered in our definitions.

§7.11 **Definition** (Interpretation of closed formulas). The interpretation of a closed formulas w.r.t. a structure $S = (U, I)$ is defined as follows:

• $[[P(t_1, ..., t_n)]_S = I(P)(I(t_1), ..., I(t_n));$

• $[[\forall x.A]]_S = \min_{t \in U} [[\{x := t\}A]]_S;$

• $[[\exists x.A]]_S = \max_{t \in U} [[\{x := t\}A]]_S;$

• the other connectives are defined as in propositional logic.

We require that {$x := t$}A is A for which all occurrences of x are replaced by a term t.

§7.12 **Remark.** We have $[[\forall x.A]]_S = [[\neg(\exists x.\neg A)]]_S$ and $[[\exists x.A]]_S = [[\neg(\forall x.\neg A)]]_S$.

§7.13 We write $M \models A$ for a structure $M$ and a formula $A$ when $[[A]]_M = 1$ and say that $M$ is a *model* of $A$. In case it is not a model of $A$, we simply write $M \not\models A$. For instance, given the model $M$ of the previous example, we have $M \models H(a)$ because $[[H(a)]_M = I(H)(I(a)) = I(H)(\text{Aristotle}) = 1$. If for a given formula $A$, there exists a model $M$ such that $M \models A$, we say that $A$ is *satisfiable*. If there exists $M$ such that $M \not\models A$, we say that $A$ has a *counter-model*. As in propositional calculus, a formula of predicate calculus is a *tautology* or *valid* when $M \models A$ for any model $M$, which can be written $\models A$.

§7.14 **Equality.** The equality predicate which is essential in mathematics becomes a mere binary predicate = which is true if and only if the inputs correspond to identical objects in a given structure, i.e. $\models [[a = b]]_S$ for $S = (U, I)$ when $I(a) = I(b)$. It shows that equality in syntax is just the reflection of equality in semantics. It is fair to ask whether it is a right definition or not considering how important equality is in mathematics. Is it right to define it simply as a symbol like other ones? It looks like we are only delegating the problem of equality in syntax to the implicit equality of semantics.

§7.15 Do quantifiers really add something more than propositional calculus? Universal quantification can naturally be seen as a *n*-ary conjunction over the *n* elements of a structure. For instance, the formula $\forall x.P(x)$ can be encoded by the formula $\bigwedge_{i=1}^n P(a_i)$ for a structure of *n* elements $a_1, ..., a_n$. This poses no problem for the finite case and the two formulas are equivalent. However, for the case of infinite models, we have to switch to *infinitary propositional logic* [Moo97] instead. Even in this case, universal quantification and infinitary conjunction are different. For instance, the formula $\bigwedge_{i=1}^\infty P(a_i)$ only has infinite models for constants $a_1, a_2, ..., $, but $\forall x.P(x)$ can be true in finite models as well as infinite models. Predicate calculus actually subsumes propositional calculus. If we remove quantifiers and restrict predicates to the nullary case only (no argument), we exactly obtain propositional calculus. Universes must also be restricted to the set $\{0, 1\}$ so that structures corresponds to a truth interpretation.
§7.16 **Empty models.** Let us now discuss about a small but important detail: the exclusion of non-empty models. Actually, this is a technical requirement. Consider an empty model $M_\emptyset = (\emptyset, I)$. If we have a universal formula $\forall x.P(x)$, it states that $P$ is true for all $x$ in the model. But what happens if the model is empty? It is usually considered that $M_\emptyset \models \forall x.P(x)$. This can be justified by the fact that $1$ is the neutral elements for $\wedge$ or that it is impossible to find an element of the model for which $[P(x)]_{M_\emptyset} = 0$ which would contradict the formula. In particular, we have $M_\emptyset \not\models (\forall x.P(x)) \Rightarrow (\exists x.P(x))$ because the premise is true but not the conclusion. The problem is that this formula is actually provable in usual proof systems (in syntax). This makes the correctness formula *false* in this case. The usual (ad-hoc) solution is simply to forbid the empty model. This choice does not seem to be philosophically justified.

## 8 Second-order logic

§8.1 It happens in the practice of mathematics that we need to quantify over predicates. For instance the formula $\exists P.P(a)$ states that there is some predicate $P$ which holds for the constant $a$. Since unary predicates can be seen as set of individuals (for which the predicate holds), extending quantification to predicates corresponds to quantifying over sets, which is strictly stronger than predicate calculus. In Tarskian terms, set theory can be chosen as a metalanguage for second-order logic (but other semantic theory can be chosen as well).

§8.2 Second-order logic<fnref n="20" /> corresponds to predicate calculus extended to quantification over predicates. It has also been introduced by Frege who introduced the expression of second-order ("zweiter Ordnung" in German) [Fre82, §53]. When considering the restriction to the propositional case (using nullary predicates), the quantification applies on propositions and the atomic formulas correspond to variables. For this reason we use a notation of variable in the following definition of the second-order formulas.

§8.3 The formulas of second-order logic are defined by the following grammar:

$$A, B ::= \quad X_i(t_1, ..., t_n) \mid \neg A \mid A \wedge B \mid \forall x.A \mid \forall X_i.A \quad (\text{Formulas})$$

where $X_i$ is a predicate symbol, $t_1, ..., t_n$ are terms and $i \in \mathbb{N}$. It is sufficient to restrict the formulas to universal quantification since existential quantification can be retrieved by Remark 7.12. In the same fashion, the set of connectives $\{\neg, \wedge\}$ is functionally complete (cf. Paragraph 6.10) and is thus sufficient to express $\vee$ or $\Rightarrow$.

§8.4 For the interpretation of closed second-order formulas, we extend interpretation of predicate calculus (cf. Definition 7.11) to an interpretation of predicate symbols by sets (the

<footnote n="20">²⁰I remember a presentation where Gilles Dowek (jokingly) said that he did not know what second-order logic was since he did not understand what *first-order* logic was.</footnote>
set of all terms for which the represented property holds). However, as we saw in Section 3, invoking the set of all sets is problematic. Either some properties cannot be represented or we have to choose another foundation (using type theory for instance). We leave all these foundational discussions aside.

§8.5 **Example.** In second-order logic, the predicate even corresponding to even natural numbers is interpreted by the set of all even natural numbers {$n | \exists k \in \mathbb{N}, n = 2k$}.

§8.6 **Definition (Interpretation of closed second-order formulas).** The interpretation of a closed second-order formula w.r.t. a structure $S = (U, I)$ is defined as follows:

• $[\forall X_i.A]_S = \min_P [\{X_i := P\}A]_S$ where P is a predicate, and

• other connectives are interpreted in the same way as for predicate calculus.

§8.7 **Indiscernibility principle.** Second-order logic enjoys a different (and more interesting notion of equality). Instead of a simple binary predicate, equality can be defined with the following second-order formula:

$$a = b \text{ is defined as } \forall X.X(a) \leftrightarrow X(b)$$

meaning that $a$ and $b$ are considered equal when they cannot be distinguished for all properties, or in other words, that all property satisfied by $a$ are satisfied for $b$ and vice-versa. This is usually attributed to Leibniz and even called *Leibniz's law* for that reason:

• the implication $(a = b) \Rightarrow (\forall X.X(a) \leftrightarrow X(b))$ is known as *indiscernibility of identities* and is trivial<sup>21</sup> (replace $a$ by $b$ or the converse and you obtain the identity $A \leftrightarrow A$);

• the converse implication $(\forall X.X(a) \leftrightarrow X(b)) \Rightarrow (a = b)$ is more controversial because of whether or not it is a sufficient principle of individuation. Distinguishing individuals strongly depends on what we mean by property. Are we considering all possible properties? If so, then we are implicitly invoking the forbidden set of all sets. If not, how are we choosing our properties? As Girard remarked [Gir18b, Section 2.1], in $a = a$, one symbol is on the left and the other on the right but no predicate takes spatial position into account. Is it considered logically irrelevant? Why?

In fact, Leibniz's notion of indiscernibility was a metaphysical concept which had nothing to do with formal logic and the correspondence with Leibniz's original thought may be exaggerated. For that reason, I choose to not call this logical principle Leibniz's law but indiscernability principle instead.

<footnote n="21"><sup>21</sup>In its philosophical forms, it is rejected by Peter Geach who consider a notion of relative equality.</footnote>
§8.8 Peano arithmetic. Peano arithmetic which has often been discussed in the context of formal logic is naturally expressed as a second-order theory. All axioms except the last one are statements of predicate calculus. The last axiom expresses induction over natural numbers, which allows to prove a general statement P for all natural numbers only from the base case P(0) and the propagation P(n) ⇒ P(n + 1). In other words, we have:

$$ \forall X. (X(0) \land (\forall n. X(n) \Rightarrow X(n + 1))) \Rightarrow \forall n. X(n) $$

We call PA2 Peano arithmetic with second-order induction. A consequence of Gödel's incompleteness theorem is that second-order logic cannot be both sound and complete since it can express Peano arithmetic. However, these properties are valid for predicate calculus which also enjoys additional properties (e.g. compactness theorem). For that reason, the last axiom is often replaced by infinitely many axioms of predicate calculus for each predicate P (countably many):

$$ (P(0) \land (\forall n.P(n) \Rightarrow P(n + 1))) \Rightarrow \forall n.P(n) $$

Peano arithmetic with this infinite axiom scheme is called PA. Since there are countably many predicates in predicate calculus and uncountably many ones in second-order logic, PA2 is theoretically more expressive than PA (some second-order predicate cannot be represented in predicate calculus). However this has no serious effect in practice.

§8.9 Although full second-order logic is too powerful, it is possible to have alternative weaker semantics for which we can retrieve properties we wish for. Reverse mathematics (cf. Paragraph 5.7), for instance, studies subsystems of PA2. For more details about the power and problems related to second-order logic, we refer to Väänänen's article on second-order logic [Vää19].

§8.10 It is possible to consider even stronger extensions of logic such as *higher-order logic* which quantifies over nested sets of arbitrary depth instead of simply sets of elements as in second-order logic. In particular, mathematics using quantification over general sets should be expressed in higher-order logic as predicate calculus is not sufficient.

# 9 Natural deduction

§9.1 In the following sections, I will only mention Gentzen's natural deduction and sequent calculus since they are the most relevant proof systems for this thesis. The idea is that we would like to represent a proof of a statement as a mathematical object. In Figure 4.1, proofs are sequences of operations following some rules but a more structural representation are *trees* since some rules can create several branches (the modus ponens referring to two previous assumptions). This section is inspired by Olivier Laurent's great course notes on proof theory (https://perso.ens-lyon.fr/olivier.laurent/thdem11.pdf).
<figure><img src="image_5.png" /><figcaption>Figure 9.1: Rules of intuitionistic natural deduction (NJ). We require that $x$ is not free in any hypothesis of the rule $\forall i$ and that $x$ is not free in neither $C$ nor any hypothesis for the rule $\exists e$. These requirements avoid weird behaviours related to variables such as identifying the reference of two variables which were previously pointing at different things. The expression $[A]_x$ corresponds to an infinite supply of occurrences of an assumed formula $A$. These assumptions have to be justified by specifying which rule introduced them. The $x$ in $[A]_x$ refers to a rule identified by a label $x$. A rule can be linked to any number of assumptions (including 0). These assumptions are called *discharged assumptions*.</figcaption></figure>

§9.2 We will only focus on logic without second or higher-order quantification because this is how proof systems are usually introduced.

Intuitionistic natural deduction

§9.3 Natural deduction has been introduced by Gentzen [Gen35a] as an alternative to axiomatic systems which would be more natural. Such a system should look like as much as possible as the “natural rules of logic”. The formulas we consider are defined by the following grammar:

$$A, B ::= X_i \mid \top \mid \bot \mid A \wedge B \mid A \vee B \mid A \Rightarrow B \mid \forall x.A \mid \exists x.A \quad i \in \mathbb{N}$$

where $\top$ and $\bot$ corresponds to constants for truth and contradiction. Rules are written several premise formulas on the top of a conclusion formula, separated by a horizontal line. The rules of natural deduction are presented in Figure 9.1. The rules are divided into two classes: *introduction rules* and *elimination rules*. An intuitive way to understand this separation is that introduction rules correspond to *defining* or *constructing* a logical
$$ \frac{\frac{[A \lor B]_1 \quad \frac{[A]_2 \quad \forall i_2}{B \lor A} \quad \frac{[B]_3 \quad \forall i_2}{B \lor A}}{\forall e(2, 3)} \quad \frac{B \lor A}{(A \lor B) \Rightarrow (B \lor A)} \Rightarrow i(1)}{A \lor B}$$

Figure 9.2: A proof of $(A \lor B) \Rightarrow (B \lor A)$ in natural deduction. The application of the rule $\Rightarrow i(1)$ needs to justify that there is some $A \lor B$ above which would imply $B \lor A$. The 1 shows that we found the required formula in the formula supply $[A \lor B]_1$ of identifier 1.

symbol (if you have $A$ and $B$, you can construct $A \land B$) and elimination rules define the use of logical symbols (if you have $A \land B$ then you can extract either $A$ or $B$). The rule $\Rightarrow e$ corresponds to the so-called modus ponens and show how we can use an implication.

§9.4 **Defined negation.** Remark that there is no rule for the negation $\neg A$. This is because the negation can be defined by $\neg A := A \Rightarrow \bot$. It is then sufficient to have rules for implication and contradiction. If we want to explicitly give the rules for negation (which would be redundant), we would have an introduction rule reaching $\bot$ from $[A]$ and inferring $\neg A$, and an elimination rule producing $\bot$ from $A$ and $\neg A$.

§9.5 I comment the rules of NJ (cf. Figure 9.1).

* For $\land$, we can either construct a pair or destruct it by extracting a component;

* The rule $\Rightarrow i$ allows to infer $A \Rightarrow B$ when you can reach $B$ with some $A$ existing somewhere above, and $\Rightarrow e$ is the modus ponens which allows to use an implication $A \Rightarrow B$ providing you can feed it with an argument $A$;

* The rules $\forall i_1$ and $\forall i_2$ make a statement more confusing<sup>22</sup> by encapsulating it in a more general structure so that they can be treated in a uniform way. For instance, a proof of $A$ and $B$ would be treated as the same entity $A \lor B$, thus hiding if it was a proof of $A$ or $B$. The rule $\lor e$ corresponds to case analysis. If we have proven $A \lor B$ then we can look at the possible case: either $A$ or $B$ is true but we do not know which one. If both lead to the same conclusion $C$ then $C$ can be inferred from the whole reasoning;

* The rule $\bot e$, corresponding to the explosion principle (cf. Paragraph 1.9), says that from a contradiction, anything can be said<sup>23</sup>;

* The rule $\vdash i$ introduces a statement considered trivially provable;

<footnote n="22"><sup>22</sup>Why would we do that, logically speaking? This rule will later be justified by its connexion with programming.</footnote>

<footnote n="23"><sup>23</sup>I give a brief explanation because people often find it confusing. Assume $A$ and $\neg A$ are true. Then $A \lor B$ must be true since $A$ is true in particular. But since $\neg A$ is true (and hence $A$ false), it follows that $B$ must be true.</footnote>
* The rule $\forall i$ says that a statement can be *generalised*. The rule $\forall e$ says that a general statement can be *instantiated* to a more specific case;

* The rule $\exists i$ says that if we have a witness $t$ for some formula $A$ then there exists some $x$ (which is $t$) such that $A$ holds for it (it is similar to the introduction of $\lor$). The rule $\exists e$ which is a bit more confusing behaves exactly like a generalised $\forall e$ rule.

§9.6 Proofs are trees constructed with those rules such that their leaves are formulas corresponding to assumptions. An example of proof is given in Figure 9.2. In particular, the formula $A$ alone (written $[A]_x$ for some $x$) is a proof by itself because it corresponds to assuming $A$, then having to prove $A$, which is trivial$^{24}$. We can finally remark that the only axiom that natural deduction allows is the identity $A \Rightarrow A$.

§9.7 When trying to construct a proof, there are two strategies which imply two different reading of rules. The bottom-up method starts from the conclusion and use rules from the bottom until reaching justified hypotheses only. It is especially natural for implications since the goal tells what hypothesis you need to introduce. This strategy is also called *goal-directed*. The other strategy uses a top-down reading of rules (it is also probably the most natural for mathematicians). We start from assumptions and try to reach a wanted goal. We then have to guess what hypotheses are necessary.

§9.8 Although this system is called “natural”, it is not exactly natural in the sense that it does not reflect the practice of mathematicians. Look at the rule $\forall i_1$. What mathematician would prove $A$ then forget that he proved $A$ by making it a proof of $A \lor B$? The same problem happens with $\exists i$. We actually lose information with these operations. We can also observe a duality between rules such as the elimination of conjunction and the introduction disjunction or the elimination and introduction of the universal and existential quantifiers. Those rules are not so innocent since they are what we call *irreversible rules*. When we wish to prove $A \lor B$ in a bottom-up strategy and *choose* either $A$ or $B$, we can do a mistake and obtain an unprovable goal. The same phenomena happens with $\exists i$ when choosing a wrong existential witness $t$. The provability is not preserved in a bottom-up use of rules. Moreover, the elimination for these connectives also has a quite weird shape. If we look at the rule $\forall e$ in Figure 9.1, the “flow of reasoning” seems bended: there is a path ending on $A \lor B$ then continuing to the conclusion $C$ and going up to the hypotheses $[A]_x$ and $[B]_x$ which are the connectives subject to the formula $A \lor B$ on which the rule is focussing. This *detour* looks like a compensation for the inability to produce $A$ and $B$ on the bottom (which would break the shape of tree) because of the rigid distinction between hypothesis and conclusion.

<footnote n="24">²⁴When I learned logic for the first time, I was very confused by these discharged assumptions. I thought that since you could start from any assumption without justification, anything could be trivially proven. You want to prove A? Well take a node A and it is done! But actually, either you have unjustified assumptions and they represent hypotheses in the context of an hypothetical reasoning, or assumptions are justified which means they have been correctly introduced by some rule</footnote>
<figure><img src="image_6.png" /><figcaption>Figure 9.3: Rules of intuitionistic natural deduction (NJ). We require $x \notin \mathbf{fv}(\Gamma)$ for $\forall i$ and $x \notin \mathbf{fv}(\Delta \cup \{C\})$ for $\exists e$. The expression $\sigma(\Gamma)$ is the permutation of the order of the formulas in $\Gamma$ given by some function $\sigma$.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Figure 9.4: Shape shifting from the vertical and horizontal (sequents) presentations of rules. Inspired by a picture I once saw in a presentation of Elaine Pimentel.</figcaption></figure>

**§9.9 Sequents.** If you try to prove some statements by yourself, you will probably find that the rules are not very handy to write proof trees. Consider that you want to prove $(A \lor B) \Rightarrow (B \lor A)$ as in Figure 9.2. Either you start from the top and assume $A \lor B$ and try to reach $B \lor A$, which is not very convenient when you want to write a tree (from the root to the leaves) or you start from the bottom but then you have to keep somewhere that you assumed $A \lor B$. We will see that it is even less convenient when considering *classical logic*. Another style of rules also suggested by Gentzen [Gen35a] is to use *sequents* which are expressions $\Gamma \vdash A$ where $\Gamma := \{A_1, ..., A_n\}$ is a set of formulas representing hypotheses. This expression asserts that from $\Gamma$, it is possible to infer $A$. It is expected to have the same meaning as the formula $(A_1 \land ... \land A_n) \Rightarrow A$. The rules now handle sequents instead of formulas. By doing so, we can keep track of the hypotheses at the left of the symbol $\vdash$ (called “turnstile”). This change of proofs’ shape is illustrated in Figure 9.4. The rules for natural deduction in a sequent presentation are given in Figure 9.3. You can compare the two set of rules to convince yourself that they have the same meaning. As expected, the rule $\Rightarrow i$ only introduce the premise on the left part of $\vdash$. Now, since the assumptions are now located in the left part of $\vdash$ and not leaves anymore, we need another terminal rule which is the axiom $A \vdash A$ (as we said before in Paragraph 9.6, the identity is the only axiom considered). Because of this change we also need to represent the fact that we can use as many occurrences of a hypothesis as we want (this corresponds to the fact that a rule can be linked with several occurrences
$$ \frac{\begin{array}{c} \neg\neg A \\ A \end{array}}{A} \text{ dne} \quad \frac{\begin{array}{c} \Gamma \vdash \Delta, A, B \\ \Gamma \vdash \Delta, A \lor B \end{array}}{\forall i^m} \quad \frac{\begin{array}{c} \Gamma \vdash \Delta, A \lor B \\ \Gamma \vdash \Delta, A, B \end{array}}{\forall e^m} \quad \frac{\begin{array}{c} \Gamma \vdash \Delta \\ \Gamma \vdash \Delta, A \end{array}}{w_R} \quad \frac{\begin{array}{c} \Gamma \vdash \Delta, A, A \\ \Gamma \vdash \Delta, A \end{array}}{c_R} \quad \frac{\begin{array}{c} \Gamma \vdash \Delta \\ \Gamma \vdash \sigma(\Delta) \end{array}}{e x_R} $$

<figure><img src="image_8.png" /><figcaption>Figure 9.6: Proof of excluded middle for the two presentations of natural deduction (without and with sequents). Recall that we write $\neg A$ for $A \Rightarrow \bot$. Look at how it is much more complicated without sequent where it is not natural to write multiple conclusions. In the left proof, remark that we come back again to the goal $A \lor \neg A$ but together with the hypothesis $\neg(A \lor \neg A)$ which makes it provable.</figcaption></figure>

of a discharged assumption). For that reason, the structural rules $w_L$ (left weakening) and $c_L$ (left contraction) are introduced. We also have a rule $ex_L$ which exchanges the order of formulas (if we want to be very formal) but its use is usually left implicit.

**§9.10 Structural rules.** The weakening rule can be interpreted as making the goal “weaker” by adding useless hypotheses. In a bottom-up reading, it corresponds to erasing useless information when trying to prove a statement. The contraction corresponds to identifying two copies of a formula (top-down) or duplicating formulas (bottom-up). These operations are very common and natural: when trying to prove a statement, it happens that some information are not relevant or that we use several times the same hypothesis. This happens when proving the sequents $A, B \vdash A$ and $A \vdash A \wedge A$.
Classical natural deduction

§9.11 We presented a system for intuitionistic logic, a logic rejecting *classical rules* such as the excluded middle $A \lor \neg A$ (cf. Paragraph 4.3). If we try to give a derivation of $\vdash A \lor \neg A$, then we have to prove either $A$ or $B$, which is impossible for a generic statement $A$ we know nothing about. It is still possible to get the classical statements back:

• in the original notation without sequent, we can add a rule called *double-negation elimination* which infer $A$ from $\neg\neg A$ (which is equivalent to the excluded middle). It is also possible to simply add an axiomatic rule for the excluded middle;

• in the notation with sequent, we allow multiple conclusions and the meaning of a sequent $A_1, \dots, A_n \vdash B_1, \dots, B_m$ is $(A_1 \wedge \dots \wedge A_n) \Rightarrow (B_1 \vee \dots \vee B_m)$. In order to prove the excluded middle, we must consider an alternative (but equivalent) rule $\vee i^m$ for disjunction which infers $\Gamma \vdash A \vee B$ from $\Gamma \vdash A, B$.

This yields a system of *classical natural deduction* (NK). The additional rules to add for classical logic are given in Figure 9.5 and a proof excluded middle for the two presentations of NJ is given in Figure 9.6.

§9.12 But what changed by adding these rules? If we look at Figure 9.6, the rule dne over a formula $A$ (with conclusion $\neg\neg A$) allows the introduction of several occurrences of $A$ so that the proof can keep going without “loss of information” (if we use $\vee i$, it forces us to prove either $A$ or $\neg A$ and we lose the possibility to use the other). Similarly, for the sequent presentation, the new rules allow an occurrence of $A$ to be introduced as a hypothesis. Classical logic is related to the ability to save a goal for later and switch to another goal, or to *retract* during an attempt to prove a statement<fnref n="25" />.

§9.13 This ability to introduce hypotheses can actually be simulated in intuitionistic logic as well by considering Gödel's *double-negation translation*. Even though the excluded middle $A \lor \neg A$ is not provable, it appears that its double-negated version $\neg\neg(A \lor \neg A)$ is provable in intuitionistic logic. The first proof of Figure 9.6 corresponds to an intuitionistic proof of $\neg\neg(A \lor \neg A)$.

Proof reduction

§9.14 In natural deduction, if we introduce a connective then eliminate it, we obtain a redundancy since it is the same as just introducing it (as if we were computing $n + 1 - 1$). It should then be possible to eliminate such redundancies in order to obtain a simpler and irreducible final proof called the *normal form* of a proof. However, it is not so simple to

<footnote n="25">²⁵This idea has been illustrated by Wadler’s story of the Devil of excluded middle. The devil suggests an offer: (a) either he gives you a billion dollars (b) or anything you wish provided you give him a billion dollars. He chooses (b). You try to get a billion dollars after few years but then the Devil changes his choice and say that he chooses (a) instead and gives you a billion dollars.</footnote>
<figure><img src="image_9.png" /><figcaption>Figure 9.7: Proof reduction for NJ (presentation without sequent) with $k \in \{1, 2\}$.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 9.8: Example of commutative case of reduction for the rules $\forall e/ \Rightarrow e$ of NJ.</figcaption></figure>

do these proof reductions<sup>26</sup>. Reduction rules for NJ are given in Figure 9.7. The case of $\wedge$ corresponds to extracting a component from a pair we constructed. In the case of $\Rightarrow$, the proof is replaced by a proof of $A$ but instead of coming from the assumption $[A]_x$, it comes from the proof of $A$ on the right. All assumptions $[A]_x$ are then replaced by a proof of $A$: we have a substitution of proofs which multiply the size of the proof by the number of occurrences of $[A]_x$. In the case of $\forall$, we know that $A$ holds for some possible variables $x$ so we generalise it into $\forall x.A$ but then specialise it with some term $t$. We can reduce this to a proof of $\{x := t\}A$ which takes the proof of $A$ and replaces its occurrences of variables $x$ by $t$. The other rules behaves in the same ways as the rules previously described.

§9.15 There exists more subtle cases of reduction which does not correspond to redundancies introduced with an elimination rule following an introduction rule. They correspond to exchange of rules and are called *commutation cases* for that reason. An example of reduction for a commutative case is presented in Figure 9.8. The (problematic) rules

<footnote n="26"><sup>26</sup>Although it is called *reduction*, it is possible for the normal form to be bigger.</footnote>
concerned by these commutative cases are the irreversible rules $\vee e$, $\exists e$ and $\bot e$.

§9.16 **Links with computation.** Although this procedure of proof reduction looks innocent, it has deep connexions with computation as we will see later in this thesis. The reduction rule for $\wedge$ corresponds to constructing a pair and extracting a component out of it. The reduction for $\Rightarrow$ corresponds to activating a function by *inlining*, by copying its code and pasting it in the place of all the corresponding function calls. This will establish a formal correspondence between (intuitionistic) proof and (functional typed) programs, presented later in this thesis.

# 10 Sequent calculus

## Classical sequent calculus

§10.1 Gentzen's original goal was to establish consistency results for number theory but it seems that natural deduction was not very convenient for that purpose. For that reason, he introduced another proof system called *classical sequent calculus* (LK). In this system we also have rules handling sequents but instead of introduction and elimination rules, we only have introduction rules but which introduce formulas either on the left (as hypothesis) or on the right (as conclusion) of the symbol $\vdash$. Sequent calculus has redundancies since several sequent calculus proofs can correspond to a single natural deduction proof. As we will see, sequent calculus proofs allow a more fine-grained analysis of reasoning. As for the sequent presentation of NJ, a restriction of conclusion to a single formula yields intuitionistic sequent calculus (LJ). The rules of LK are presented in Figure 10.1a. As for natural deduction, we have identity rules (although one is added) and structural rules. Logical rules are divided into two equivalent variants: additive and multiplicative rules.

§10.2 **Additive and multiplicative rules.** Additive (marked with $a$) and multiplicative rules (marked with $m$) are two variants of the same logical concept. If we look at $\wedge R^m$ and $\wedge R^a$ in bottom-up reading, the former *splits* its contexts and the latter *shares* its contexts. Since structural rules (which are the same as for natural deduction) allow the erasure and duplication formulas, the two variants can be shown to be equivalent. This equivalence is illustrated by an example in Figure 10.3. This distinction emphasises the point of view of formulas as resources which is essential in linear logic. Duplicating formulas ensures that we will not have a shortage of resources and erasing formulas ensures that we get rid of superfluous information so that we can reach the axiom $A \vdash A$. In strictly linear logic which see formulas as *limited resources*, structural rules are forbidden$^{27}$ and multiplicative and additive rules become truly distinct logical concepts with their own handling of formulas, seen as resources.

<footnote>$^{27}$But allowed with more control in full linear logic.</footnote>
$$ \frac{\Gamma_1 \vdash A, \Delta_1}{A \vdash A} \quad \frac{\Gamma_2 \vdash A \vdash \Delta_2}{\Gamma_1, \Gamma_2 \vdash \Delta_1, \Delta_2} \quad \text{cut}^m \quad \frac{\Gamma \vdash A, \Delta}{\Gamma, A \vdash A, \Delta} \quad \frac{\Gamma \vdash A, \Delta}{\Gamma \vdash \Delta} \quad \text{cut}^a $$

(a) Multiplicative and additive identity rules.

$$ \frac{\Gamma \vdash \Delta}{\sigma(\Gamma) \vdash \sigma'(\Delta)} \quad \text{ex} \quad \frac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} w_L \quad \frac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} c_L \quad \frac{\Gamma \vdash \Delta}{\Gamma \vdash \Delta, A} w_R \quad \frac{\Gamma \vdash \Delta, A, A}{\Gamma \vdash \Delta, A} c_R $$

(b) Structural rules.

$$ \frac{\Gamma \vdash A, \Delta}{\Gamma, \neg A \vdash \Delta} \quad \neg L \quad \frac{\Gamma, A \vdash \Delta}{\Gamma \vdash \neg A, \Delta} \quad \neg R $$

(c) Rules for negation.

$$ \frac{\Gamma, A, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta} \wedge L^m \qquad \frac{\Gamma_1 \vdash A, \Delta_1 \quad \Gamma_2 \vdash B, \Delta_2}{\Gamma_1, \Gamma_2 \vdash A \wedge B, \Delta_1, \Delta_2} \wedge R^m \\ \frac{\Gamma_1, A \vdash \Delta_1 \quad \Gamma_2, B \vdash \Delta_2}{\Gamma_1, \Gamma_2, A \vee B \vdash \Delta_1, \Delta_2} \vee L^m \qquad \frac{\Gamma \vdash A, B, \Delta}{\Gamma \vdash A \vee B, \Delta} \vee R^m \\ \frac{\Gamma_1 \vdash A, \Delta_1 \quad \Gamma_2, B \vdash \Delta_2}{\Gamma_1, \Gamma_2, A \Rightarrow B \vdash \Delta_1, \Delta_2} \Rightarrow L^m \qquad \frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \Rightarrow B, \Delta} \Rightarrow R^m \\ \frac{\vdash \top}{\vdash \top} \top R^m \qquad \frac{\vdash \bot}{\vdash \bot} \bot L^m \qquad \frac{\Gamma \vdash \Delta}{\Gamma, \top \vdash \Delta} \top L^m \qquad \frac{\Gamma \vdash \Delta}{\Gamma \vdash \bot, \Delta} \bot R^m $$

(d) Multiplicative logical rules.

$$ \frac{\Gamma, A \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta} \wedge L_1^a \qquad \frac{\Gamma, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta} \wedge L_2^a \qquad \frac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \wedge B, \Delta} \wedge R^a \\ \frac{\Gamma, A \vdash \Delta}{\Gamma, A \vee B \vdash \Delta} \vee L^a \qquad \frac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \vee B, \Delta} \vee R_1^a \qquad \frac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \vee B, \Delta} \vee R_2^a \\ \frac{\Gamma \vdash A, \Delta}{\Gamma, A \Rightarrow B \vdash \Delta} \Rightarrow L^a \qquad \frac{\Gamma, A \vdash \Delta}{\Gamma \vdash A \Rightarrow B, \Delta} \Rightarrow R_1^a \qquad \frac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \Rightarrow B, \Delta} \Rightarrow R_2^a \\ \frac{\vdash \top}{\Gamma, \vdash \bot} \bot L^a \qquad \frac{\vdash \top}{\Gamma \vdash \bot, \Delta} \top R^a $$

(e) Additive logical rules.

$$ \frac{\Gamma, A \vdash \Delta}{\Gamma, \exists x. A \vdash \Delta} \exists L \qquad \frac{\Gamma \vdash \{x := t\} A, \Delta}{\Gamma \vdash \exists x. A, \Delta} \exists R \qquad \frac{\Gamma, \{x := t\} A \vdash \Delta}{\Gamma, \forall x. A \vdash \Delta} \forall L \qquad \frac{\Gamma \vdash A, \Delta}{\Gamma \vdash \forall x. A, \Delta} \forall R $$

(f) Rules for quantifiers. We require $x \notin fv(\Gamma)$ for $\forall R$ and $\exists L$.

<caption>Figure 10.1: Rules of classical sequent calculus (LK).</caption>
$$ \frac{\Gamma \vdash A, \Delta \quad \underline{\hspace{2cm}} \perp \underline{\hspace{2cm}} L^m}{\Gamma, \neg A \vdash \Delta} \Rightarrow L^m \qquad \frac{\Gamma, A \vdash \Delta \quad \underline{\hspace{2cm}} \perp R^m}{\Gamma, A \vdash \perp, \Delta \quad \underline{\hspace{2cm}} \perp \Delta} \Rightarrow R^m $$

<figure><img src="image_11.png" /><figcaption>Figure 10.3: Equivalence between additive and multiplicative conjunction. The double line represents multiple applications of a same rule.</figcaption></figure>

§10.3 I comment the interesting rules of LK (cf. Figure 10.1). It is mostly the rules of “probi-lematic” connectives such as $\vee$ and $\exists$ that change. The rules for $\wedge$ and $\forall$ are the same as in natural deduction.

* Notice the presence of a new rule: the *cut rule*. The cut rule takes its name from the fact that, in a top-down reading, the formula $A$ disappears during inference in order to connect two goals. The meaning of this rule is that if $A$ is proven in some context (left sequent) and that can be used in another context (right sequent), then we can continue the proof in the composition of these two contexts by using $A$. Hence, the cut is a *shortcut* using $A$ as a bridge in reasoning. This can also be understood as the use of a lemma $A$ in a bottom-up reading.

* The rules for negation $\neg$ can be confusing. They can actually be defined with $\neg A := A \Rightarrow \perp$ and other LK rules as shown in Figure 10.2 (hence they are redundant). The rule $\neg L$ says that if you can prove $A$ among other alternative goals $\Delta$, then it is valid to turn $A$ into an hypothesis $\neg A$. If $A$ was a provable goal, then the provability is given by contradiction, and otherwise a goal of $\Delta$ must be provable by validity of the disjunction. As for $\neg R$, if a goal is provable with $A$ as hypothesis, then it is valid to turn $A$ into a goal $\neg A := A \Rightarrow \perp$ which would introduce a hypothesis $A$ and an unprovable goal $\perp$ (but it does not matter since $\Delta$ was provable by itself);

* For the rule $\vee L^a$, remark that it is nicer than $\vee e$ because $A \vee B$ is allowed to appear on the bottom sequent (since it is introduced on the left and not eliminated from the top). Hence, we can do the same reasoning without “bending” the structure of the rule as for $\vee e$. The multiplicative variant $\vee R^m$ corresponds to classical disjunction which keeps the two goals available (hence removing the need for “data saving”).

* The rule $\exists L_a$ is similar to $\vee L^a$. If you can prove your goal with a generic $A$ then you should be able to prove it with the fact that there is some $x$ such that $A$ holds;
* The rule $\Rightarrow L^m$ still is modus ponens but in another form. If you are able to prove $A$ in some context and know that $B$ is the key argument to prove your goal $\Delta$, then you know that $A \Rightarrow B$ is a relevant tool to infer $\Delta$.

* The rule $\perp L^a$ corresponds to the explosion principle. If you have $\perp$ as hypothesis then your statement is vacuously proven.

**§10.4 Subformula property.** It appears that proofs of a sequent $\Gamma \vdash \Delta$ only use subformulas occurring in $\Gamma \cup \Delta$ *except* when the cut rule is present. This property is called *subformula property*<sup>28</sup>. The meaning of this property is rather profound: it means that everything we need is *already there*. A proof enjoying the subformula property does not rely on something else than subformulas of its conclusion. There is no need to summon something external to the proof (in our intuition or culture of mathematics for instance).

**§10.5 Cut-elimination theorem.** Gentzen's showed that the cut rule, representing the use of lemma in mathematical practice was in fact... useless. It can be eliminated, exactly like the redundancies of natural deduction. The proof of the cut-elimination theorem (also called *Hauptsatz*) gives rise to a procedure of proof reduction. Let us now mention why sequent calculus is interesting regarding semantic results. If there is a proof of $\perp$, then there must be a cut-free proof of $\perp$ (by cut-elimination). However, there is no cut-free proof of $\perp$ because of the subformula property (which is a key tool for the cut-elimination theorem) and because no rule introduces $\perp$. It follows that there cannot be a proof of $\perp$, which is the consistency property. We do not give the reduction rules since they are quite complicated. A simplification of LK will be presented later, in which reduction rules are way simpler.

**§10.6 Symmetry.** Notice how LK rules enjoy a very beautiful symmetry. The origin of this symmetry is the separation between left and right introduction rules. The rules $\neg L$ and $\neg R$ show that the symbol $\vdash$ acts as an inversion of *point of view*. This is due to involution of negation occurring in classical logic: we have $A = \neg\neg A$ (we can transfer a formula on the left then on the right or vice-versa and obtain the formula we started with). This duality appears in the left/right distinction of rules. The rule $\wedge R^m$ and $\vee L^m$ have the same operational behaviour except that the former works on the right and the latter on the left. Logical operations behave exactly like how our movements are reproduced by a mirror. A conjunction on the left is a disjunction on the right and vice-versa. The same phenomena occurs with the other rules of the pair $\wedge/\vee$ and $\forall/\exists$. It shows that it is technically possible to just put every formulas on the right with negation and forget half the rules we presented. This symmetry was not present in NJ because NJ enjoys a *top-bottom* symmetry. In Figure 9.1, look at how the elimination rules for $\wedge$ are upside-down versions of the introduction rules for $\vee$. However, as mentioned in Paragraph 9.8, this symmetry is not natural for elimination rules since we cannot produce two conclusions $A$

<footnote n="28"><sup>28</sup>It does not hold for NJ since some rules such as the elimination of disjunction $\vee e$ can introduce formulas which are not necessarily subformulas of $C$. For instance, if $C$ is always provable (e.g. $D \Rightarrow D$) then any formulas can take the place of $A$ and $B$, including formulas more complex than $C$.</footnote>
<figure><img src="image_12.png" /><figcaption>Figure 11.1: (Right) Monolateral rules of classical sequent calculus (LK). We require $x \notin fv(\Gamma)$ for $\forall$. I choose to exclude the additive axiom rule because we will not need it.</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 11.2: Proof of $((A \land B) \Rightarrow C) \Rightarrow (A \Rightarrow (B \Rightarrow C))$ in (right) monolateral sequent calculus. If we push negations, the formula becomes $\neg((A \land B) \Rightarrow C) \lor (A \Rightarrow (B \Rightarrow C)) = \neg(\neg(A \land B) \lor C) \lor (\neg A \lor (\neg B \lor C)) = (\neg(\neg A \lor \neg B) \land \neg C) \lor \neg A \lor \neg B \lor C = (A \land B \land \neg C) \lor \neg A \lor \neg B \lor C$.</figcaption></figure>

and $B$ (which would break to shape of tree) and have to *bend* the rule with an auxiliary formula $C$.

# 11 Monolateral sequent calculus

§11.1 **The logical space of interaction.** Thanks to the nice symmetries of LK and the fact that the symbol $\vdash$ acts like a mirror, it is possible to forget one side and just consider the other as suggested in Paragraph 10.6. If we take the remark seriously, this yields a *monolateral* sequent calculus. The rules of this new system are presented in Figure 11.1. Although it is possible to only consider formulas on the left, we usually consider formulas on the right. We obtain a unique rule for each connective and consider a multiplicative cut which is more standard. Sequents are therefore collections of formulas $\vdash \Gamma$. Working on this new calculus has few interesting consequences:
* there is no rule for negation (because no way to go the left of ⊢ anymore) and negation only appears on atomic formulas by pushing the negation with double-negation elimination (¬¬A ↝ A) and De Morgan's laws. The set of formulas becomes:

$$A, B ::= X_i | \neg X_i | A \land B | A \lor B | \forall x.A | \exists x.A \quad i \in \mathbb{N};$$

* a sequent is a sort of *space of interaction* where atomic formulas interact with their negation by the axiom rule;

* there is no distinction between a negated conclusion and a hypothesis. Input hypotheses can then be seen as *demand* for a formula and the axiom rule connects supply and demand;

* the implication $A \Rightarrow B$ must be defined as $\neg A \lor B$ since there is no hypotheses anymore.

I give an example of proof of monolateral sequent calculus in Figure 11.2.

§11.2 **A simpler analysis of sequent calculus.** Thanks to this monolateral version, it is possible to provide a simple interpretation of rules and logical principles.

◇ **Implication** If we look at $A \Rightarrow B = \neg A \lor B$, the bottom-up reading of the rule $\lor^m$ gives $\vdash \neg A, B$ which can be understood as the demand for A with B waiting in the space of interactions.

◇ **Cut rule** The cut rule joins two spaces of interaction along compatible formulas. It is similar as plugging a male cable with a female cable in electronics.

◇ **Conjunction** Multiplicative conjunction *splits* by distributing its interaction context whereas additive conjunction *shares* it. They are both equivalent thanks to structural rules.

◇ **Disjunction** Multiplicative disjunction $A \lor B$ keeps A and B separated but living in the same space of interaction whereas additive disjunction only keeps one side and deletes the other. They are both equivalent thanks to structural rules.

◇ **Neutral elements** The constant $\top$ corresponds to having a trivial goal and the constant $\bot$ corresponds to having an unprovable goal which can be discarded.

§11.3 **Comparing natural deduction and sequent calculus.** Something I find very instructive is how natural deduction rules can be translated into sequent calculus. First, introduction rules are exactly the same (nothing surprising) and only elimination rules are translated. Some cases of translation are presented in Figure 11.3. First, remark that a cut always appears. If elimination rules symbolise the *use* of a symbol, then cuts are also related to use. Actually, sequent calculus concentrates all the use of symbols in the cut rules and everything else is definition (introduction of symbols). Recall that cuts represent the use of a lemma, then sequent calculus turns the use of symbols into the use
$$ \frac{\Gamma \vdash A \wedge B \quad \wedge e_1}{\Gamma \vdash A} \rightsquigarrow \frac{\Gamma \vdash A \wedge B \quad \frac{\overline{A \vdash A} \quad \text{ax}}{A \wedge B \vdash A} \wedge L_1^a}{\Gamma \vdash A} \text{cut}^m \\ \frac{\Gamma \vdash A \vee B \quad \frac{\Delta_1, A \vdash C \quad \Delta_2, B \vdash C}{\Gamma, \Delta_1, \Delta_2 \vdash C} \vee e}{\Gamma, \Delta_1, \Delta_2 \vdash C} \rightsquigarrow \frac{\Gamma \vdash A \vee B \quad \frac{\overline{\Delta_1, A \vdash C} \quad w_L \quad \overline{\Delta_2, B \vdash C} \quad w_L}{\Gamma_1, \Delta_1, \Delta_2 \vdash C} \wedge L_1^a}{\Gamma_1, \Delta_1, \Delta_2 \vdash C} \text{cut}^m \\ \frac{\Gamma \vdash A \Rightarrow B \quad \frac{\Delta \vdash A \quad \overline{B \vdash B} \quad \text{ax}}{\Delta, A \Rightarrow B \vdash B} \Rightarrow L^m}{\Gamma, \Delta \vdash B} \Rightarrow e \rightsquigarrow \frac{\Gamma \vdash A \Rightarrow B \quad \frac{\overline{\Delta \vdash A} \quad \overline{B \vdash B} \quad \text{ax}}{\Gamma, \Delta \vdash B} \text{cut}^m}{\Gamma, \Delta \vdash B} \text{cut}^m $$

<caption>Figure 11.3: Translation of the rules $\wedge e_1$ and $\Rightarrow e$ of NJ (sequent presentation) into sequent calculus proofs. The double line represents multiple applications of a same rule.</caption>

of lemmas. The left premise of the cut defines/introduces a symbol and the right premise is a lemma explaining how that symbol is able to prove our goal. Sequent calculus is often said to be *analytic*: it decomposes the steps of natural deduction into more elementary operations. In particular, a natural deduction proof potentially corresponds to several different sequent calculus proofs<sup>29</sup> (permuting the order of rules for instance) while there are not so many possible choices in natural deduction proofs.

## Cut-elimination procedure

§11.4 In natural deduction, we are interested in removing redundancies coming from the elimination of previously introduced symbols. In sequent calculus, we only have introductions, hence these redundancies disappear. However, as we have seen in the previous translation of NJ into LJ (cf. Figure 11.3), elimination rules introduce cuts, hence the elimination of redundancies becomes the elimination of cuts. But more than that, consistently with the fact that redundancies somehow turned into uses of lemmas (which are essentially implications), cut-elimination will naturally looks like the elimination of redundancy for implication: lemmas will be *inlined*, i.e. their call is replaced by their proof, similarly to how convenient mathematical notations can be replaced by their more primitive definition. Cut-elimination is a procedure of *explicitation*. The main cases of cut-elimination are presented in Figure 11.4. A very intuitive computational explanation of these reduction rules can be given:

* the elimination ax/cut is an annihilation occurring when an axiom rule interacts with a cut rule, leaving only the other premise of the cut which was unrelated to the interaction;

<footnote n="29"><sup>29</sup>For that reason, natural deduction is seen as a quotient over sequent calculus proofs.</footnote>
$$
\begin{align*}
& \frac{\overline{\vdash \neg A, A}^{ax}}{\vdash A, \Gamma} \vdash A, \Gamma \quad \text{cut}^m \rightsquigarrow \vdash A, \Gamma \\
& \frac{\vdash \Gamma, A \quad \vdash \Delta, B \quad \vdash \Xi, \neg A, \neg B}{\vdash \Gamma, \Delta, A \wedge B} \wedge^m \frac{\vdash \Xi, \neg A \vee \neg B}{\vdash \Gamma, \Delta, \Xi} \quad \text{cut}^m \rightsquigarrow \frac{\vdash \Delta, B \quad \vdash \Xi, \neg A, \neg B}{\vdash \Gamma, \Delta, \Xi} \quad \text{cut}^m \\
& \frac{\vdash \Gamma, A_1 \quad \vdash \Gamma, A_2 \quad \vdash \Delta, \neg A_k}{\vdash \Gamma, A_1 \wedge A_2} \wedge^a \frac{\vdash \Delta, \neg A_1 \vee \neg A_2}{\vdash \Gamma, \Delta} \quad \text{cut}^m \rightsquigarrow \frac{\vdash \Gamma, A_k \quad \vdash \Delta, \neg A_k}{\vdash \Gamma, \Delta} \quad \text{cut}^m \\
& \frac{\vdash \Gamma, A \quad \forall \quad \vdash \Delta, \neg \{x := t\} A}{\vdash \Gamma, \forall x.A} \quad \exists \quad \frac{\vdash \Delta, \exists x. \neg A}{\vdash \Gamma, \Delta} \quad \text{cut}^m \rightsquigarrow \frac{\vdash \Gamma, \{x := t\} A \quad \vdash \Delta, \neg \{x := t\} A}{\vdash \Gamma, \Delta} \quad \text{cut}^m
\end{align*}
$$

<caption>Figure 11.4: Main cases of cut-elimination for the (right) monolateral sequent calculus.</caption>

$$
\frac{\frac{\vdash \Gamma, B, C \quad \vdash \Gamma_1, A, C, \quad \wedge^a}{\vdash \Gamma, A \wedge B, C} \quad \vdash \Delta, \neg C}{\vdash \Gamma, \Delta, A \wedge B} \quad \text{cut}^m \rightsquigarrow \frac{\vdash \Gamma, B, C \quad \vdash \Delta, \neg C}{\vdash \Gamma, \Delta, A} \quad \text{cut}^m \quad \frac{\vdash \Gamma, A, C \quad \vdash \Delta, \neg C}{\vdash \Gamma, \Delta, B} \quad \text{cut}^m \quad \wedge^a
$$

<caption>Figure 11.5: An example of commutation case in cut-elimination for LK.</caption>

• the elimination $\wedge^m/\vee^m$ is a rewiring on the premises: the left and right premises respectively interact with each other through an application of cut rule;

• the elimination $\wedge^a/\wedge^a$ corresponds to a choice. Two parallel possibilities are on the left and a selector is given on the right of the cut rule;

• the elimination $\forall/\exists$ corresponds to shifting the interaction between general statements to specific cases.

§11.5 In sequent calculus (independently from NJ's translation), most cases of cut-elimination are commutations. They occur in case a cut is applied on a formula which is not introduced by the last rule. For instance, in Figure 11.5, the cut rule is applied on C but it is A ∧ B which has been introduced in the left sequent. It intuitively corresponds to an interaction at distance, and which can be resolved by pushing the cuts up so that a direct interaction can be done, as if the interaction was obtruded.

§11.6 There are several ways to eliminate cuts and we just suggested one set of rules among others. The idea is always the same: suggesting another proof derivation with the same premises (possibly with duplications or unused premises) and the same conclusion. The reduced proof has to be "simpler". Some sets of cut-elimination rules are "better"
than others for some properties. An important property is termination which states
that applying the rules will ultimately ends on an irreducible cut-free proof. Another
property is confluence with states that when there are two ways to reduce a proof,
they ultimately ends on the same irreducible cut-free proof. This usually fails with LK
for the typical cut-elimination rules but it is possible to hack sequent calculus so to
get the desired properties. If you want more about confluence in sequent calculus, I
wrote a blog article with Farzad Jafarrahmani (https://prooftheory.blog/2021/09/
23/confluence-in-the-sequent-calculus/).

§11.7 Difference between implication and turnstile. What is the difference between $\vdash$ and $\Rightarrow$? Did not we say that they had the same meaning? Are we just adding superfluous notations? The expression $A \vdash B$ could be written $A \Rightarrow B$. It is semantically the same. However, sequent calculus would not exist anymore (not in this form at least) as $\vdash$ is a horizontal materialisation of the vertical distinction between hypothesis and conclusion occurring in natural deduction. This distinction is of a *procedural* nature, rooted in the dynamics of the *action of deduction*. The symbol $\vdash$ is part of the inference system or the “machine” while $A \Rightarrow B$ is just a syntactic object handled by the system which is moved back and forth. This difference can be observed in LK rules Figure 10.1. The rule $\Rightarrow R^m$ (which is the same as $\Rightarrow i$ in natural deduction) shows that it is possible to *freeze* the current reasoning $A \vdash B$ and turn it into a static and handleable token $A \Rightarrow B$. Moreover, cut-elimination (which holds all the computational dynamics of logic) only applies on sequents by annihilating formulas in two interacting sequents while the implication $A \Rightarrow B$ is only a *resource* which is added to this inference machine like adding an ingredient to a cooking pot. You can think of it as taking a photo: an instant is captured into something we can exchange, throw away or even duplicate. You can find a small discussion on this subject in Barbarossa's PhD thesis [Bar21, Section 5.3] (he is very fascinated by this distinction).

§11.8 **What about second-order?**. Second-order logic has not been mentioned in the pre-
vious technical chapters. If we would like to work with second-order logic, it is sufficient
to reuse the rules for first-order quantification and replace the first-order variable by a
second-order one. It works correctly when considering the syntactic part of logic but
is a bit more complicated and awkward if we would like to consider its relation with
a semantic interpretation. Moreover, it appears that we lose analyticity (sub-formula
property).

§11.9 **Returning to axiomatic.** If you still want to retrieve an axiomatic system using Gentzen's systems (which would betray his original goal), it is possible to consider a theory $\mathcal{T}$ (set of axioms). We then have additional axiom rules $\vdash_T \Gamma, A$ for $A \in \mathcal{T}$.
**12 Discussion: doubting traditions**

§12.1 I presented the big lines of what I call *traditions of logic*. However, some other people speak another “logical dialect”: they will say that their tradition of logic is *model theory* (that I did not mention much since it is not my field of expertise) or *computability theory*. Keep in mind that I am deeply influenced by my background of computer scientist.

§12.2 The formal vessel of logic emerged from empirical phenomena such as the *experience of regularities*; the fact that some phenomena we are able to describe by language have a consistent shape which can be freed from contingent information. Aristotle's logic was more concerned about the *shape* of reasoning while Stoic's logic was interested in the *decomposition* of statements. This already shows that there are several ways to formally capture the logical activity. And yet, we tend to take our formalisation of logic for granted. What makes our encapsulation of logic *right*? The explanation of the convenient syntax/semantics separation is that it is correct when the syntactic operations we defined conform to the semantics, *i.e.* the meaning we expect. Gödel's incompleteness shows that mismatches can occur between syntax and semantics<fnref n="30" />. This seems unsatisfying. On the top of that, semantics is basically just another syntax in an upper level, judging another lower-level syntax by a procedure of evaluation. To quote Girard's [Gir07, Section 5.1] cliché (and rather brutal) remark, such semantic explanations sound rather silly when we think about it: *A ∧ B* is true when the interpretation of *A* and *B* is 1 (being true). This shows how semantics mirrors syntax. Then, what justifies semantics apart from our hermetic and unintelligible intuitions? After all, where does our intuitions on logic even come from? With this semantic justification, we are not able to justify what we are doing unless we say that it is how the *laws of nature* are but then we are stuck with a definitive and limited answer about what logic is.

§12.3 **The role of intuition.** Any tradition should be doubted but their systematic rejection in a sort of *tabula rasa* is too extreme. We should ask ourselves if this logical folklore has a *reason to be*, if it can be *justified* at all. It makes no sense to get rid of traditions only because they are traditions (even when they are perpetuated without serious self-questioning). All these developments of logic are not a bunch of nonsense. They led to the developments of various practical tools and ideas now used in computer science. But even without this utilitarian point of view on logic, we *feel* that it is meaningful even if we cannot put words on it. Moreover, foundational issues actually barely affect mathematical practice. It is still impressive how natural deduction and sequent calculus, with their beautiful structures and properties, mainly emerged from rather vague intuitions about logic. I believe that our vague intuitions and our prejudices are still essential after all, even though logic is often seen as cold, exact and void of any feeling. Obviously, it is an error to take our intuition for reality as if logic was the circuits of reality, hard-coded in our brain, which we are somehow fully conscious of. Our vague intuitions, either right or wrong still guide us pretty well providing we learn to tame them.

<footnote n="30">³⁰If completeness is the fact that syntax is correct with respects to semantics, then incompleteness is the fact that it is not; that some parts of syntax exist without conforming to semantics.</footnote>
<figure><img src="image_14.png" /><figcaption>Figure 12.1: Natural deduction rules for tonk and a proof containing a redundancy. This proof can infer everything we want from any statement. Is it logical? If not, then why?</figcaption></figure>

**§12.4 The search for justifications.** The culprit is the *evaluative* nature of semantics. To evaluate logical objects means that we already have in mind how they should be and what they should mean. If an external and explanation of logic apparently cannot be found<fnref n="31" />, it may be possible to look for an *internal* explanation instead. But how can syntax explains itself? At a first glance, it makes absolutely no sense at all. The question of justification of logic has already been discussed by several philosophers. Regarding natural deduction, Arthur Prior [Ste61] asked why would not it be possible to consider a new connective “tonk” with the introduction rule of ∨ and the elimination rule of ∧. We would then be able to prove any statement (cf. Figure 12.1). We can conclude, like Prior did, that inference rules by themselves are not able to provide any logical meaning. Nuel Belnap [Bel62] and Michael Dummett [Dum91] thought that not all combinations of rules were “meaning-constituting”. The rules has to follow some constraints. Gentzen (although it was mainly studied by Dummett) introduced the term of “harmony” to describe the property of those inference rules which are meaning-constituting. The ideal objective would be to formalise Wittgenstein’s [Wit10] famous slogan “meaning is use” implying that the procedural operations done on logical symbols are sufficient to convey their meaning: we would then reach our internal explanation.

**§12.5** We already saw in the presentation of natural deduction that elimination rules intuitively correspond to the use of symbols. Then the possibility of reducing a redundancy might mean that the use of a symbol is *sound*, that it is possible to do something out of it (while preserving hypotheses and conclusion). Harmony is then probably related to a balance between introduction rule (definitions) and elimination rules (use of definitions). This idea gives an *utilitarian* and *computational* meaning to logical symbols. For instance, the meaning of conjunction would be its computational ability to construct pairs and extract its components. But then, our question reduces to “what proof reductions steps are valid?”. It is possible to hack the system so that our tonk connective can be reduced (for instance with a reduction similar to the case of ⇒ in Figure 9.7). In this thesis I show that a more satisfying answer is possible, providing we work in another logical architecture. If the subjective evaluative aspect of semantics asserting objectivity is faulty, then we shall go beyond evaluation. The key is to consider *mutual interaction* from which meaning will emerge.

**§12.6 Doubts about the unicity and plurality of logic.** In this chapter, I presented

<footnote n="31">³¹Unless we are able to directly communicate with God.</footnote>
classical and intuitionistic logic. But when we think about it, is logic not *unique*? When we say “it’s logical!” in our everyday life, to what logic do we refer to? Do not we refer to a *unique* logic? I now expose a personal and speculative point of view (which may be completely wrong) I have about the nature of classical and intuitionistic logic:

* *classical logic* can be reduced to a single connective $A \uparrow B := \neg(A \land B)$ called Scheffer's stroke. This connective basically express the *incompatibility* of two formulas *w.r.t.* to truth values; they cannot be true at the same time. Negation corresponds to the fact that a formula is incompatible with itself: $\neg A := A \uparrow A$. For the disjunction, it is false only when both inputs are false. This can naturally be expressed as the incompatibility $A \lor B := \neg A \uparrow \neg B$. Similarly, implication is the incompatibility between a true assumption and a false conclusion. Hence, we have $A \Rightarrow B := A \uparrow \neg B$ (as already explained in Paragraph 6.7). As for the fundamental equivalence $A \equiv \neg\neg A$, it is justified by the fact that the incompatibility of $\neg A$ and $\neg A$ is consistent with $A$. However, classical logic is not a mere calculus of incompatibility between individuals. If it is about incompatibility then it should be a *manichean* incompatibility: the excluded middle $A \lor \neg A$, says that anything is either true or false and it is expressed by the incompatibility $A \uparrow \neg A$ between A and its alter ego $\neg A$. The world is divided into two hermetic categories: whoever is not with me is against me<fnref n="32" />. Girard's alternative definition [Gir18b, Section 1.2] of the excluded middle ($A \equiv B) \lor (B \equiv C) \lor (C \equiv A$) accentuates this *social segregation*: among 3 propositions, two must be equivalent, you have no other choice. Although I do not investigate it, it is even possible to consider a logical system with Scheffer's stroke [Ten79]. Finally, what is a *classical proof*? Is classical provability simply asserting/resolving (in)compatibilities?

* In *intuitionistic logic*, the implication $A \Rightarrow B$ is primitive and cannot be defined by $\neg A \lor B$ since the translation actually relies on classical axioms. Intuitionism cannot be reduced to incompatibility. Forgetting $A \lor \neg A$ is like forgetting that some statements are incompatible as if we could not be sure about it. Instead, this limitation has the very nice property of forcing the unique conclusion formula to be justified/constructed: the limitation becomes an ability, a requirement for more information. This makes intuitionism about *functionality*: we focus, not on incompatibility but on the *process* or *actions* leading to some result. Intuitionistic logic can then be seen as actually stronger than classical logic in some sense since classical axioms can be encoded (cf. Paragraph 9.12). This surprising encoding seems related to the fact that functionality may be able to encode a space of incompatibility, as shown in the natural deduction proof on Figure 9.6 which is completed with two functional operations: *saving* the data $\neg(A \lor \neg A)$ (which is only possible with the wrapping of double negation) then *loading* it afterwards in the rightmost branch.

## §12.7 Doubts about the elementary logical operations. A reasonable doubt about logic

<footnote n="32">³²Which is apparently something shared by both Jesus and antifascist activists.</footnote>
is whether these natural notions of conjunction, disjunction, negation, implication and quantification constitute the *bedrock of logic*. Or can logical operations can be decomposed to reveal more primitive constructions? Girard's linear logic [Gir87a] shows that the implication $A \Rightarrow B$ can actually be decomposed as $!A \dashv! B$ where !A represent a potentially infinite amount of A and $A \dashv! B$ is a *linear implication* using its argument exactly once as if it was a limited resource. This offers a point of view of logic as *resources handling*. Moreover, if logic is related to natural language at all, it is fair to ask whether it is possible to represent other aspects of natural language (such as references, indexicals etc) without resorting to ad-hoc constructions (such as temporal modalities but what is ad-hoc, by the way?).

**§12.8 Doubts about predicate calculus.** As already remarked by Girard [Gir18b, Section 1], predicate calculus (cf. Section 7) is not a so natural extension of propositional calculus. A class of *individual*, distinct from logical entities, is introduced. They cannot hold a truth value but refer to some entity in a given universe. It is not clear what logically justifies such a distinct category apart from our own point of view (or prejudice in Girardian terms) on what logic should be. Another suspicious point is the exclusion of empty model (cf. Paragraph 7.16) which seems ad-hoc. Finally, equality is treated as a mere binary predicate but should not equality be a more fundamental notion?

**§12.9 Doubts about the undoubtable.** Finally, Girard dares to doubt about the most elementary things: the logical identity $A \Rightarrow A$ and the equality $a = a$. Doubting about such things (which were often considered axioms) makes no sense for most logicians and mathematicians. However, Girard suggests the idea that they actually reflect some preconceptions of logic [Gir18b, Section 2].

* For $A \Rightarrow A$, the idea is that it reflects Frege's philosophy of denotation. The two occurrences of A refer to the same entity. However, such paradigm is not sufficient to explain some phenomena occurring in sequent calculus such as the distinction between $\Rightarrow$ and $\vdash$ (cf. Paragraph 11.7). We have to take into account the cold aspect of sequent calculus and consider that it speaks about *actions on some locations*. It then appears that the two occurrences of A are two distinct entities at different locations but which are related. This is similar to how printers can copy a sheet of paper. The two sheets of paper are *distinct* but we can verify that one has the same content as the other: identity becomes something one has to prove. This will be more explicit when introducing Girard's proof-nets and transcendental syntax;

* as for $a = a$, in the same fashion, the two occurrences of $a$ are thought to refer to the same entity in a given universe. If we consider second-order equality (cf. Paragraph 8.7), in order to prove $a = a$, we would have to prove $X(a) \Leftrightarrow X(a)$ for any $X$ but this is trivial since $X(a) \Rightarrow X(a)$ by identity. However, as Girard pointed out, some properties are implicitly forbidden such as the fact of "being on the right" which indeed distinguishes the two occurrences of $a$. Ironically, it is as
if the “licit properties” were the ones satisfying our preconceptions about equality,
hence making equality trivial.

§12.10 A criticism of Truth and Reality. Everything being either true or false is a very
natural statement but if we take formal logic as presented in this chapter and forget
the metaphysical connexion between truth values (just symbols) and the philosophical
concept of truth, then what distinguishes 0 and 1? What makes 1 more *virtuous* than
0? They are distinguished because we choose that some statements are true (typically,
axioms). But is truth a matter of choice when I say that 1 + 1 = 2 is true and 1 + 1 ≠ 2
is not? There is an idea<fnref n="33" /> that axioms could be *proven* instead of simply *given*. But even
with this idea, absoluteness of truth cannot be found. Computer science could probably
give answers, for instance by saying that what is true is what can be computationally
materialised, *i.e*. what corresponds to some material reality (computation being the
ground of reality). If we step back from all our logical formalities, our formal conception
of logic presupposes a specific shape of reality. However, some parts of computational
reality are not captured by neither classical nor intuitionistic logic (as pointed out by
Girard in his commentary on Turing [TGBB95, Chapter 3] and the beginning of his
geometry of interaction project [Gir89b]).

* Chemical equations such as $2H_2 + O_2 \rightarrow 2H_2O$ consumes matter. But these equations abstract from details such as time or the environment so that what is kept is only the relation between concepts. Both classical and intuitionistic logic violates chemical principles as $A \Rightarrow A \land A$ (matter can be produced out of nowhere). Should we say that chemical reactions are not logical?

* In the same fashion, banks do a lot of operations which have to keep a certain consistency so that clients do not suddenly obtain or lose money by mistake. However, money is also an entity which can be consumed. Can we say that it has nothing to do with logic?

* Databases are able to store data such as clients registered in a bank. It is possible to update, add or remove data. However, if two data *A* and *B* are related in the database, either we have the truth of the statement expressing this relation (classical world) or a constructive proof of it (intuitionistic world). But in both cases, truth and provability are static and eternal properties which never die. What is true, is true forever (mathematical truth). How to treat the removal or update of data? But can we say that databases are simply not logical?

Girard's linear logic shows that it is possible to consider a logic of resources, thus giving a formal logical account to these ideas<fnref n="34" /> but his last project of transcendental syntax, presented in this thesis, shows that it is not the last answer yet.

<footnote n="33">³³ Already there at the time of Leibniz, according to David Rabouin.</footnote>

<footnote n="34">³⁴Actually, it is an a posteriori justification of linear logic. He discovered linear logic first in another context then tried to justify how interesting it actually was.</footnote>
# Chapter 2

## Computational panorama

After all this logical history of conflicts, ideals and failures, I would like to tell a whole new story: the story of computation. Like logic, computation is a natural phenomenon which has always “been there”. But it is only recently that it took a great importance. Unlike logic, it is a bit (only a bit) more clear what computation is about. Computation in its mature form also came way later. An amusing fact that computer scientists like to tell is that the theory of computation (and computers) existed way before computers themselves. Those computers being *everywhere* nowadays, it shows how of a great importance the study of computation is.

I start with few historical facts about computation then present the main classes of models of computation. Most definitions are inspired from Sipser's introduction to the theory of computation [Sip06]. This chapter sometimes refers to the previous chapter about logical foundations and is thus not completely independent.

## 13 The experience of procedurality

My main reference for this section is Dowek's book "Les métamorphoses du calcul" (in French).

§13.1 We only need time to realise an order in the succession of events. We sometimes are subject to some events. We are sometimes responsible of some events. We are sometimes also responsible of some events to which we are subject, or in other words: we can make some events happen. A typical example are methods described by a list of actions. It can be a cooking recipe or a method to solve a specific problem. Such methods can be shared so that other people can reproduce it, so there is a social aspect to it. It can be more or less precise and sensitive to an environment. For instance, for a cooking recipe, we may give more details about ingredients or leave the choice free. Those methods are called algorithms<fnref n="1" />.

<footnote n="1">¹Term thought to be derived from Al-Khwârizmî's name (a Persian mathematician) but the reality seems more nuanced than that, as stated by McLarty [McL08] (himself quoting Theseus Logic's website): "*The term algorithm was not, apparently, a commonly used mathematical term in America or Europe before Markov, a Russian, introduced it. None of the other investigators, Herbrand and*</footnote>
§13.2 A common example of an old algorithm<fnref n="2" /> is Euclid's algorithm which is the method computing the greatest common divisor of two integers. For instance, the set of common divisors of 36 and 30 is {1, 2, 3, 6} and the greatest is 6. Euclid's method is defined by the following steps for two positive integers *a* and *b*:

1. if $b = 0$ then the result is *a*;

2. otherwise, we compute the remainder *r* of the integer division *a* ÷ *b* and do the step 1 again with *a* := *b* and *b* := *r*.

We apply this algorithm on the inputs $a := 36$ and $b := 30$:

* the remainder of 36 ÷ 30 is *r* = 6 since 36 = 30 × 1 + 6;

* we have $a := 30$ and $b := 6$. The remainder of 30 ÷ 6 is $r = 0$ since 30 = 6 × 5 + 0;

* we have $a := 6$ and $b := 0$. Since $b = 0$, the final result is 6.

Algorithms are often related to the practice of mathematics as they provide a way to solve problems. However, notice that algorithms are actually *sensitive* to a context: I do not explain the method to do the integer division *a* ÷ *b*. You are free to choose any method you want providing it does *what it should do*. It is similar to not giving too many details about the tools in a cooking recipe, you just have to find something which does the job. In the case of the integer division ÷, your choice has to follow a particular specification implicitly given by the algorithm which defines what we mean by “integer division”.

§13.3 Logically speaking, algorithms provide an alternative way to prove mathematical statements. When having an existential statement $∃x.P(x)$, I need to find some element *x* that satisfies the property *P*. It is possible to prove it only by using logical means without ever knowing what that *x* looks like. But it is also possible to *construct* that *x*, called *existential witness*. Those constructions give rise to what we call *constructive proofs*. On the other hand, non-constructive proofs usually occur when using proof by contradiction (or equivalent rules such as the excluded middle). Proof by contradiction says that whenever you need to prove some statement *A*, you can virtually assume it to be wrong (assume $¬A$) and show that it leads to a contradiction only to infer at the end that *A* must be true (and that our initial assumption was impossible). By doing so, we do not construct an actual proof of *A* but take a sort of *logical detour*. This is connected to the ideas of *intuitionistic logic* (cf. Paragraph 4.3): proofs in intuitionistic logic correspond to constructive proofs and algorithms seem to be a way to construct such proofs.

<footnote>Gödel, Post, Turing or Church used the term. The term however caught on very quickly in the computing community.". Al-Khwârizmî's name indeed produced terms similar to "algorithm" but it initially referred to algebraic/numerical systems.</footnote>

<footnote n="2">²It has to be noted that although Euclid's algorithm is already a relatively old notion of computation, computational methods were not uncommon. I have heard from a presentation of Gilles Dowek in the Château de Goutelas (Summer 2022) that reasoning was exclusively computational before the Ancient Greeks.</footnote>
Those ideas of algorithms and constructive proofs were developed independently until
the middle of the 20th century.

§13.4 Similarly to logic, the theory of algorithms has been seriously developed rather late; around the 20th century when predicate calculus (cf. Section 7) was rising. But unlike logic which was studied since at least since the Ancient Greek, the theory of algorithms is a rather recent subject which took a great importance from its connexions with formal logic. Using predicate calculus, it is possible to represent mathematical statements with logical formulas. In particular, Euclid's algorithm is a way to prove the statement "c is the greatest common divisor of a and b" which can be represented by the atomic formula $GCD(a, b, c)$ or equivalently, by the formula $gcd(a, b) = c$ where $GCD$ is a predicate and $gcd$ is a function giving the greatest common divisor of two inputs. Algorithms become procedural ways to *prove logical statements*. Several other algorithms were developed to prove logical statements for arithmetic (or a fragment of arithmetic). For instance, Presburger developed a method to prove arithmetical statements for integers without multiplication.

§13.5 **Decision problem.** Given the procedural philosophy of formalists (cf. Paragraph 4.4), it is not surprising that questions between logic and algorithms were explicitly mentioned by Hilbert. Hilbert's *decision problem*<fnref n="3" /> asks for a mechanical and *effective* procedure to solve statements of predicate calculus. This method should always terminate with an answer in finite time. If such method exists, then mathematics (thought to be fully expressible in formal logic at this time) could be *mechanised*. Logic and mathematics would then be reduced to *pure computation*. More generally, given a function *f* taking a formula as input and answering either true (1) or false (0) is there a mechanical way to compute this function? This can also be generalised to any mathematical function. The main problem is that no mature notion of *computation* existed at that time.

§13.6 **Computation.** Alonzo Church and Alan Turing both independently came up (around the 30s) with a formalisation of computation, now called *model of computation*. Their answer was apparently influenced by Gödel's incompleteness theorems Paragraph 5.4.

* Church's proposal, is the λ-calculus [Chu32], a model of computation corresponding to a sort of *realisation* of mathematical functions. It is the ancestor of *functional programming*. It works with a functional language explicating the relation between input *x* and output *f*(*x*) for a function *f*;

* Turing's model is the famous Turing machine [Tur36] which formalises the intuitive idea of a mathematician writing on a piece of paper. Symbols can be written on paper depending on what is read on that same paper and the pencil can move either to the left or the right. To correctly model theoretical computation, we assume that we will never run out of paper. This is the ancestor of *imperative programming* where programs are sequences of instructions doing a specific task.

<footnote n="3">³ *Entscheidungsproblem* in German.</footnote>
Both models have been shown to be equivalent for functions over rational numbers. A function which can be computed in finite time by an expression of $\lambda$-calculus or a Turing machine is said to be *computable*. A formula $A$ is *decidable* when its associated function returning its truth value $f(A) \in \{0, 1\}$ is decidable. A lot of models of computation have been considered but the most powerful ones (Herbrand-Gödel's equations and Kleene's recursive functions) were all shown to be equivalent to Church and Turing's proposal. This defines a space of *computable functions*. Models equivalent to Turing machines are called *Turing-complete*.

**§13.7 Church's thesis.** Until now, no model of computation has been shown to be stronger than Turing-complete models in the sense that there would be a problem solved by some model but not by a Turing-complete one. This is *Church's thesis* (a term introduced by Kleene who was one of Church's students), also called *Church-Turing thesis*. Two notions are identified: Turing-complete models and the vague and intuitive notion of *computation*. This thesis (which is not a theorem) asserts that Turing-complete defines *the* notion of computation. Two versions of Church's thesis can actually be distinguished:

* the *physical variant* asserts that Turing-completeness captures the intuitive of computation by a physical system, hence it captures the concept of *natural computation*;

* the *psychological variant* asserts that Turing-completeness captures what is computable by the human mind, hence it captures the concept of *mental computation*.

The two variants are not necessarily equivalent depending on whether Nature computes more than humans or the opposite. This is the subject of a debate between Longo and Dowek known as the *Longo-Dowek controversy* explained in Yannis Hausberg's PhD thesis (not completed yet as I am writing this thesis). Other interesting related references are Longo and Paul's papers [LP11, PL09].

**§13.8 Partial recursive functions.** Still in the 30s, Kleene constructed (from works of Gödel and Herbrand) a mathematical theory of computable functions (which can be implemented by “effective procedures” such as $\lambda$-calculus and Turing machines). These functions, called *partial recursive functions* or ($\mu$-recursive functions), are constructed from the following primitive functions:

* constant functions $\text{Const}_n^k(x_1, ..., x_k) = n$;

* successor function $\text{Succ}(x) = x + 1$;

* projection functions $\Pi_i^k(x_1, ..., x_k) = x_i$

and closed under the following operations:

* $n$-ary function composition $f \circ (g_1, ..., g_n) = h$ where:

$$h(x_1, ..., x_k) = f(g_1(x_1, ..., x_k), ..., g_n(x_1, ..., x_k))$$
* primitive recursion defined on functions *base* and *ind* by:

$$ \mathbf{Rec}(\mathbf{base}, \mathbf{ind})(0, x_1, \dots, x_k) = \mathbf{base}(x_1, \dots, x_k); $$

$$ \mathbf{Rec}(\mathbf{base}, \mathbf{ind})(\mathbf{Succ}(x), x_1, \dots, x_k) = \mathbf{ind}(x, \mathbf{Rec}(\mathbf{base}, \mathbf{ind})(x, x_1, \dots, x_k), x_1, \dots, x_k); $$

* minimisation operator $\mu$ defined on a function $f$ by:

$$ \mu(f)(x_1, \dots, x_k) = a \text{ such that } f(a, x_1, \dots, x_k) = 0 $$

$$ \text{and } f(i, x_1, \dots, x_n) > 0 \text{ otherwise.} $$

The minimisation operator searches for the smallest natural number for which the input function $f$ returns 0 on it. In case there is no such argument, it is not defined. The implementation of minimisation corresponds to a procedure which searches with a counter (initialised to 0) on the first argument of $f$ and which loops by incrementing its counter until finding the right $a$ cancelling the function. Functions without minimisation are called *primitive recursive functions* and are only implemented by terminating procedures. This corresponds to a weaker form of potentially looping procedures.

**§13.9 Undecidability.** Unfortunately, the answer to Hilbert quest for mechanised mathematics is *negative*. It is impossible to always provide an answer for any logical statement of predicate calculus. This can also be formalised by the fact that we cannot provide a constructive proof of $\forall X.X \lor \neg X$ (corresponding to the excluded middle) because we would need to either construct a proof of $X$ or a proof of $\neg X$, which is impossible without any information about $X$. But this can be decidable for some specific choice of $X$. In terms of Turing machine, it can be shown that some problems are impossible to solve by a finite succession of steps. In particular, the famous *Halting problem* asks for a way to tell whether or not a given Turing machine will halt (only by looking at how it is constructed and without simulating it). It is possible to show (and we do in a dedicated section of this chapter) that assuming the existence of a Turing machine deciding this problem leads to a contradiction. Undecidability can be seen as a consequence of Cantor's *diagonal method*. Since Gödel's incompleteness (cf. Paragraph 5.4) is also related to this method, undecidability can be seen as a *computational version* of incompleteness: it expresses the gap between a program/machine and its result, the former cannot be reduced to the latter (since an answer may not come at all depending on inputs).

# 14 Realisation of machines

**§14.1** The story of machines is a parallel story. There are methods that we can share and use but executing them can require an important amount of time or work. Tools has always been made all around the world to reduce the workload of people and increase the efficiency of work for various activities (including very early forms of programmable
machines for music [Koe01]). But what about purely *mental* operations? Can we automatically reproduce some operations occurring in our mind such as arithmetic calculation?

**§14.2 Pascal's calculator.** In the Western world, it is considered that Blaise Pascal, a French scientist, was the first to design a mechanical calculator called the *Pascaline* [Pas97]. This machine was required by his father who was a tax commissioner. Important calculations can take a lot of time and such a machine would be indeed very useful, especially in scientific professions. Pascal's calculator had wheel to write the digit of input numbers. His machine could do basic arithmetic operations such as addition and subtraction with a carry mechanism. Unfortunately, it seems that because of social relations with craftsmen and other factors of his time, Pascal could not expand his project and only 20 machines were constructor over 10 years [Mou88].

**§14.3 Calculus Ratiocinator.** Several different machines were designed after Pascal such as Gottfried Leibniz or Thomas de Colmar's calculators. But let us focus on Leibniz's idea. In his "De arte combinatoria" (1666), he imagined a machine (or algorithm) which could determine whether a sentence, expressed in an idealised language called *characterisca universalis*, was true or false. Such a machine, called *calculus ratiocinator*, would be able to answer everything, any philosophical or scientific question. A famous quote of Louis Couturat illustrate this idea:

“Pour résoudre une question ou terminer une controverse, les adversaires n’auront qu’à prendre la plume, en s’adjoignant au besoin un ami comme arbitre, et à dire : « Calculons ! »

– Louis Couturat

”

meaning that two persons discussing would only need to *compute* in order to conclude the conversation. A common caricature is that Leibniz's idea corresponds more or less to Hilbert's ideal of mechanised mathematics (cf. Paragraph 4.4). However, it seems that Leibniz idea was more nuanced and that he later considered himself that those ideas were too naive and probably impossible to realise (see David Rabouin's works).

**§14.4 Babbage's engine.** To tell the story briefly, Charles Babbage, a British inventor, remarked that some minor errors were present in calculus tables. These human errors are usually caused by unawareness. Inspired by Pascal's engine and his own knowledge of logarithm table, he presented in 1821, the *difference engine* for the purpose of computing polynomials. However, for mechanical reasons, it has never been completed. Another machine, the *analytical engine* is even closer to today's computer. It is designed for more general purposes, and would include arithmetic operations, conditional branching, memory and loops, making it Turing-complete a century before Turing. But again, Babbage was ahead of his time's technology and his machine could not be completed
⁴. His machine would be theoretically be fed with “punched cards” with holes encoding instructions to execute. This is indeed a form of program.

§14.5 **Lovelace's implication.** His engine has been developed jointly with Ada Lovelace, with whom she was corresponding. Ada Lovelace was a countess who received a mathematical education and who was able to interact with great scientists of her time. She called her approach “poetical science”, probably in reference to her mathematician mother and her poet father. Lovelace was very interested in Babbage’s analytical engine and it is thought that she had a great vision of the potential of these machines [FF03]. Babbage’s himself was fascinated by her mathematical skills. She was especially known for her contribution to the analytical engine with a program computing Bernoulli numbers. Today, she is often considered as the *first* programmer<fnref n="5" />.

# 15 Computation as functional process

My personal reference for this chapter is Hammache's PhD thesis (in French) [Ham21, Chapter 4]. A lot of historical information of this section are more or less translated summaries of parts of Hammache's thesis.

Now, I suggest to dive into the λ-calculus, one of the most important models of computation. The λ-calculus comes from logical considerations and from philosophical questioning about the notion of function.

## The notion of function

§15.1 A very natural way to approach computation is to start from (*mathematical*) functions. Functions are often defined as associations of two values (input and output). A first intuition of computation is then to give a concrete realisation which simulates this association. But since we are still in mathematics and not in concrete physical realisations, it is not clear what is a satisfying set of steps mechanically simulating a function.

§15.2 Frege, in his ideal of meaning, developed the notion of function together with some other authors such as Schönfinkel. Although functions were already widely used by mathematicians, definitions of function were neither satisfying nor accurate for Frege. A first characteristic of functions is to distinguish their *argument* (input) and *result* (output) but the point was to understand what could be an argument and what could be a result. Frege wanted to enrich logic with a more mature idea of function, probably because it

<footnote n="4">⁴It even inspired sci-fi novels such as William Gibson and Bruce Sterling’s “The Difference Engine” which imagines a world in which Babbage was able to realise and popularise his inventions.</footnote>

<footnote n="5">⁵Although there are actually historical contestations showing that Babbage was actually the first programmer (see Doron Swade’s affirmations) and controversies about how much Lovelace played a role in “programs” for analytical engine. I cannot tell who is wrong or right but this is a rather convenient myth today.</footnote>
would materialise his personal philosophy. In Frege's philosophy, logic was about relations between "pure" concepts. In his mind, a *concept* was a function returning a *truth value* and a *relation* was a binary function returning a truth value. He distinguished a hierarchy of concepts so that a concept of first level is a function from a class of "objects" to a truth value.

§15.3 The common notation for functions was $f(x) = y$, expressing the product or result $y$ of a function $f$ when applied to an input $x$. We can then plug a value as input and obtain a result: $f(a) = \{x := a\}y$ where $\{x := a\}y$ is a replacement of $x$ by $a$ in $y$. However, as remarked by Frege, it only expresses the result of the function, hence what the function *does*: we have a black box producing $y$ from $x$. We have no mean to express what the function *is*, independently of any *use* of it and of any argument. Frege wanted to find the *essence* of functions, and for that reason, he introduced a notation called *course-of-values*. The function $f$ defined by $f(x) = x + 2$ can be represented by the distinguished expression $\dot{\alpha}(\alpha + 2)$. The application of the function $\dot{\alpha}(f(\alpha))$ (representing a function $f$) to an argument $c$ is seen as an intersection written $c \cap \dot{\alpha}(f(\alpha)) = f(c)$. We now have two expressions, one to refer to the result produced by a function and another one referring to the function itself.

§15.4 Schönfinkel had the ambition of reducing logic to the mechanisms of functions and eventually establishing a “calculus of functions” [Sch24]. It was already remarked in logic that most connectives were superfluous and could be defined by a small set of connectives (cf. Paragraph 6.10). For instance, Whitehead and Russell wanted a reduction to negation and conjunction, and Frege to negation and implication. However, Scheffer<fnref n="6" /> showed that it was possible to consider a unique connective $A \mid B := \neg(A \land B)$ (sometimes written $A \uparrow B$) which would define all the others. Schönfinkel wanted to extend this idea to predicate calculus. It was already known that every predicate calculus formulas could be turned into a formula $\forall x_1...\forall x_n.A$ for a quantifier-free formula $A$. All Schönfinkel needed to do was to get rid of universal quantification. A natural solution was to extend Sheffer’s stroke with a variable in order to define the formula $f(x)|^x g(x) := \forall x.f(x)|^x g(x)$. But the variable $x$ is not even so essential. We can forget it since $A|^x B$ expressed the incompatibility between two predicates (written with a notation of function), independently of the variable $x$ itself. Hence, he introduced the functional notation $Ufg := f(x)|^x g(x)$ and was led to introduce other such functions like $Ix = x$ or $Sfgx = fx(gx)$. These expressions are now known as “combinators” and they later have been developed by Haskell Curry around 1930.

§15.5 Remark that in Schönfinkel’s expression $Ufg$, we have an occurrence of function taking another function as argument. It is also technically possible to consider functions returning other functions. Nowadays, it is known as the idea that functions of several arguments can be represented by unary functions only<fnref n="7" />. The idea is that a function

<footnote n="6">⁶Although it was already present in Peirce’s works [Ham21, Section 4.3.1]. Peirce again!</footnote>

<footnote n="7">⁷This feature is usually called *curryfication* but it seems that there are reasons to call it *fregeing* since the idea was originally introduced by Frege [AK12, Chapter 3].</footnote>
$f : (x, y) \mapsto a$ of two arguments can be represented as a unary function $f' : x \mapsto (y \mapsto a)$ returning another unary function $g : y \mapsto a$ as a result.

## Functional foundations for logic

§15.6 In 1932, Alonzo Church [Chu32] was interested in alternative foundations for logic which would be more satisfying than Russell's type theory and Zermelo's axiomatic theory. Instead of set theory, he was interested in functions as a basis for logical foundations<fnref n="8" />. Church had a representation of functions which could both represent the function itself and their application to arguments. The function $f(x) = x + 2$ was written $\lambda x.x + 2$ and its application to the argument 2 (corresponding to $f(2) = 4$) was written $(\lambda x.x + 2) 2$ which could be reduced to $\{x := 2\}(x + 2)$. Such an expression is called $\lambda$-abstraction. Everything can be considered a function providing we have a mature notion of function. Using $\lambda$-abstractions, the mechanisms linking the input and the output of a function are explicited by reducible syntactic expressions taking into account the notion of function application within the system itself<fnref n="9" />.

§15.7 Church then designed a logical system where all logical constructions are unary functions. The grammar of Church's formulas is the following:

$$M, N ::= x \mid \lambda x.M \mid M N \mid \Pi \mid \Sigma \mid \& \mid \sim \mid \iota \mid A$$

where $x$ is a variable and both $A$ and $\iota$ are special operators we will not talk about. The application $MN$ will sometimes be written $MN$. We leave parentheses implicit and application is considered left-associative, i.e. $M_1M_2M_3 = (M_1M_2)M_3$. We also write $\lambda x.\lambda y.M$ or even $\lambda xy.M$ for $\lambda x.(\lambda y.M)$. Remark that predicates are replaced by functions (this is consistent with Frege's idea of concepts/predicates as functions). The symbols $\Pi$, $\Sigma$ are respectively the universal and existential quantification and the symbols $\&$ and $\sim$ are respectively the conjunction and negation. A very important construction in the function application $MN$ which corresponds to $M(N)$ in mathematics. Remark the unusual presentation of connectives. This is due to the fact that connectives are primitive unary functions. For instance, the formula $A \wedge B$ would be written $(\&A)B$ representing a function $\&$ applied to a first argument $A$ and returning a function to which we feed a second argument $B$. The main reduction rule called $\beta$-reduction is the following:

$$(\lambda x.M)N \rightsquigarrow \beta \{x := M\}N$$

For instance, we have $\vee := \lambda x.\lambda y. \sim ((\&(\sim x))(\sim y))$ which corresponds to the disjunction and $(\vee A)B \rightsquigarrow \beta \sim ((\&(\sim A))(\sim B))$ for some formulas $A$ and $B$.

<footnote n="8">⁸The use of a calculus of functions to solve foundational problems was apparently not considered by Schönfinkel.</footnote>

<footnote n="9">⁹In modern programming we sometimes talk about *nameless functions* and see Church language as programming with mathematical functions</footnote>
§15.8 Around the same period, Haskell Curry was also interested in a functional point of view on the foundations of logic. He introduced *combinatory logic* which can be seen as a further development of Schönfinkel's calculus of functions. Curry wanted to develop what he called an *Urlogik*, a sort of *proto-logic* which would precede any logical construction. Another interest of Curry was to study the notion of *substitution* which had not been clearly formalised although widely used, sometimes implicitly (by Frege and Russell in particular). Combinators are constants representing functions without explicit bound variables (unlike the *x* attached to λ and ∀), and are associated with a reduction rule. Curry considered the following combinators:

• $Bxyz \leadsto x(yz);$

• $Cxyz \leadsto (xz)y;$

• $Kxy \leadsto x;$

• $Wxy \leadsto xyy.$

It is possible to retrieve Schönfinkel's combinators with $I := SKK = WK$ and $S := B(B(BW)C)(BB)$. In particular, $S$ was thought to be counter-intuitive and Curry provided a decomposition with more intuitive combinators. It appears that combinatory logic is equivalent to λ-calculus:

• not so surprisingly, combinators can be easily represented with λ-terms;

• more surprisingly, any computable function can be represented with only the combinators $S, K$ and $I$.

Chris Barker showed (around 2000) that it was possible to consider only one combinator $ι$ [Bar01] defined by $ι := λf.((fS)K)$ such that the SKI combinators could be defined with $I := ιι, K := ι(ιι)$ and $S := ι(ι(ιι))$.

§15.9 **Paradoxes.** It has quickly been remarked that Church's system was inconsistent and that a paradox similar to Russell's one is present Section 3. It is possible to construct the expression $λf. ∼(ff)$ which will be sometimes true or false depending on its argument (Church considered his language a logic and hence any statement could be either true or false). But even weirder, it is possible to feed it with... itself and obtain $R := (λf. ∼(ff))(λf. ∼(ff))$. Now we obtain the following reductions:

$$R \leadsto_{β} \sim((λf. \sim( ff ))(λf. \sim( ff ))) = \sim R$$
$$\sim R \leadsto_{β} \sim\sim R \equiv R$$

The last reduction relies on the equivalence $¬¬A ≡ A$ that Church allowed. The main problem of Church's logic is not the presence of this paradox itself but the requirement that formulas must be either true or false. The expressions already have a *computational* meaning independent of any logical meaning. Unlike Church, Curry did not necessarily want to get rid of paradoxes at any cost. His Urlogik was more permissive and he thought
$$
\begin{align*}
& \text{disj } (\text{is\_zero } \overline{1}) (\text{neg } (\text{is\_zero } \overline{1})) \\
& = \text{cond } (\text{is\_zero } \overline{1}) \text{ true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& = (\lambda c.\lambda x.\lambda y.cxy) (\text{is\_zero } \overline{1}) \text{ true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& \rightsquigarrow_{\beta} (\{c := \text{is\_zero } \overline{1}\}(\lambda x.\lambda y.cxy)) \text{ true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& = (\lambda x.\lambda y.(\text{is\_zero } \overline{1})xy) \text{ true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& \rightsquigarrow_{\beta}^{*} (\text{is\_zero } \overline{1}) \text{ true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& \rightsquigarrow_{\beta}^{*} \text{false true } (\text{neg } (\text{is\_zero } \overline{1})) \\
& \rightsquigarrow_{\beta}^{*} \text{neg } (\text{is\_zero } \overline{1}) \\
& \rightsquigarrow_{\beta}^{*} \text{neg false} \\
& = (\lambda x.\text{cond } x \text{ false true}) \text{ false} \\
& \rightsquigarrow_{\beta} \{x := \text{false}\} (\text{cond } x \text{ false true}) \\
& = \text{cond false false true} \\
& \rightsquigarrow_{\beta}^{*} \text{false false true} \\
& \rightsquigarrow_{\beta}^{*} \text{true}
\end{align*}
$$

<caption>Figure 15.1: Example of computation of the truth value of the statement “either 1 is null or it is not”</caption>

that it could be interesting to study systems containing paradoxes and the meaning of
those paradoxes.

**Mathematical functions as a model of computation**

§15.10 Lambda-calculus. Forgetting the functional point of view of logic, we can consider Church's system as a model of computation now known as (pure or untyped) λ-calculus. The expressions are called λ-terms and are defined by the following grammar:

$$
M, N ::= x \mid \lambda x.M \mid MN \qquad \text{(Lambda-terms)}
$$

And the only reduction rule, as expected, is still the $\beta$-reduction$^{10}$:

$$
(\lambda x.M)N \rightsquigarrow_{\beta} \{x := M\}N
$$

<footnote n="10">¹⁰Although other rules are often considered, this is the most important rule.</footnote>
We say that two terms $M$ and $N$ are $\beta$-equivalent, written $M \equiv_\beta N$ when there is a sequence of terms $M_0 = M, M_1, \dots, M_n, M_{n+1} = N$ such that either $M_i \rightsquigarrow_\beta M_{i+1}$ or $M_{i+1} \rightsquigarrow_\beta M_i$. We write $M \rightsquigarrow_\beta^* N$ when $M$ can be reduced in zero or at least one step to $N$. When we have $M \rightsquigarrow_\beta N$ and $N$ is irreducible then we say that $N$ is a normal form of $M$. This model of computation is very powerful since it has been shown that it is expressive enough to express all the computable functions. It is also powerful for its simplicity: it only needs three constructors and a single reduction rule. Here are some common example of terms:

* the identity function $\lambda x.x$;

* the left and right projection $\lambda x.\lambda y.x$ and $\lambda x.\lambda y.y$;

* $\lambda x.xx$;

* $(\lambda x.xx)(\lambda x.xx)$ which reduces into itself.

It is also possible to encode boolean operators or natural numbers so that the reductions behaves as expected:

* the truth value 0 is represented by `true` := $\lambda x.\lambda y.x$;

* the truth value $f$ is represented by `false` := $\lambda x.\lambda y.y$;

* conditionals are represented by `cond` := $\lambda c.\lambda x.\lambda y.cxy$ ($c$ will be a truth value seen as a selector selecting either $x$ or $y$);

* negation is represented by `neg` := $\lambda x.cond x false true$;

* conjunction is represented by `conj` := $\lambda x.\lambda y.cond x y false$;

* disjunction is represented by `disj` := $\lambda x.\lambda y.cond x true y$;

* the natural number $n$ is represented by $\bar{n}$ := $\lambda s.\lambda z.s^n z$ where $s^n$ corresponds to $n$ successive applications of $s$ (representing the successor function over the variable $z$ representing zero);

* the function `is_zero` := $\lambda n.n (\lambda xfalse) true$ which returns true if its input is 0 and false otherwise.

A simple example of computation with $\lambda$-terms is $(\lambda x.\lambda y.y)(\lambda x.x)(\lambda x.x) \rightsquigarrow_\beta (\{x := \lambda x.x\}(\lambda y.y))(\lambda x.x) = (\lambda y.y)(\lambda x.x) \rightsquigarrow \{y := \lambda x.x\}y = \lambda x.x$. A more complex example of detailed computation is given in Figure 15.1.

**§15.11 Conflicts of names.** There is a small technical and often neglected (and also often painful to treat) detail to take into account with $\lambda$-terms. In the expression $\lambda x.M$, the variable $x$ is *bound* in $M$, meaning that all occurrences of $x$ appearing in $M$ are virtually linked to $\lambda x$. This is similar to the mathematical function $f(x) = M$. When an argument is provided, all those occurrences of $x$ are replaced. But in $\lambda$-calculus, it is technically possible to use several occurrences of a variable which are unrelated. For instance, in $\lambda x.M(\lambda x.N)$, the first $x$ is bound in $M$ only and the second one in $N$ only.