Twierdzenie Craiga

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

DefinicjeEdytuj

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  

TezaEdytuj

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

PrzykładEdytuj

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  

PrzypisyEdytuj

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