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.
– pewne zmienne
– pewne stałe
– pewne funkcje jednoargumentowe
![{\displaystyle R(x,c)\lor R(d,y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a514f3e4906f0b25c3b33d4562468d60cb54507b)
Uniwersum Herbranda to
![{\displaystyle R(x,c)\land \neg R(d,f(y))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/975acff7ea084f909b49fab4600fe664960a856a)
Uniwersum Herbranda to
![{\displaystyle R(x,c)\land R(d,f(y))\land R(f(c),g(x))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1774053527394c16ad9264d9a5cc971d3c3ec87e)
Uniwersum Herbranda to
![{\displaystyle x>0\implies s(x)>s(0)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bfc6742f2731d364b9996d4f3e679da2cf8d69a7)
Uniwersum Herbranda to
Przykłady dla formuł bez stałych:
![{\displaystyle R(x)\lor R(y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1f5141d517df103bf4bea06382506d00ab66835)
Uniwersum Herbranda to
(
– dodana stała)
![{\displaystyle x>y\implies s(x)>s(y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7813ce0c2e76b23bf81c64054c0ba824eab9be61)
![{\displaystyle x>y\implies x+z>y+z}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e5dccd0a9106ac186c6aaefff79d5f84a5372d0e)
Uniwersum Herbranda to
(
– dodana stała)