Twierdzenie Craiga

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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

Definicje[edytuj | edytuj kod]

Interpolantem nazwiemy taką formułę Z, że X \implies Z i Z \implies Ytautologiami, 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[edytuj | edytuj kod]

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

Przykład[edytuj | edytuj kod]

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.

Przypisy

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