Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Logique, démonstration et théorie des types Cassis November 2021 2 Avant-propos

Logique, démonstration et théorie des types Cassis November 2021 2 Avant-propos Ce document a pour objectif de donner une vision de ce qu’est la logique mathématique, des bases de la théorie de la démonstration, en construire les objets de base des mathématique, puis enfin d’établir des liens avec la théorie des types et le lambda-calcul. Une précision assez importante : le symbole = aura plusieurs usages, et pour éviter trop d’ambiguïtés et de confusion, nous utiliserons ∶= pour écrire une égalité définitionnelle (du moins dans les chapitres précédant celui sur la théorie des types), c’est-à-dire qu’un objet que nous ver- rons pour la première fois, sera en général introduit par ce symbole. (Par exemple la proposition P ∶= x = y devient plus lisible avec cette notation). Si plusieurs preuves sont présentées dans ce document, elles le sont à titre principalement indicatif, et il n’est pas nécessaire de les intégrer pleinement pour comprendre les définitions et exemples. En effet, ce document vise avant tout à ce que le lecteur se familiarise avec la logique et la théorie de la démonstration, puis dans un deuxième temps avec la théorie des types. A ce propos, une partie non négligeable du document est dédiée au lambda-calcul : cette partie est une introduction négligeant particulièrement les aspects techniques, et il est plus que conseillé de suivre un cours sur ce sujet pour plus de rigueur (c’est aussi le cas de la théorie des types). Enfin, précisons que le public visé est un public déjà familier avec la pratique des maths, donc des élèves avec une abstraction et une aisance avec les notations mathématiques du niveau d’un bon élève de licence. La partie I a avant tout été inspirée de [1, Cor], tandis que la partie II a été basée sur [3, Sel] pour toute la partie sur le lambda-calcul. Le lien profond entre logique et lambda-calcul est aussi développé dans [2, Gir], qui m’a servi avant tout d’inspiration générale, et pour parler de la différence entre la sémantique de Tarski et celle de Heyting. Enfin, le chapitre 7 provient intégralement de [4, HoTT] (mais seulement de la partie dédiée à la théorie des types de Per Martin- Löf, sans inclure la part propre à l’homotopie). Ainsi, pour plus de rigueur, de précision et de profondeur, ces ouvrages sont de bonnes ouvertures. Introduction La distinction entre la syntaxe et la sémantique Faire des mathématiques, c’est en premier lieu parler d’objets mathémati- ques. Pour un lycéen, par exemple, ce terme semble souvent être un fourre-tout signifiant « quelque chose dont on parle en mathématiques». C’est une défini- tion circulaire. Une autre façon de définir ce terme serait de dire qu’il s’agit d’une construction ensembliste, mais cela signifierait qu’un objet mathématique est uniquement un ensemble construit à partir d’un système axiomatique par- ticulier. Un étudiant en première année dans le supérieur, par exemple, sera peut-être d’accord, mais il sera alors face à une incohérence : un objet mathé- matique dont on n’a pas encore trouvé de formalisation dans ZF n’en serait pas un. De plus, la recherche manipule souvent des objets avant d’en avoir une définition exacte. En conclusion, un «objet mathématique» restera ici un terme flou, et un bon mathématicien doit commencer par accepter ce fait : le jeu des mathématiques est de trouver une rigueur sur des objets que seule l’intuition peut toucher. Si certains doutent de la pertinence de ce problème, l’histoire nous a plusieurs fois prouvé que le manque de rigueur a pu conduire a de nombreux débats mathématiques. L’existence des complexes, par exemple, montre la nécessité d’un consensus sur ce qu’introduire un objet mathématique signifie. On peut naïvement décider que tout constat doit être prouvé, mais l’on serait alors face à une spirale infinie de constats mathématiques qui ont besoin les uns des autres. Les preuves circulaires (partir d’un postulat pour arriver à ce même postulat) ne donnent aucune vérité mathématique. Il faut donc en premier lieu admettre qu’un ensemble de résultats devra être accepté, sans quoi l’on ne peut rien bâtir. Ces résultats sont nommés des axiomes : ce sont des hypothèses de travail sans quoi nous ne pouvons pas effectuer de raisonnement mathématique poussé. Un argument récurrent sur l’acceptation ou non d’un axiome est son évidence. Nous n’entrerons pas dans ce débat, cependant l’évidence de certains axiomes (comme l’axiome du choix) reste un débat récurrent. La première étape vers une vraie rigueur mathématique est celle d’un cadre formel. Si les objets que l’on manipule sont flous, leur comportement ne l’est pas forcément. L’exemple le plus évident est celui des ensembles. Lorsque l’on introduit les ensembles (dès le lycée pour certains, en entrant dans l’enseigne- 3 4 ment supérieur pour d’autres), on se contente d’une description floue telle que « Ce sont des paquets d’objet » ou alors « On peut y mettre n’importe quoi ». Pour autant, il n’y a aucun doute possible sur leur comportement : un objet peut appartenir à un ensemble, et des ensembles peuvent être égaux. Notre cadre formel aura donc pour objectif de rendre compte du comportement des objets, en évitant soigneusement leur nature intrinsèque. C’est ici qu’entre en jeu la distinction entre la sémantique et la syntaxe. — La sémantique des mathématiques est le sens de ces objets mathéma- tiques. Par exemple, « un ensemble est un paquet d’objet non ordonné et sans répétitions » est la sémantique d’un ensemble. Cependant, la plu- part des sémantiques que l’on peut mentionner sont plus précises, du fait qu’un ensemble est un objet particulièrement primitif (nos mathématiques contemporaines sont construites sur la base des ensembles, donc si tous les objets peuvent être décrits comme des ensembles, il reste que les ensembles ne peuvent être décrits de façon plus primitive) : citons par exemple les fonctions, dont la sémantique est d’associer à un objet un autre objet. — La syntaxe, elle, est l’aspect purement calculatoire (au sens large) des mathématiques. Par exemple, si l’on définit une fonction f par f(x) = 2x, en déduire que f(3) = 6 est purement syntaxique. L’avantage évident de la syntaxe est qu’il n’est pas sujet à interprétation : une fois que l’auteur et le lecteur se sont mis d’accord sur les règles qui permettent de passer d’un terme à l’autre, aucune ambiguïté n’est possible. Moralement, la syntaxe est ce qu’un ordinateur peut traiter. La logique est alors l’étude du passage entre la sémantique et la syntaxe. Pour cela, nous sommes confrontés à un premier problème : comment étudier ces aspects mathématiquement ? Nous voulons parler de théorie mathématique, mais alors dans quelle théorie se placer ? Il n’y a pas vraiment d’autre choix ici que d’adopter une meta-théorie : des raisonnements portants sur les théories. Comme on l’a dit plus tôt, il convient pour tout raisonnement de se donner des points de départ, et dans le cadre de la logique, nous devrons aussi convenir de certains éléments. Cependant, la meta-théorie est aussi sûre que la théorie mathématique habituelle, puisque nos « meta-preuves » seront construites sur les mêmes bases logiques et argumentatives. En contrepartie, la théorie mathé- matique habituelle, elle, en la traduisant en un système syntaxique, pourra être (du moins, nous l’espérons) un simple ensemble de calculs, dont la fiabilité sera donc bien plus grande. Nous utiliserons comme système syntaxique la déduction naturelle présen- tée avec des séquents (ne vous inquiétez pas, chers lecteurs, ces termes seront introduits et expliqués plus tard). Table des matières I Logique mathématique classique 9 1 Propositions 11 1.1 Définitions par induction . . . . . . . . . . . . . . . . . . . . . . . . 11 1.1.1 Construction formelle . . . . . . . . . . . . . . . . . . . . . . 11 1.1.2 Définir une fonction par induction . . . . . . . . . . . . . . 15 1.1.3 Prouver par induction . . . . . . . . . . . . . . . . . . . . . 16 1.2 Définition d’une proposition . . . . . . . . . . . . . . . . . . . . . . 17 1.2.1 Langage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.2.2 Terme et proposition . . . . . . . . . . . . . . . . . . . . . . 17 1.2.3 Variables libres, variables liées, renommage . . . . . . . . . 18 1.2.4 Codage et un peu de logique du premier ordre . . . . . . . 20 2 Preuves syntaxiques 23 2.0.1 De la nécessité d’un système de preuves . . . . . . . . . . . 23 2.1 Déduction naturelle et calcul des séquents . . . . uploads/Philosophie/ introduction-logique-type1.pdf