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]

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

Teza[edytuj]

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

Przykład[edytuj]

Niech , a . Twierdzenie jest tautologią.

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

Łatwo zgadnąć, że szukanym interpolantem jest , gdyż istotnie zachodzi

,
.

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ą i .

Przypisy

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