Herbrand, teorema di

Herbrand, teorema di

Herbrand, teorema di o teorema di Herbrand-Tarski, in logica, altra denominazione del teorema di deduzione, dimostrato da J. Herbrand nella sua opera del 1930, ma già delineato da A. Tarski nell’anno precedente. Il teorema stabilisce un collegamento tra una teoria logica contenente anche assiomi non logici, ma specifici, e la teoria logica generale, indipendente da essi (→ deduzione, teorema di). Con la denominazione teorema di Herbrand sono riportati anche altri risultati del giovane logico francese; in particolare, la possibilità di ridurre algoritmicamente questioni relative alla logica del primo ordine alla logica proposizionale. Per questo tale risultato ha avuto una notevole importanza nel successivo sviluppo di procedure di dimostrazione automatica.