3. L'ordinal ε0 et la ω-logique
À plusieurs reprises dans les années trente, Gentzen allait donner des démonstrations de cohérence pour l'arithmétique de Peano AP. Pour obtenir de tels résultats, il était nécessaire, par le second théorème d'incomplétude, de se servir de méthodes extérieures à l'arithmétique. Gentzen utilisa comme méthode l'induction transfinie jusqu'à ε0, où ε0 est défini comme le suprémum des ordinaux ωn, avec ω0 = 1, ωn+1 = ωωn). Dans les années cinquante, Schütte allait donner une version plus accessible de ces mêmes résultats : essentiellement, l'arithmétique de Peano est obtenue à partir du calcul des prédicats en ajoutant le schéma d'axiomes d'induction :
Le schéma d'induction devient démontrable dans la ω-logique ; c'est, en fait, un cas particulier du théorème suivant, dû à Orey :
Théorème d'ω-complétude. Γ ⊢ Δ est vrai dans tout ω-modèle (modèle dont le domaine est exactement N et où 0̄ et S sont interprétés de façon standard) si et seulement s'il y a une ω-démonstration récursive […]
… pour nos abonnés, l'article se prolonge sur 9 pages…
