Rozwinięcie Herbranda

Rozwinięcie Herbranda dla formuły rachunku predykatów pierwszego rzędu to formuła, w której wszystkie kwantyfikatory ogólne (a także zmienne wolne) $\mathrm{\forall }x.\varphi (x)$ zostały zastąpione przez koniunkcje $\varphi (t_1)\wedge \varphi (t_2)\wedge \cdots \wedge \varphi (t_n)$ natomiast egzystencjalne $\mathrm{\exists }x.\varphi (x)$ przez alternatywę $\varphi (t_1)\vee \varphi (t_2)\vee \cdots \vee \varphi (t_n),$ gdzie $t_1,t_2,\dots ,t_n$ to pewien podzbiór skończony uniwersum Herbranda.

Taka formuła – bez zmiennych i kwantyfikatorów jest w praktyce równoważna pewnej formule rachunku zdań.

Zbiór rozwinięć Herbranda jest co najwyżej przeliczalny.

Zobacz też

• twierdzenie Herbranda