LOGIQUE MATHEMATIQUE ET APPLICATIONS.

1 - 5. Survol des Théorèmes d'Incomplétude en Arithmétique et/ou Théorie des Ensembles: 5 exposés possibles.

La Théorie de la Démonstration a établie plusieurs résultats dont on démontre la vérité sur certaines structures mathématiques, ainsi que l'indémontrabilité à l'intérieur des Théorie formelles qui étaient sensé les "formaliser". L'élève devrait étudier un des résultats de ce genre pour l'Arithmétique (Incomplétude: Goedel, ou Paris-Harrington ou Kruskal-Friedman) ou pour la Théorie des Ensembles (Indépendance: Continu ou Choix, Goedel/Cohen).

(Le théorème de Kruskal-Friedman, par exemple, est un résultat récent, fort intéressant et "simple" d'indémontrabilité; voir les présentations rigoureuses de Simpson dans Harrington ou Gallier et/ou l'introduction informelle de Smorinsky dans Harrington. Pour les autres théorèmes d'incomplétude ou indépendance, voir Devlin, Kunen ou Jech (ou Paris-Harrington dans Barwise, J. ed.)

Barwise, J. ed. Handbook of Math. Logic, North-Holland, 1978. ( ENS-BM M 760 080)

Smorinsky C. "The incompleteness theorems" in Handbook of Math. Logic, Barwise ed., 1978.

Harrington L. et al. (eds), H. Friedman's Research on the Foundations of Mathematics, North-Holland, 1985.

Gallier J. "What is so special about Kruskal's theorem and the ordinal G0?"Ann. Pure. Appl. Logic, 53, 1991.

Pour une introduction ''philosophique'' au problème et des reférences, voir aussi:
Giuseppe Longo. Mathematical Intelligence, Infinity and Machines: beyond the Goedelitis.�Invited paper, Journal of Consciousness Studies, special issue on Cognition, vol. 6, 11-12, 1999.�

Pour une travail plus technique :
Giuseppe Longo. On the proofs of some formally unprovable propositions and Prototype Proofs in Type Theory. Invited Lecture,Types 2000, Durham (GB), Dec. 2000, to appear in LNCS 2277, Springer, 2002.

Les deux articles sont parmi les ''downloadable papers'' de la page web de l'auteur.

6 - Définitions imprédicatives en Logique et en Math (e.g. Mesure de Lebesgue, domains continus de Scott).

On utilise, en mathématiques, des définitions apparament "circulaires", c.a.d. qui définissent une notion, un ensemble en termes qui "contiennent" l'ensemble ainsi défini. La topologie, la Mesure de Lebesgue en donnent des exemples à voir de près.
Voir un texte de théorie générale de l'intégration et

Giuseppe Longo. Cercles vicieux, Math�matiques et formalisations logiques.

Thomas Fruchart and Giuseppe Longo. Carnap's remarks on Impredicative Definitions and the Genericity Theorem.

(Downloadable de la page web) pour savoir ce que c'est qu'un définition imprédicative et avoir d'autres références à discuter avec Longo.

La théorie des types clarifie très bien ce concept, en sons sein: un exposé possible pourrait se concentrer sur son traitement par la notion de catégorie interne.
Voir le chapitre 11 de

Asperti A., Longo G. Categories, Types and Structures, M.I.T. - Press, 1991.

7 - Théorie des Domaines pour la calculabilité et systèmes dynamiques

Un sujet fondateur est celui des modèles des calculs non-typés (voir
Barendregt H. Type-free lambda-calculus, North-Holland 1984, consulter Longo pour le choix des chapitres).

Quelques résultats récents permettent de donner des représentations efficaces de certaines notions de théorie de la mesure et des systèmes dynamiques, dans un cadre familier au logiciens et aux informaticiens: la Théorie des Domaines "à la Scott". Une introduction à l'argument permet une intéraction intéressante entre la calculabilité logico-informatique et des secteur pointus des maths (voir G. Santini "Théories des domaines et systèmes dynamiques", rapport LIENS 97-15, pour en savoir plus et pour une bibliographie, à discuter avec Longo).

Back to Longo's index page.