From Dialogues to the Foundations of Constructive Mathematics : for a Dynamic Perspective on the Concept of Demonstration in the Constructive Theory of Types

La thèse s'intéresse aux fondements des Mathématiques Constructives et donc de fait à la conception dialogique de la Théorie Constructive des Types (TCT) qui conteste à la fois le Logicisme de Frege et Russell et le Formalisme Syntaxique. En effet, la présente thèse s'enracine dans l'approche Dialogique de la Logique et du sens qui a été initiée par Paul Lorenzen vers 1958, développée plus loin par Kuno Lorenz, et qui poursuivait l'objectif d'enchâsser la critique épistémique de l'intuitionnisme de Brouwer envers le logicisme et le formalisme au sein d'une approche pragmatiste. En fait, la logique dialogique faisait suite à une approche pragmatiste antérieure appelée logique opératoire et mathématiques. Le tournant dialogique de l'opérativisme a fait des règles de construction des règles d'interaction. En 1980, la Théorie Constructive des Types de Per Martin Löf a donné une nouvelle impulsion au projet de Brouwer, par lequel les caractéristiques subjectivistes de l'intutionnisme de Brouwer ont été remplacées par une approche théorique des types à la notion d'objet de preuve développant davantage l' isomorphisme de Curry-Howard entre les types en tant que propositions / ensembles et programmes comme preuves. Cela a permis non seulement d'étendre le projet constructiviste en mathématiques mais aussi en langage naturel (tel que développé par Arne Ranta) avec la conception d'un langage entièrement interprété où les objets de preuve (en gros les vérificateurs) sont explicites dans le langage objet. Les dernières publications de Martin Löf suggèrent un lien fort entre la TCT et l'approche dialogique. Plus récemment, Shahid Rahman et ses collaborateurs à Lille, suivant les suggestions de Martin-Löf et Göran Sundholm, ont développé le Raisonnement Immanent, qui est un cadre qui relie la TCT de Martin-Löf à l'approche dialogique et étend les Dialogues purement formels de Lorenzen et Lorenz à la construction d'une langue avec un contenu. Cela conduit à l'objectif principal de la présente thèse : le développement d'un calcul des séquents pour le raisonnement immanent qui émerge de bas en haut à partir du niveau de jeu - c'est-à-dire au niveau où le sens est forgé, plutôt que de haut en bas à partir du niveau de validité logique : l'accent mis sur le sens dans la présente étude est le sens mathématique : le point est de montrer que le cadre dialogique permet de construire les objets mathématiques au moyen de l'interaction. Cette démonstration nécessitera que nous travaillions dans un ordre supérieur avec des "fonction-types" ou des fonctions comme types, correspondant au niveau stratégique des Dialogues. Le projet lui-même s'inscrit dans le cadre des programmes de recherches ADA-LACTO, et en particulier à l'étude de l'interaction entre l'argumentation et le raisonnement inférentiel.The thesis is concerned with the foundations of Constructive Mathematics and more precisely with the dialogical conception of Constructive Type Theory (CTT) which contests both the Logicism of Frege and Russell and Syntactic Formalism. Indeed, the present thesis is rooted in the dialogical approach to logic and meaning that wasinitiated by Paul Lorenzen around 1958, further developed by Kuno Lorenz. This approach aimed to embed the epistemic critique of Brouwer's intuitionism towards logicism and formalism within a pragmatist framework. In fact, Dialogical Logic followed up on an earlier pragmatist approach called “Operative Logic and Mathematics”. The Dialogical approach to operativism turned rules of construction into rules of interaction.By 1980 Per Martin Löf's Constructive Type Theory gave a new impulse to Brouwer's project,whereby the subjectivist features of Brouwer's intutionism were replaced by a type-theoreticapproach to the notion of proof-object, further developing further the Curry-Howard isomorphism between types as propositions/sets and programs as proofs. This allowed not only to extend the constructivist project in mathematics but also in natural language (as developed by Arne Ranta) with the design of a fully interpreted language where the proof objects roughly truth-makers) are explicit in the object language. The latest publications of Martin Löf suggest a strong link between CTT and the Dialogical approach. More recently Shahid Rahman and collaborators in Lille, following Martin-Löf's and Göran Sundholm's suggestions, developed Immanent Reasoning, which is a framework that links Martin-Löf's CTT with the dialogical approach and extends the purely formal Dialogues of Lorenzen and Lorenz to the construction of a language with content. This leads to the main goal of this thesis:the development of a Sequent Calculus for Immanent reasoning which emerges bottom-up from the play level - that is, at the level where meaning is forged, rather than top-down from the level of logical validity: the focus on meaning in this study is mathematical meaning: the point is to show that the dialogical framework allows for the construction of mathematical objects by means of interaction. This demonstration will require that we work in a higher order with "function-types" or functions as types, which corresponds to the strategic level of Dialogues. The project itself is part of the ADA-LACTO research programs, and in particular the study of the interaction between argumentation and inferential reasoning