|
Affiner ou élargir la recherche
Résultats n° 1 à 8 sur un total de 15 entrées référencées
| Titre |
La théorie des types et les systèmes informatiques de traitement de démonstrations mathématiques |
| Auteur |
DOWEK Gilles |
| Mots-clefs |
Calcul, Démonstration, Fonction, Langage mathématique, Raisonnement, Systèmes de traitement de démonstrations mathématiques, Théorie des ensembles, Théorie des types |
| Thèmes |
Calcul, Ensembles (Théorie des), Informatique, Logiciel, Logique |
| Résumé |
Depuis la fin des années soixante, on a vu apparaître plusieurs logiciels destinés à traiter des connaissances mathématiques, en particulier des démonstrations formelles. La réalisation de tels logiciels pose de nouveaux problèmes, en particulier celui de la conception de cadres logiques dans lesquels les mathématiques puissent être formalisées en fait. Cela renouvelle la problématique des fondements des mathématiques, jusque-là davantage concentrée sur la potentialité de la formalisation que sur son actualité. Plusieurs raisons expliquent que les concepteurs de tels logiciels choisissent bien souvent de formaliser les mathématiques en théorie des types, plutôt qu'en théorie des ensembles. |
| Numéro |
165, Printemps 2004, n° spécial La théorie constructive des types |
| Langue |
 Français | Lire l'article
| Titre |
La théorie de la preuve de la théorie des types de Marin-Löf |
| Auteur |
SETZER Anton |
| Mots-clefs |
Arbres bien fondés, Définitions inductive-récursives, Ordinaux de Kleene, Programmation générique, Théorie des ensembles, Théorie des ensembles de Kripke Platek, Théorie des types de Martin-Löf, Univers de Mahlo |
| Thèmes |
Arbres, Ensembles (Théorie des), Logique, Ordres et préordres, Types (Théorie des) |
| Résumé |
Nous donnons une vue d'ensemble du développement historique de la théorie de la preuve et des principales techniques utilisées dans la théorie ordinale de la preuve. Nous soutenons que, dans une forme révisée du programme d'Hilbert, la théorie ordinale de la preuve doit être complétée par une seconde étape, à savoir le développement de théories constructives fortes et équiconsistantes. Comme partie d'un tel programme, nous présentons ensuite l'analyse, en théorie de la preuve, de la théorie des types de Martin-Löf avec un univers microscopique ne contenant que deux types finis. Nous examinons ensuite l'analyse de la théorie des types de Martin-Löf avec type W et un univers clos pour ce type, puis nous étendons la théorie des types par un univers de Mahlo et considérons son analyse en théorie de la preuve. Enfin, nous présentons le concept de définition inductive-récursive, qui étend de façon substantielle la notion de définition inductive. Nous introduisons une formalisation close, qui peut être employée en programmation générique, et expliquons ce que nous savons de sa force ordinale. |
| Numéro |
165, Printemps 2004, n° spécial La théorie constructive des types |
| Langue |
 Anglais | Lire l'article
| Titre |
La critique de la théorie des ensembles dans la dissertation de Brouwer (1907) |
| Auteur |
BOURDEAU Michel |
| Mots-clefs |
Continu, Intuitionnisme, Ordinaux, Transfini |
| Thèmes |
Ensembles (Théorie des), Epistémologie, Histoire des mathématiques, Logique, Ordres et préordres |
| Résumé |
S'il faudra attendre 1917 pour que Brouwer développe une mathématique distincte des mathématiques classiques, certains des thèmes caractéristiques de l'intuitionnisme, comme l'attachement à une intuition de type kantien ou l'idée que le continu est une donnée irréductible, apparaissent dès la Dissertation de 1907. C'est le cas en particulier de l'attitude à l'égard de la création cantorienne, où il convient, nous dit-on, de distinguer deux aspects : les acquis proprement mathématiques (topologie, ordinaux), qu'il s'agit de sauvegarder, une confiance excessive dans les pouvoirs de la logique, qui est responsable des contradictions. Le transfini se présente ainsi sous deux formes : la théorie des puissances, les ordinaux. Brouwer accepte celle-ci mais non celle-là. La même attitude explique encore que l'hypothèse du continu soit examinée en deux endroits différents : dans la première partie, pour sa version proprement mathématique, dans la troisième, pour sa version logique. Dans ce dernier cas, Brouwer admet les deux principes de construction des ordinaux, mais estime que cela n'autorise pas à considérer la seconde classe de nombres comme une totalité achevée. |
| Numéro |
164, Hiver 2003 |
| Langue |
Français | Lire l'article
| Titre |
Cercles vicieux, mathématiques et formalisations logiques |
| Auteur |
LONGO Giuseppe |
| Mots-clefs |
Anti-fondation, Auto-application, Auto-référence, Equation, Imprédicativité |
| Thèmes |
Algèbre, Ensembles (Théorie des), Epistémologie, Logique, Ordres et préordres, Types (Théorie des) |
| Résumé |
Certaines formes de circularité logiques et mathématiques (auto-appartenance, auto-implication, imprédicativité) sont analysées comme des propriétés de fermeture de certaines structures mathématiques puisqu'on peut les interpréter comme des solutions de certains systèmes d'équations. Parallèlement, du point de vue philosophique, on met en évidence la contribution de ces circularités au pouvoir des mathématiques à rendre le monde intelligible. |
| Numéro |
152, Hiver 2000 |
| Langue |
Français | Lire l'article
Lire l'article
Lire l'article
Lire l'article
Lire l'article
Droits des utilisateurs :
Cette création est mise à disposition sous un contrat Creative Commons
|
