Uniwersum Herbranda

Szablon:Dopracować Uniwersum Herbranda – dla formuły rachunku predykatów pierwszego rzędu to uniwersum składające się z wszystkich zamkniętych termów złożonych ze stałych i symboli funkcyjnych występujących w formule. Jeśli formuła nie zawiera żadnych stałych, dodaje się do uniwersum dowolną stałą, żeby nie było ono puste.

Jeśli formuła zawiera choć jeden symbol funkcyjny o argumentowości większej niż 0, uniwersum Herbranda jest zbiorem nieskończonym. Uniwersum Herbranda jest zawsze co najwyżej przeliczalne.

Przykłady

• $x,$ $y$ – pewne zmienne
• $c,$ $d$ – pewne stałe
• $f,$ $g$ – pewne funkcje jednoargumentowe

$R(x,c)\vee R(d,y)$

Uniwersum Herbranda to $\{c,d\}.$

$R(x,c)\wedge \mathrm{\neg }R(d,f(y))$

Uniwersum Herbranda to $\{c,f(c),f(f(c)),f(f(f(c))),\dots \}.$

$R(x,c)\wedge R(d,f(y))\wedge R(f(c),g(x))$

Uniwersum Herbranda to $\{c,d,f(c),f(d),g(c),g(d),f(f(c)),f(g(c)),g(f(c)),f(f(d)),\dots \}$

$x>0⟹s(x)>s(0)$

Uniwersum Herbranda to $\{0,s(0),0>0,s(s(0)),s(0)>0,0>s(0),s(0)>s(0),s(s(0))>s(0),\dots \}$

Przykłady dla formuł bez stałych:

$R(x)\vee R(y)$

Uniwersum Herbranda to $\{c\}.$ ($c$ – dodana stała)

$x>y⟹s(x)>s(y)$

$x>y⟹x+z>y+z$

Uniwersum Herbranda to $\{c,s(c),c+c,s(s(c)),s(c)+c,c+s(c),s(c)+s(c),s(s(c))+s(c),\dots \}.$ ($c$ – dodana stała)