In matemaattinen logiikka , Craig interpoloimalla lause sanoo, että jos kaava φ liittyy toisen ψ, ja φ ja ψ osuus vähintään yhden ei-loogisen symboli yhteistä, sitten on kaava ρ, kutsutaan interpolant siten, että:
Esimerkiksi asettamalla:
φ = (otan K-tie tai otan sateenvarjon) ja syön jäätelöä; ψ = (jos sataa, käytän K-tietä) tai (jos sataa, otan sateenvarjon),meillä on φ merkitsee ψ. Kaavat φ ja ψ jakavat "otan K-tie" ja "otan sateenvarjon" ei-loogisina symboleina. Kaava (otan K-suunnan tai otan sateenvarjon) on interpolantti.
Muodollisesti ehdotuslogiikassa asettamalla:
φ = (P ∨ R) ∧ Q; ψ = (T → P) ∨ (T → R),meillä on φ merkitsee ψ. Kaavat φ ja ψ jakavat P ja R ei-loogisina symboleina. Kaava (P ∨ R) on interpolantti.
William Craig osoitti sen ensimmäisen tilauksen logiikalle vuonna 1957.
Ensimmäisen asteen logiikassa Craigin interpolaatiolause esitetään seuraavasti:
Craigin interpolaatiolauseet - Olkoon φ, ψ kaksi ensimmäisen kertaluvun kaavaa, kuten φ ja ψ, jakavat vähintään yhden ei-loogisen symbolin. Jos φ → ψ on kelvollinen , on olemassa kaava ρ, joka:
On useita tapoja todistaa Craigin interpolointilause:
Craig-Lyndonin interpolaatiolause on jatkoa Craigin interpolointilauseelle.