Théorème d'interpolation de Craig
From Wikipedia, the free encyclopedia
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 ψ.
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].
