Twierdzenie Craiga

Twierdzenie Craiga – twierdzenie 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 $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))\land q(f(x)),$ a $Y=q(f(x))\lor r(h(y,x),y).$ Twierdzenie $(p(g(x))\land q(f(x)))\implies (q(f(x))\lor 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))\land q(f(x)))\implies q(f(x)),$

$q(f(x))\implies (q(f(x))\lor 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.$