Théorème d'interpolation de Craig

En logique mathématique, le théorème d'interpolation de Craig dit que si une formule φ en implique une deuxième ψ, et que φ et ψ partagent au moins un symbole non logique en commun, alors il existe une formule ρ, appelée interpolant, telle que :

• φ implique ρ ;
• ρ implique ψ ;
• tout symbole non logique dans ρ apparaît à la fois dans φ et ψ.

Exemple

Par exemple, en posant :

φ = (je prends un K-way ou je prends un parapluie) et je mange une glace ;

ψ = (s'il pleut alors je prends un K-way) ou (s'il pleut alors je prends un parapluie),

on a φ implique ψ. Les formules φ et ψ partagent « je prends un K-way » et « je prends un parapluie » comme symboles non logiques. La formule (je prends un K-way ou je prends un parapluie) est un interpolant.

Formellement, en logique propositionnelle, en posant :

φ = (P ∨ R) ∧ Q ;

ψ = (T → P) ∨ (T → R),

on a φ implique ψ. Les formules φ et ψ partagent P et R comme symboles non logiques. La formule (P ∨ R) est un interpolant.

Histoire

Il a été démontré par William Craig pour la logique du premier ordre en 1957[1].

Démonstrations

En logique du premier ordre, le théorème d'interpolation de Craig s'énonce ainsi :

Théorèmes d'interpolation de Craig — Soit φ, ψ deux formules du premier ordre telle φ et ψ partagent au moins un symbole non logique en commun. Si φ → ψ est valide, alors il existe une formule ρ telle que :

• φ → ρ est valide ;
• ρ → ψ est valide ;
• tout symbole non logique dans ρ apparaît à la fois dans φ et ψ.

Il existe plusieurs façons de démontrer le théorème d'interpolation de Craig :

• via la théorie des modèles (théorème de Robinson) ;
• via le calcul des séquents, par induction sur une preuve[2]. Cette démonstration donne d'ailleurs un algorithme, qui prend en entrée une preuve en calcul des séquents et retourne un interpolant.

Théorème d'interpolation de Craig-Lyndon

Le théorème d'interpolation de Craig-Lyndon est une extension du théorème d'interpolation de Craig.

Notes et références

1. (en) William Craig, « Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory », The Journal of Symbolic Logic, vol. 22,‎ 1^er janvier 1957, p. 269–285 (DOI 10.2307/2963594, lire en ligne, consulté le 2 mai 2016).
2. René David, Karim Nour et Christophe Raffali, Introduction à la logique : Théorie de la démonstration, Dunod, p. 216-218