Editing Decidability (logic) (section)

==Some undecidable theories==
Some undecidable theories include:<ref name="Monk1976">{{cite book |first=Donald |last=Monk |year =1976 |title =Mathematical Logic |publisher =Springer |page=279 |isbn =9780387901701 |url-access =registration |url =https://archive.org/details/mathematicallogi00jdon }}</ref>

* The set of logical validities in any first-order signature with equality and either: a relation symbol of [[arity]] no less than 2, or two unary function symbols, or one function symbol of arity no less than 2, established by [[Boris Trakhtenbrot|Trakhtenbrot]] in 1953.
* The first-order theory of the natural numbers with addition, multiplication, and equality, established by Tarski and [[Andrzej Mostowski]] in 1949.
* The first-order theory of the rational numbers with addition, multiplication, and equality, established by [[Julia Robinson]] in 1949.
* The first-order theory of [[Group (mathematics)|groups]], established by [[Alfred Tarski]] in 1953.<ref>{{Citation| last1=Tarski| first1=A. | last2=Mostovski| first2=A. | last3=Robinson| first3=R. |  title=Undecidable Theories | publisher=North-Holland, Amsterdam | series=Studies in Logic and the Foundation of Mathematics | year=1953 |url=https://books.google.com/books?id=XtLbjZjB1B8C&pg=PP1 |isbn=9780444533784}}</ref>  Remarkably, not only the general theory of groups is undecidable, but also several more specific theories, for example (as established by Mal'cev 1961) the theory of finite groups. Mal'cev also established that the theory of semigroups and the theory of [[Ring (mathematics)|rings]] are undecidable. Robinson established in 1949 that the theory of [[Field (mathematics)|fields]] is undecidable.
*[[Robinson arithmetic]] (and therefore any consistent extension, such as [[Peano arithmetic]]) is essentially undecidable, as established by [[Raphael Robinson]] in 1950.
* The first-order theory with equality and two function symbols.<ref>{{cite journal |last=Gurevich |first=Yuri |date=1976 |title= The Decision Problem for Standard Classes|url=http://dblp.uni-trier.de/rec/bib/journals/jsyml/Gurevich76 |journal= J. Symb. Log.|volume=41 |issue=2 |pages=460–464 |doi= 10.1017/S0022481200051513|access-date=5 August 2014|citeseerx=10.1.1.360.1517 |s2cid=798307 }}</ref>

The [[interpretability]] method is often used to establish undecidability of theories. If an essentially undecidable theory ''T'' is interpretable in a consistent theory ''S'', then ''S'' is also essentially undecidable. This is closely related to the concept of a [[many-one reduction]] in [[computability theory]].