Editing Decidability (logic) (section)

==Some decidable theories==

Some decidable theories include (Monk 1976, p.&nbsp;234):<ref name=Monk1976 />
* The set of first-order logical validities in the signature with only equality, established by [[Leopold Löwenheim]] in 1915.
* The  set of first-order logical validities in a signature with equality and one unary function, established by Ehrenfeucht in 1959.
* The first-order theory of the natural numbers in the signature with equality and addition, also called [[Presburger arithmetic]]. The completeness was established by [[Mojżesz Presburger]] in 1929.
* The first-order theory of the natural numbers in the signature with equality and multiplication, also called [[Skolem arithmetic]].
* The first-order theory of [[Boolean algebras canonically defined|Boolean algebras]], established by [[Alfred Tarski]] in 1940 (found in 1940 but announced in 1949).
* The first-order theory of [[algebraically closed field]]s of a given [[characteristic (algebra)|characteristic]], established by Tarski in 1949.
* The [[Decidability of First-order Theory of Real Numbers|first-order theory of real-closed ordered fields]], [[Tarski–Seidenberg theorem|established by Tarski in 1949]] (see also [[Tarski's exponential function problem]]).
* The first-order theory of [[Euclidean geometry]], established by Tarski in 1949.
* The first-order theory of [[Abelian group]]s, established by Szmielew in 1955.
* The first-order theory of [[hyperbolic geometry]], established by Schwabhäuser in 1959.
* Specific [[decidable sublanguages of set theory]] investigated in the 1980s through today.(Cantone ''et al.'', 2001)
* The [[monadic second-order logic|monadic second-order]] theory of [[tree (graph theory)|trees]] (see [[S2S (mathematics)|S2S]]).

Methods used to establish decidability include [[quantifier elimination]], [[model completeness]], and the [[Łoś-Vaught test]].