Description

Ce projet s'intéresse à l'unification des mathématiques inverses classiques et constructives, avec un accent particulier sur des résultats issus de la théorie des modèles de la logique du premier ordre. En s'appuyant sur des analyses constructives récentes de théorèmes de complétude, la recherche portera sur des résulats connexes, tels que les théorèmes de Löwenheim–Skolem et de compacité. L'objectif est d'identifier les principes logiques exacts requis dans les contextes classique et constructif. En utilisant le calcul des constructions inductives (CIC) comme base neutre, le projet explorera comment les perspective constructive et classique peuvent être représentées au sein d'un même système. Le résultat attendu est une meilleure compréhension des points de convergence et de divergence entre les deux approches, ainsi que les premiers pas vers un cadre commun capable d'intégrer des résultats issus des deux traditions.

Compétences requises

Solide formation en théorie des modèles, démonstration interactive assistée par ordinateur et logique constructive. Idéalement, un stage portant sur l’intersection de ces trois domaines a déjà été effectué.

Bibliographie

See pdf

Mots clés

mathématiques inverses, logique constructive, théorie des modèles, démonstration interactive assistée par ordinateur