Note ABES Des Dialogues aux fondements des Mathématiques Constructives : pour une perspective dynamique sur la notion de démonstration dans la Théorie Constructive des Types From Dialogues to the Foundations of Constructive Mathematics : for a Dynamic Perspective on the Concept of Demonstration in the Constructive Theory of Types Fondement des Mathématiques Théorie Constructive des Types Dialogues Calcul des Séquents Théorie de la démonstration Fonction-Type Foundations of Mathematics Constructive Type Theory Dialogues Sequent Calculus Proof theory Type-Function Mathématiques constructives Théorie des types Théorie de la démonstration Mathématiques -- Fondements 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. Electronic Thesis or Dissertation Text fr PDF 3578809 https://pepite-depot.univ-lille.fr/ToutIDP/EDSHS/2022/2022ULILH012.pdf Eckoubili Steephen 1988-12-06 GA 263982246 https://theses.fr/2022ULILH012 2022ULILH012 https://doi.org/10.70675/38861a7fzeb76z4c79z9f6fzce7553da456f 2022-07-15 Philosophie Université de Lille (2022-....) 259265152 Doctorat Docteur es non oui Rahman Shahid MADS_DIRECTEUR_DE_THESE_1 059922435 Frápolli María José MADS_PRESIDENT_DU_JURY 087479737 Akué Adotevi Mawusse Kpakpo MADS_MEMBRE_DU_JURY_1 264201248 Fontaine Matthieu MADS_MEMBRE_DU_JURY_2 156355779 Nzokou Gildas MADS_MEMBRE_DU_JURY_3 156230364 Dango Adjoua Bernadette MADS_MEMBRE_DU_JURY_4 189409290 Frápolli María José MADS_RAPPORTEUR_1 087479737 Barés Gómez Cristina MADS_RAPPORTEUR_2 164139389 École doctorale Sciences de l'homme et de la société (Lille ; 2006-....) MADS_ECOLE_DOCTORALE_1 473 148938809 Savoirs, textes, langage (Villeneuve d'Ascq, Nord ; 2006-....) MADS_PARTENAIRE_DE_RECHERCHE_1 094767386 ddc:190 Rahman Shahid Frápolli María J. Akué Adotevi Mawusse Kpakpo Fontaine Matthieu Nzokou Gildas Dango Adjoua Bernadette Frápolli María J. Barés Gómez Cristina École doctorale Sciences de l'homme et de la société (Villeneuve d'Ascq, Nord) Savoirs, textes, langage (Villeneuve d'Ascq, Nord) PDF 3578809