Twierdzenie Craiga

Twierdzenie Craiga – twierdzenie logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione^[1] przez Williama Craiga(inne języki), amerykańskiego logika.

Definicje

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

Teza

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

Przykład

Niech ${\displaystyle X=p(g(x))\land q(f(x)),}$ a ${\displaystyle Y=q(f(x))\lor r(h(y,x),y).}$ Twierdzenie ${\displaystyle (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 ${\displaystyle q}$ oraz symbolu funkcyjnego ${\displaystyle f,}$ nie wolno zaś używać predykatów ${\displaystyle p,r,}$ ani też symboli funkcyjnych ${\displaystyle g}$ i ${\displaystyle h.}$

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

${\displaystyle (p(g(x))\land q(f(x)))\implies q(f(x)),}$

${\displaystyle 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ą ${\displaystyle X}$ i ${\displaystyle Y.}$

Przypisy

1. William Craig: Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Logic 22 1957, s. 250–268.