Büchi–Elgot–Trakhtenbrot theorem

{{Short description|Formal language theorem}}

In formal language theory, the Büchi–Elgot–Trakhtenbrot theorem states that a language is regular if and only if it can be defined in monadic second-order logic (MSO): for every MSO formula, we can find a finite-state automaton defining the same language, and for every finite-state automaton, we can find an MSO formula defining the same language. The theorem is due to Julius Richard Büchi,{{cite journal |last1=Büchi |first1=Julius Richard |title=Weak second order arithmetic and finite automata |journal=Zeitschrift für Mathematische Logik und Grundlagen der Mathematik |date=1960 |volume=6 |issue=1–6 |pages=66–92|doi=10.1002/malq.19600060105 }} Calvin Elgot,{{cite journal |last1=Elgot |first1=Calvin C. |title=Decision problems of finite automata design and related arithmetics |journal=Transactions of the American Mathematical Society |date=1961 |volume=98 |pages=21–52|doi=10.1090/S0002-9947-1961-0139530-9 |s2cid=119721061 |doi-access=free |hdl=2027.42/4758 |hdl-access=free }} and Boris Trakhtenbrot.{{cite journal |last1=Trakhtenbrot |first1=Boris A. |title=Конечные автоматы и логика одноместных предикатов |language=Russian |trans-title=Finite automata and the logic of one-place predicates |journal=Siberian Mathematical Journal |date=1962 |volume=3 |pages=103–131}}{{cite journal |last1=Trakhtenbrot |first1=Boris A. |title=Finite automata and the logic of one-place predicates |journal=American Mathematical Society Translations |series=American Mathematical Society Translations: Series 2 |date=1966 |volume=59 |pages=23–55|doi=10.1090/trans2/059/02 |isbn=9780821817599 }}