Twierdzenie Craiga

Twierdzenie Craiga – twierdzenie logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione przez Szablon:Link-interwiki, amerykańskiego logika.

Definicje

Interpolantem nazwiemy taką formułę $Z,$ że $X⟹Z$ i $Z⟹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⟹Y$ będącego tautologią istnieje interpolant.

Przykład

Niech $X=p(g(x))\wedge q(f(x)),$ a $Y=q(f(x))\vee r(h(y,x),y).$ Twierdzenie $(p(g(x))\wedge q(f(x)))⟹(q(f(x))\vee 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))\wedge q(f(x)))⟹q(f(x)),$

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