Twierdzenie Craiga
Twierdzenie Craiga – twierdzenie 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łę że i są tautologiami, zaś w nie występuje żadna relacja ani symbol funkcyjny (w tym stała), która nie występuje jednocześnie w i
Teza[edytuj | edytuj kod]
Dla każdego zdania rachunku predykatów pierwszego rzędu postaci będącego tautologią istnieje interpolant.
Przykład[edytuj | edytuj kod]
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[edytuj | edytuj kod]
- ↑ William Craig: Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symb. Logic 22 1957, s. 250–268.