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.

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. 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.