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
- (en) William Craig, « Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory », The Journal of Symbolic Logic, vol. 22, , p. 269–285 (DOI 10.2307/2963594, lire en ligne, consulté le ).
- René David, Karim Nour et Christophe Raffali, Introduction à la logique : Théorie de la démonstration, Dunod, p. 216-218