Tekst źródłowy strony Rozwinięcie Herbranda

'''Rozwinięcie Herbranda''' dla formuły [[rachunek predykatów pierwszego rzędu|rachunku predykatów pierwszego rzędu]] to formuła, w której wszystkie [[kwantyfikator ogólny|kwantyfikatory ogólne]] (a także zmienne wolne) <math>\forall x . \phi(x)</math> zostały zastąpione przez [[Koniunkcja (logika)|koniunkcje]] <math>\phi(t_1) \land \phi(t_2) \land \cdots \land \phi(t_n)</math> natomiast [[kwantyfikator egzystencjalny|egzystencjalne]] <math>\exists x . \phi(x)</math> przez [[alternatywa|alternatywę]] <math>\phi(t_1) \lor \phi(t_2) \lor \cdots \lor \phi(t_n),</math> gdzie <math>t_1, t_2, \dots, t_n</math> to pewien podzbiór skończony [[uniwersum Herbranda]].

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

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

== Zobacz też ==
* [[twierdzenie Herbranda]]

[[Kategoria:Logika matematyczna]]