Model Herbranda
Z Wikipedii
Model Herbranda to taki model, w którym:
Na przykład jeśli rozpatrujemy język złożony ze stałej 0, funkcji jednoargumentowej s, funkcji dwuargumentowej + oraz relacji dwuargumentowej >, możemy dać temu językowi wiele interpretacji.
Jedną z nich - dość oczywistą - jest dziedzina złożona z liczb naturalnych, przy czym 0 równe 0, s(x) = x + 1, + (x,y) = x + y, a > (x,y) = x > y.
Ale problem pojawiłby się, jeśli wybralibyśmy liczby rzeczywiste, gdyż nie każdy element dziedziny (która jest nieprzeliczalna) można otrzymać wartościując jakiś term (bo zbiór termów jest przeliczalny).
Jak na przykład udowodnić spełnialność pewnego zbioru formuł? Nie zawsze możemy użyć lematu Hintikki, gdyż jeśli formuła zawiera kwantyfikator ogólny, a nie każdą wartość dziedziny można uzyskać przez pewien term, nie możemy takiego zbioru zapełnić.
Prawdziwe jest jednak następujące twierdzenie:
- jeśli zbiór formuł w rachunku predykatów pierwszego rzędu ma model, to ma też model Herbranda.
Tak więc żeby udowodnić, że coś jest spełnialne lub też nie, wystarczy rozpatrzyć o wiele mniejszą i wygodniejszą klasę modeli, na których możemy już stosować ten sam lemat Hintikki, który był użyty w rachunku zdań.
