Twierdzenie Craiga – twierdzenie logiki, a w szczególności rachunku predykatów pierwszego rzędu. Udowodnione przez , amerykańskiego logika.
Definicje 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 Dla każdego zdania rachunku predykatów pierwszego rzędu postaci będącego tautologią istnieje interpolant.
Przykład 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
Craiga