Complétude forte d'une logique temporelle du premier ordre pour le temps réel

Résumé La logique temporelle propositionnelle sur le flux temporel des nombres réels est finiment axiomatisable, mais son homologue du premier ordre n'est pas axiomatisable de manière récursive. Nous étudions la logique qui combine l'axiomatisation propositionnelle avec les axiomes habituels de la logique du premier ordre avec identité, et développons une sémantique alternative « admissible » pour celle-ci, montrant qu'elle est fortement complète pour les modèles admissibles sur les réels. En revanche, il n'existe pas d'axiomatisation récursive de la logique temporelle du premier ordre des modèles admissibles dont le flux temporel est constitué des entiers, ou de tout ordre linéaire dispersé.