Twierdzenie Craiga

Z Wikipedii, wolnej encyklopedii
Przejdź do nawigacji Przejdź do wyszukiwania

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

Definicje[edytuj | edytuj kod]

Interpolantem nazwiemy taką formułę że i 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]

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