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..
Démonstrations En logique du premier ordre, le théorème d'interpolation de Craig s'énonce ainsi :
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. 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
Catégorie:Lemme de mathématiques Catégorie:Théorème de logique mathématique