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) ${\displaystyle \forall x.\phi (x)}$ zostały zastąpione przez koniunkcje ${\displaystyle \phi (t_{1})\land \phi (t_{2})\land \cdots \land \phi (t_{n})}$ natomiast egzystencjalne ${\displaystyle \exists x.\phi (x)}$ przez alternatywę ${\displaystyle \phi (t_{1})\lor \phi (t_{2})\lor \cdots \lor \phi (t_{n}),}$ gdzie ${\displaystyle 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