Preuve et logique intuitionniste : les origines de la sémantique BHK

Brien, Simon (2019). « Preuve et logique intuitionniste : les origines de la sémantique BHK » Mémoire. Montréal (Québec, Canada), Université du Québec à Montréal, Maîtrise en philosophie.

Fichier(s) associé(s) à ce document :

Prévisualisation	PDF Télécharger (2MB)

Résumé

Ce mémoire porte sur un chapitre de l'histoire de la logique au vingtième siècle, soit l'émergence de logique intuitionniste, qui a longtemps été tenue pour seule rivale de la logique classique, et qui continue de jouer un rôle majeur aujourd'hui, en particulier dans le domaine où se chevauchent logique mathématique et informatique théorique, ou encore dans les fondements des mathématiques. Nous retraçons les étapes de cette émergence à partir de son origine (chapitre 1) dans la critique du principe du tiers exclu par L. E. J. Brouwer dans son texte de 1908, « Que les principes logiques ne sont pas fiables », dont nous montrons qu'elle est basée sur des thèses philosophiquement problématiques sur la construction des objets mathématiques dans l'intuition et sur le divorce radical entre la pensée et le langage dans lequel on communique ces constructions mentales. La logique étant affaire de langage, par des inférences logiques faisant usage du tiers exclu on peut dériver des formules auxquelles plus aucune construction mentale ne correspond, d'où la non-fiabilité de ce principe. Dans le chapitre 2, nous montrons comment ces thèses sont abandonnées par l'étudiant de Brouwer, A. Heyting, ce qui ouvre la voie à une formalisation de la logique intuitionniste. Nous examinons aussi rapidement une objection de M. A. E. Dummett, qui justifie après coup la démarche de Heyting. Dans le chapitre trois, en prenant pour point de départ l'axiomatisation de la logique classique dans les travaux de Hilbert (en 1923 et 1927) nous retraçons soigneusement les étapes ayant mené à la formalisation de Heyting en 1930, dans les travaux de Kolmogorov, d'Orlov et de Glivenko, ainsi qu'à élaboration d'une sémantique des preuves pour la logique intuitionniste, dont le nom « BHK » dérive des initiales de ses concepteurs. Nous concluons sur les travaux de Gentzen, en montrant comment il reprend l'idée de Brouwer de la preuve comme acte, et comment il implémente la sémantique BHK dans son calcul de déduction naturelle intuitionniste, tout en ouvrant de nouveaux horizons pour la logique intuitionniste. _____________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Logique formelle, Fondements des mathématiques, Intuitionnisme, Déduction naturelle

Type:	Mémoire accepté
Informations complémentaires:	Le mémoire a été numérisé tel que transmis par l'auteur.
Directeur de thèse:	Marion, Mathieu
Mots-clés ou Sujets:	Logique symbolique et mathématique / Intuitionnisme / Déduction (Logique) / L. E. J. Brouwer
Unité d'appartenance:	Faculté des sciences humaines > Département de philosophie
Déposé par:	Service des bibliothèques
Date de dépôt:	18 juill. 2019 12:43
Dernière modification:	16 avr. 2021 09:50
Adresse URL :	http://archipel.uqam.ca/id/eprint/12631

Modifier les métadonnées (propriétaire du document)

Statistiques