Trakhtenbrotův teorém je teorém o nerozhodnutelnosti pravdivosti logických formulí prvního řádu pro konečné modely. Zformuloval ji B. A. Trakhtenbrot v roce 1950 [1] Jejím důsledkem je existence neomezeného počtu formulí vyjadřujících podmínku (a následně i definici) konečnosti množiny a mezi nimi je neomezený počet nezávislých jedničky. [2] Také jeho důsledkem je absence nejslabšího axiomu nekonečna (pro každý axiom nekonečna existuje slabší axiom nekonečna) [3] .
Existuje řada logických vzorců, které vyjadřují podmínku konečnosti množiny, a proto jsou její definice, např.
Důsledkem Trachtebrotovy věty je existence neomezeného počtu takových vzorců a absence toho nejslabšího a nejsilnějšího z nich. [2]
V matematické logice je vzorec považován za silnější než vzorec , pokud vyplývá z , ale nevyplývá z .
Dalším důsledkem Trachtenbrotovy věty je absence nejslabšího axiomu nekonečna [3] .