Nella logica matematica , il teorema di Trakhtenbrot afferma che il problema della validità di una formula di logica del primo ordine sulla classe dei modelli finiti è indecidibile . In altre parole, non esiste un algoritmo che prenda come input una formula con quantificatori del primo ordine come "per tutte le x, esiste y tale che y è il padre di x" e che risponde sì se la formula è vera. In qualsiasi situazione con un numero finito di elementi e non altrimenti.
Questo teorema è stato dimostrato da Boris Trakhtenbrot nel 1950. Il teorema ha un impatto importante: mostra che non esiste un sistema completo di deduzione per le validità nella logica del primo ordine su modelli finiti.
Ci sono dimostrazioni in vari libri.