Twierdzenie Craiga

Z Wikipedii

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

Spis treści 1 Definicje 2 Teza 3 Przykład 4 Bibliografia 5 Zobacz też

[edytuj] Definicje

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

[edytuj] Teza

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

[edytuj] 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 q oraz symbolu funkcyjnego f, nie wolno zaś używać predykatów p,r, ani też symboli funkcyjnych g i h.

Łatwo zgadnąć, że szukanym interpolantem jest q(f(x)), 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ą X i Y.

[edytuj] Bibliografia

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

[edytuj] Zobacz też

• przegląd zagadnień z zakresu matematyki.

To jest tylko zalążek artykułu związanego z matematyką. Jeśli potrafisz, rozbuduj go.