Twierdzenie Craiga

Twierdzenie Craiga jest twierdzeniem logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione przez Williama Craiga, amerykańskiego logika.

Definicje

Interpolantem nazwiemy taką formułę $Z$, że $X \implies Z$ i $Z \implies Y$ są tautologiami, zaś w w $Z$ nie występuje żadna relacja ani symbol funkcyjny (w tym stała), która nie występuje jednocześnie w $X$ i $Y$.

Teza

Dla każdego zdania rachunku predykatów pierwszego rzędu postaci $X \implies Y$ będącego tautologią istnieje interpolant.

Przykład

Niech $X = p(g(x)) \and q(f(x))$, a $Y = q(f(x)) \or r(h(y,x),y)$. Twierdzenie $(p(g(x)) \and q(f(x))) \implies (q(f(x)) \or r(h(y,x),y))$ jest tautologią.

Spróbujmy zbudować więc interpolant, pamiętajmy jednak, że wolno nam do tego użyć jedynie predykatu $q$ oraz symbolu funkcyjnego $f$, nie wolno zaś używać predykatów $p, r$, ani też symboli funkcyjnych $g$ i $h$.

Łatwo zgadnąć, że szukanym interpolantem jest $q(f(x))$, gdyż istotnie zachodzi

$(p(g(x)) \and q(f(x))) \implies q(f(x))$,

$q(f(x)) \implies (q(f(x)) \or r(h(y,x),y))$.

W tym przykładzie interpolant można było odgadnąć dość łatwo, jednak wiemy przecież, że istnieją formuły dużo bardziej skomplikowane. Twierdzenie Craiga mówi, że interpolant istnieje zawsze, niezależnie od tego jak skomplikowane są $X$ i $Y$.