View source for List of first-order theories

{{Short description|Theories in mathematical logic}}
In [[first-order logic]], a first-order theory is given by a [[Set (mathematics)|set]] of axioms in some
language. This entry lists some of the more common examples used in [[model theory]] and some of their properties.

{{TOC right}}

==Preliminaries==

For every natural mathematical structure there is a  [[Signature (logic)|signature]] &sigma;  listing the constants, functions, and relations of the theory together with their [[Arity|arities]],  so that the object is naturally a [[model theory|&sigma;-structure]].   Given a signature &sigma; there is a unique first-order language  ''L''<sub>&sigma;</sub> that can be used to capture the first-order expressible facts about the &sigma;-structure.

There are two common ways to specify theories:
#List or describe a set of [[Sentence (mathematical logic)|sentences]] in the language ''L''<sub>&sigma;</sub>, called the '''axioms''' of the theory.
#Give a set of  &sigma;-structures, and define a theory to be the set of sentences in ''L''<sub>&sigma;</sub> holding in all these models. For example, the "theory of finite fields" consists of all sentences in the language of fields that are true in all finite fields.

An L<sub>&sigma;</sub> theory may:
*be consistent: no proof of contradiction exists;
* be satisfiable: there exists a &sigma;-structure for which the sentences of the theory are all true (by the [[completeness theorem]], satisfiability is equivalent to consistency);
*be complete: for any statement, either it or its negation is provable;
*have [[quantifier elimination]];
*[[elimination of imaginaries|eliminate imaginaries]];
* be [[Axiom_schema#Finite_axiomatization|finitely axiomatizable]];
*be [[Decidability (logic)|decidable]]: There is an algorithm to decide which statements are provable;
*be recursively axiomatizable;
*be [[model complete]] or sub-model complete;
*be [[Morley's categoricity theorem|κ-categorical]]: All models of [[cardinality]] κ are isomorphic;
*be [[stable theory|stable]]  or unstable;
*be [[ω-stable]] (same as [[totally transcendental]] for [[Countable set|countable]] theories);
*be [[superstable]]
*have an [[atomic model (mathematical logic)|atomic model]];
*have a [[prime model]];
*have a [[saturated model]].

==Pure identity theories==

{{Main|Theory of pure equality}}

The signature of the pure identity theory is empty, with no functions, constants, or relations.

'''Pure identity theory''' has no (non-logical) axioms. It is decidable.

One of the few interesting properties that can be stated in the language of pure identity theory is that of being infinite.
This is given by an infinite set of axioms stating there are at least 2 elements, there are at least 3 elements, and so on:
*∃''x''<sub>1</sub> ∃''x''<sub>2</sub> ¬''x''<sub>1</sub> = ''x''<sub>2</sub>,    ∃''x''<sub>1</sub> ∃''x''<sub>2</sub> ∃''x''<sub>3</sub> ¬''x''<sub>1</sub> = ''x''<sub>2</sub> ∧ ¬''x''<sub>1</sub> = ''x''<sub>3</sub> ∧ ¬''x''<sub>2</sub> = ''x''<sub>3</sub>,...
These axioms define the '''theory of an infinite set'''.

The opposite property of being finite cannot be stated in [[first-order logic]] for any theory that has arbitrarily large finite models: in fact any such  theory has infinite models by the [[compactness theorem]]. In general if a property can be stated by a finite number of sentences of first-order logic then the opposite property can also be stated in first-order logic, but if a property needs an infinite number of sentences then its opposite property cannot be stated in first-order logic.

Any statement of pure identity theory is equivalent to either σ(''N'') or to ¬σ(''N'') for some finite [[subset]] ''N'' of the [[non-negative integer]]s, where σ(''N'') is the statement that the number of elements is in ''N''. It is even possible to describe all possible theories in this language as follows. Any theory is either  the theory of all sets of cardinality in ''N'' for some ''finite'' subset ''N'' of the non-negative integers, or the theory of all sets whose cardinality is not in ''N'', for some ''finite or infinite'' subset ''N'' of the non-negative integers. (There are no theories whose models are exactly sets of cardinality ''N'' if ''N'' is an infinite subset of the integers.) The complete theories are the theories of sets of cardinality ''n'' for some finite ''n'', and the theory of infinite sets.

One special case of this is the '''inconsistent theory''' defined by the axiom ∃''x'' ¬''x'' = ''x''. It is a perfectly good theory with many good properties: it is complete, decidable, finitely axiomatizable, and so on. The only problem is that it has no models at all. By Gödel's completeness theorem, it is the only theory (for any given language) with no models.<ref>{{citation|title=Propositional and Predicate Calculus: A Model of Argument: A Model of Argument|first=Derek|last=Goldrei|publisher=Springer|year=2005|isbn=9781846282294|url=https://books.google.com/books?id=edqwSVJ9GGQC&pg=PA265|page=265}}.</ref> It is not the same as the theory of the [[empty set]] (in versions of first-order logic that allow a model to be empty): the theory of the empty set has exactly one model, which has no elements.

==Unary relations==
A set of unary  relations ''P''<sub>''i''</sub> for ''i'' in some set ''I'' is called '''independent''' if for every two disjoint finite subsets ''A'' and ''B'' of ''I''  there is some element ''x'' such that ''P''<sub>''i''</sub>(''x'') is true for ''i'' in ''A'' and false for ''i'' in ''B''. Independence can be expressed by a set of first-order statements.

The '''theory of a countable number of independent unary relations''' is complete, but has no [[atomic model (mathematical logic)|atomic models]]. It is also an example of a theory that is [[superstable]] but not [[totally transcendental]].

==Equivalence relations==
The signature of [[equivalence relation]]s has one binary infix relation symbol ~, no constants, and no functions. Equivalence relations satisfy the axioms:
*'''[[Reflexive relation|Reflexive]]''' ∀''x'' ''x''~''x'';
*'''[[Symmetric relation|Symmetric]]''' ∀''x'' ∀''y'' ''x''~''y'' → ''y''~''x'';
*'''[[Transitive relation|Transitive]]''': ∀''x'' ∀''y'' ∀''z'' (''x''~''y'' ∧ ''y''~''z'') → ''x''~''z''.

Some first-order properties of equivalence relations are:
*~ has an infinite number of [[equivalence classes]];
*~ has exactly ''n'' equivalence classes (for any fixed positive integer ''n'');
*All equivalence classes are infinite;
*All equivalence classes have size exactly ''n'' (for any fixed positive integer ''n'').

The theory of an equivalence relation with exactly 2 infinite [[equivalence class]]es is an easy example of a theory which is ω-categorical but not categorical for any larger [[cardinal number|cardinal]].

The equivalence relation ~ should not be confused with the [[identity (philosophy)|identity]] symbol '=': if ''x''=''y'' then ''x''~''y'', but the converse is not necessarily true. Theories of equivalence relations are not all that difficult or interesting, but often give easy examples or counterexamples for various statements.

The following constructions are sometimes used to produce examples of theories with certain [[spectrum of a theory|spectra]]; in fact by applying them to a small number of explicit theories ''T'' one gets examples of complete countable theories with all possible uncountable spectra. If ''T'' is a theory in some language, we define a new theory 2<sup>''T''</sup> by adding a new binary relation to the language, and adding axioms stating that it is an equivalence relation, such that there are an infinite number of equivalence classes all of which are [[model theory|model]]s of ''T''. It is  possible to iterate this construction [[transfinite induction|transfinitely]]: given an [[ordinal number|ordinal]] α, define a new theory by adding an equivalence relation ''E<sub>β</sub>'' for each β&lt;α, together with axioms stating that whenever β&lt;γ then each ''E<sub>γ</sub>'' equivalence class is the union of infinitely many ''E<sub>β</sub>'' equivalence classes, and each ''E<sub>0</sub>'' equivalence class is a model of ''T''. Informally, one can visualize models of this theory as infinitely branching trees of height α with models of ''T'' attached to all leaves.

==Orders==
The signature of [[List of order structures in mathematics|orders]] has no constants or functions, and one binary relation symbols ≤. (It is of course possible to use ≥, &lt; or &gt; instead as the basic relation, with the obvious minor changes to the axioms.)
We define ''x'' ≥ ''y'', ''x'' &lt; ''y'', ''x'' &gt; ''y'' as abbreviations for ''y'' ≤ ''x'', ''x'' ≤ ''y'' ∧¬''y'' ≤ ''x'', ''y'' &lt; ''x'',

Some first-order properties of orders: 
*'''Transitive''': ∀''x'' ∀''y'' ∀''z'' (''x'' ≤ ''y)'' ∧ (''y'' ≤ ''z)'' → ''x'' ≤ ''z''
*'''Reflexive''': ∀''x'' ''x'' ≤ ''x''
*'''[[Antisymmetric relation|Antisymmetric]]''': ∀''x'' ∀''y'' (''x'' ≤ ''y)'' ∧ (''y'' ≤ ''x)'' → ''x'' = ''y''
*'''[[Partial order|Partial]]''': Transitive ∧ Reflexive ∧ Antisymmetric;
*'''[[Linear order|Linear]]''' (or '''total'''): Partial ∧ ∀''x'' ∀''y'' (''x'' ≤ ''y)'' ∨ (''y'' ≤ ''x)''
*'''[[Dense order|Dense]]''' ("Between any 2 distinct elements there is another element"): ∀''x'' ∀''z'' (''x'' &lt; ''z)'' → ∃''y'' (''x'' &lt; ''y)'' ∧ (''y'' &lt; ''z)'' 
*There is a smallest element: ∃''x'' ∀''y'' (''x'' ≤ ''y)''
*There is a largest element: ∃''x'' ∀''y'' (''y'' ≤ ''x)''
*Every element has an immediate successor: ∀''x'' ∃''y'' ∀''z'' (''x'' &lt; ''z)'' ↔ (''y'' ≤ ''z)''
The theory DLO of ''dense linear orders without endpoints'' (i.e. no smallest or largest element) is complete, ω-categorical, but not categorical for any uncountable cardinal. There are three other very similar theories: the theory of dense linear orders with a:
* Smallest but no largest element;
* Largest but no smallest element;
* Largest and smallest element.

Being '''[[Well-ordered set|well ordered]]''' ("any non-empty subset has a minimal element") is not a first-order property; the usual definition involves quantifying over all ''subsets''.

==Lattices==
[[lattice (order)|Lattices]] can be considered either as special sorts of partially ordered sets, with a signature consisting of one binary relation symbol &le;, or as [[algebraic structure]]s with a signature consisting of two binary operations &and; and &or;. The two approaches can be related  by defining  ''a'' &le; ''b'' to mean ''a''&and;''b'' = ''a''.

For two binary operations the axioms for a lattice are:
{| style="margin-left: 2em;"
| '''[[commutative operation|Commutative]] laws:''' ||
| <math> \forall a \forall b \; a  \vee b = b \vee a </math> || || <math> \forall a \forall b\; a \wedge  b = b \wedge a </math>
|-
| '''[[associativity|Associative]] laws:''' ||
| <math>\forall a \forall b \forall c\; a \vee (b \vee c) = (a \vee b) \vee c </math> || || <math> \forall a \forall b \forall c\; a \wedge (b \wedge c) = (a \wedge b) \wedge c </math>
|-
| '''[[Absorption law]]s:''' ||
| <math> \forall a \forall b \;a  \vee (a \wedge b) = a </math> || || <math>\forall a \forall b \;a  \wedge (a \vee b) = a </math>
|}

For one relation &le; the axioms are:
*Axioms stating &le; is a partial order, as above.
*<math>\forall a \forall b \exist c\; c \le a \wedge c \le b \wedge \forall d\;d \le a \wedge d \le b \rightarrow d \le c</math> (existence of c = a&and;b)
*<math>\forall a \forall b \exist c\; a \le c \wedge b \le c \wedge \forall d\;a \le d \wedge b \le d \rightarrow c \le d</math> (existence of c = a&or;b)

First-order properties include:
* <math>\forall x \forall y\forall z\;x \vee (y \wedge z) = (x \vee y) \wedge (x \vee z)</math> ([[distributive lattice]]s)
* <math>\forall x \forall y\forall z\;x \vee (y \wedge (x \vee z)) = (x \vee y) \wedge (x \vee z)</math> ([[modular lattice]]s)

[[Heyting algebra]]s can be defined as lattices with certain extra first-order properties.

[[Complete lattice|Completeness]] is not a first-order property of lattices.

==Graphs==
{{main|Logic of graphs}}
The signature of [[Graph (discrete mathematics)|graphs]] has no constants or functions, and one binary relation symbol ''R'', where ''R''(''x'',''y'') is read as "there is an edge from ''x'' to ''y''".

The axioms for the '''theory of graphs''' are
*'''Symmetric''': ∀''x'' ∀''y'' ''R''(''x'',''y'')→ ''R''(''y'',''x'')
*'''[[Anti-reflexive]]''': ∀''x'' ¬''R''(''x'',''x'') ("no [[Loop (graph theory)|loops]]")

The ''theory of random graphs'' has the following extra axioms for each positive integer ''n'':
* For any two disjoint finite sets of size ''n'', there is a point joined to all points of the first set and to no points of the second set. (For each fixed ''n'', it is easy to write this statement in the language of graphs.)

The theory of random graphs is ω categorical, complete, and decidable, and its countable model is called the [[Rado graph]]. A statement in the language of graphs is true in this theory if and only if the probability that an ''n''-vertex [[random graph]] models the statement tends to 1 in the limit as ''n'' goes to infinity.

==Boolean algebras==
There are several different signatures and conventions used for '''[[Boolean algebras]]''': 
#The signature has two constants, 0 and 1, and two binary functions ∧ and ∨ ("and" and "or"), and one unary function ¬ ("not"). This can be confusing as the functions use the same symbols as the [[propositional function]]s of first-order logic.
#In [[set theory]], a common convention is that the language has two constants, 0 and 1, and two binary functions · and +, and one unary function &minus;. The three functions have the same interpretation as the functions in the first convention. Unfortunately, this convention clashes badly with the next convention:
#In [[algebra]], the usual convention is that the language has two constants, 0 and 1, and two binary functions · and +. The function · has the same meaning as ∧, but ''a''+''b'' means ''a''∨''b''∧¬(''a''∧''b''). The reason for this is that the axioms for a Boolean algebra are then just the axioms for a ring with 1 plus ∀''x'' ''x''<sup>2</sup> = ''x''. Unfortunately this clashes with the standard convention in set theory given above.

The axioms are:
*The axioms for a distributive lattice (see above)
*&forall;a ''a''&and;¬''a'' = 0, &forall;a ''a''&or;¬''a'' = 1 (properties of negation)
*Some authors add the extra axiom ¬0 = 1, to exclude the trivial algebra with one element.

Tarski proved that the theory of Boolean algebras is decidable.

We write ''x'' ≤ ''y'' as an abbreviation for ''x''∧''y'' = ''x'', and atom(''x'') as an abbreviation for ¬''x'' = 0 ∧ ∀''y'' ''y'' ≤ ''x'' → ''y'' = 0 ∨ ''y'' = ''x'', read as "''x'' is an atom", in other words a non-zero element with nothing between it and 0. Here are some first-order properties of Boolean algebras:
*'''Atomic''': ∀''x'' ''x'' = 0 ∨ ∃''y'' ''y'' ≤ ''x'' ∧ atom(''y'')
*'''Atomless''': ∀''x'' ¬atom(''x'')
The theory of '''atomless Boolean algebras''' is ω-categorical and complete.

For any Boolean algebra ''B'', there are several invariants defined as follows. 
*the ideal ''I''(''B'') consists of elements that are the sum of an atomic and an atomless element (an element with no atoms below it).
*The quotient algebras ''B''<sup>''i''</sup> of ''B'' are defined inductively by ''B''<sup>0</sup>=''B'', ''B''<sup>''k''+1</sup> = ''B''<sup>''k''</sup>/''I''(''B''<sup>''k''</sup>).
*The invariant ''m''(''B'') is the smallest integer such that ''B''<sup>''m''+1</sup> is trivial, or &infin; if no such integer exists.
*If ''m''(''B'') is finite, the invariant ''n''(''B'') is the number of atoms of ''B''<sup>''m''(''B'')</sup> if this number is finite, or &infin; if this number is infinite.
*The invariant ''l''(''B'') is 0 if ''B''<sup>''m''(''B'')</sup> is atomic or if ''m''(''B'') is &infin;, and 1 otherwise.

Then two Boolean algebras are [[Elementary equivalence|elementarily equivalent]] if and only if their invariants ''l'', ''m'', and ''n'' are the same. In other words, the values of these invariants classify the possible completions of the theory of Boolean algebras. So the possible complete theories are:
*The trivial algebra (if this is allowed; sometimes 0&ne;1 is included as an axiom.)
*The theory with ''m'' = &infin;
*The theories with ''m'' a natural number, ''n'' a natural number or &infin;, and ''l'' = 0 or 1 (with ''l'' = 0 if ''n'' = 0).

==Groups==
The signature of [[group theory]] has one constant 1 (the identity), one function of arity 1 (the inverse) whose value on ''t'' is denoted by ''t''<sup>&minus;1</sup>, and one function of arity 2, which is usually omitted from terms. For any integer ''n'', ''t''<sup>''n''</sup> is an abbreviation for the obvious term for the ''n''th power of ''t''.

'''[[Group (mathematics)|Group]]s''' are defined by the axioms
*''Identity'': ∀''x'' 1''x'' = ''x'' ∧ ''x''1 = ''x''
*''Inverse'': ∀''x'' ''x''<sup>&minus;1</sup>''x'' = ''1'' ∧ ''xx''<sup>&minus;1</sup> = ''1''
*''Associativity'': ∀''x''∀''y''∀''z'' (''xy'')''z'' = ''x''(''yz'')

Some properties of groups that can be defined in the first-order language of groups are:
*'''[[Abelian group|Abelian]]''': ∀''x'' ∀''y'' ''xy'' = ''yx''.
*'''[[Torsion-free group|Torsion free]]''': ∀''x'' ''x''<sup>2</sup> = 1→''x'' = 1, ∀''x'' ''x''<sup>3</sup> = 1 → ''x'' = 1, ∀''x'' ''x''<sup>4</sup> = 1 → ''x'' = 1, ...
*'''[[Divisible group|Divisible]]''': ∀''x'' ∃''y'' ''y''<sup>2</sup> = ''x'', ∀''x'' ∃''y'' ''y''<sup>3</sup> = ''x'', ∀''x'' ∃''y'' ''y''<sup>4</sup> = ''x'', ...
*'''Infinite''' (as in identity theory)
*'''[[Torsion group|Exponent]]''' ''n'' (for any fixed positive integer ''n''): ∀''x'' ''x''<sup>''n''</sup> = 1
*[[Nilpotent group|Nilpotent]] of class ''n'' (for any fixed positive integer ''n'')
*[[solvable group|Solvable]] of class ''n'' (for any fixed positive integer ''n'')

The theory of '''abelian groups''' is decidable.<ref>{{citation
 | last = Szmielew | first = W. | authorlink = Wanda Szmielew
 | journal = Fundamenta Mathematicae
 | mr = 0072131
 | pages = 203–271
 | title = Elementary properties of Abelian groups
 | volume = 41
 | issue = 2 | year = 1955
 | doi=10.4064/fm-41-2-203-271| doi-access = free
 }}.</ref> The theory of '''infinite divisible torsion-free abelian groups''' is complete, as is the theory of '''infinite abelian groups of exponent p''' (for ''p'' [[Prime number|prime]]).

The theory of '''finite groups''' is the set of first-order statements in the language of groups that are true in all finite groups (there are plenty of infinite models of this theory). It is not completely trivial to find any such statement that is not true for all groups: one example is 
"given two elements of order 2, either they are conjugate or there is a non-trivial element commuting with both of them".

The properties of being finite, or [[Free group|free]], or [[Simple group|simple]], or torsion are not first-order. More precisely, the first-order theory of all groups with one of these properties has models that do not have this property.

==Rings and fields==
The signature of (unital) [[Ring (mathematics)|rings]] has two constants 0 and 1, two binary functions + and &times;, and, optionally, one unary negation function &minus;.

'''Rings'''

Axioms: Addition makes the ring into an abelian group, multiplication is associative and has an identity 1, and multiplication is left and right distributive.

'''[[Commutative ring]]s'''

The axioms for rings plus ∀''x'' ∀''y'' ''xy'' = ''yx''.

'''[[Field (mathematics)|Field]]s'''

The axioms for commutative rings plus ∀''x'' (¬ ''x'' = 0 → ∃''y'' ''xy'' = 1) and ¬ 1 = 0.
Many of the examples given here have only universal, or ''algebraic'' axioms.  The [[Class (set theory)|class]] of structures satisfying such a theory has the property of being closed under substructure.   For example, a subset of a group closed under the group actions of multiplication and inverse is again a group.  Since the signature of fields does not usually include multiplicative and additive inverse, the axioms for  inverses are not universal, and therefore a substructure of a field closed under addition and multiplication  is not always a field.   This can be remedied by adding unary inverse functions to the language.

For any positive integer ''n'' the property that all equations of degree ''n'' have a root can be expressed by a single first-order sentence:
*∀ ''a''<sub>1</sub> ∀ ''a''<sub>2</sub>... ∀ ''a''<sub>''n''</sub> ∃''x'' (...((''x''+''a''<sub>1</sub>)''x'' +''a''<sub>2</sub>)''x''+...)''x''+''a''<sub>''n''</sub> = 0

'''[[Perfect field]]s'''

The axioms for fields, plus axioms for each prime number ''p'' stating that if ''p''&nbsp;1 = 0 (i.e. the field has [[field characteristic|characteristic]] ''p''), then every field element has a ''p''th root.

'''Algebraically closed fields of characteristic ''p'''''

The axioms for fields, plus for every positive ''n'' the axiom that all polynomials of degree ''n'' have a root, plus axioms fixing the characteristic. The classical examples of complete theories. [[Category theory|Categorical]] in all uncountable cardinals. The theory ''ACF''<sub>p</sub> has a ''universal domain property'', in the sense that every structure ''N'' satisfying the universal axioms of  ''ACF''<sub>p</sub> is a substructure of a sufficiently large algebraically closed field  <math> M \models ACF_0 </math>, and additionally any two such embeddings ''N'' &rarr; ''M'' induce an [[automorphism]] of ''M''.

'''[[Finite field]]s'''

The theory of finite fields is the set of all first-order statements that are true in all finite fields. Significant examples of such statements can, for example, be given by applying the [[Chevalley–Warning theorem]], over the [[prime field]]s. The name is a little misleading as the theory has plenty of infinite models. Ax proved that the theory is decidable.

'''[[Formally real field]]s'''

The axioms for fields plus, for every positive integer ''n'', the axiom:
* ∀ ''a''<sub>1</sub> ∀ ''a''<sub>2</sub>... ∀ ''a''<sub>''n''</sub> ''a''<sub>1</sub>''a''<sub>1</sub>+''a''<sub>2</sub>''a''<sub>2</sub>+ ...+''a''<sub>''n''</sub>''a''<sub>''n''</sub>=0 → ''a''<sub>''1''</sub>=0∧''a''<sub>''2''</sub>=0∧ ... ∧''a''<sub>''n''</sub>=0.
That is, 0 is not a non-trivial sum of squares.

'''[[Real closed field]]s'''

The axioms for formally real fields plus the axioms:
*∀''x'' ∃''y'' (''x''=''yy'' ∨ ''x''+''yy''= 0);
*for every odd positive integer ''n'', the axiom stating that every polynomial of degree ''n'' has a root.

The theory of real closed fields is effective and complete and therefore decidable (the [[Tarski–Seidenberg theorem]]). The addition of further function symbols (e.g., the exponential function, the sine function) [[Decidability of first-order theories of the real numbers|may change decidability]]. 

''' ''p''-adic fields'''

{{harvtxt|Ax|Kochen|1965}} showed that the theory of ''p''-adic fields is decidable and gave a set of axioms for it.<ref>{{citation
|last=Ax|first= James|author-link =James Ax|last2= Kochen|first2= Simon|author2-link =Simon B. Kochen
|title=Diophantine problems over local fields. II. A complete set of axioms for p-adic number theory.
|journal=Amer. J. Math. |volume=87 |year=1965|pages=631–648|issue=3|doi=10.2307/2373066|jstor=2373066|publisher=The Johns Hopkins University Press
|mr=0184931  }} </ref>

==Geometry==
Axioms for various systems of geometry usually use a typed language, with the different types corresponding to different geometric objects such as points, lines, circles, planes, and so on. The signature will often consist of binary incidence relations between objects of different types; for example, the relation that a point lies on a line. The signature may have more complicated relations; for example ordered geometry might have a ternary "betweenness" relation for 3 points, which says whether one lies between two others, or a "congruence" relation between 2 pairs of points.

Some examples of axiomatized systems of geometry include [[ordered geometry]], [[absolute geometry]], [[affine geometry]], [[Euclidean geometry]], [[projective geometry]],  and [[hyperbolic geometry]]. For each of these geometries there are many different and inequivalent systems of axioms for various dimensions. Some of these axiom systems include "completeness" axioms that are not first order.

As a typical example, the axioms for projective geometry use 2 types, points and lines, and a binary incidence relation between points and lines. If point and line variables are indicated by small and capital letter, and ''a'' incident to ''A'' is written as ''aA'', then one set of axioms is
*<math>\forall a\forall b\;\lnot a=b\rightarrow \exists C\; aC\land bC </math> (There is a line through any 2 distinct points ''a'',''b'' ...)
*<math>\forall a\forall b\forall  C\forall D\; \lnot a=b\land aC\land bC \land aD\land bD\rightarrow C=D</math> (... which is unique)
*<math>\forall a\forall b\forall c\forall d\forall e\forall G\forall H \;aH\land bH\land eH\land cG\land dG\land eG\rightarrow\exists f\exists I\exists J\;  aI\land cI\land fI\land bJ\land dJ\land fJ</math> (Veblen's axiom: if ''ab'' and ''cd'' lie on intersecting lines, then so do ''ac'' and ''bd''.)
*<math>\forall A\exists b\exists c\exists d\; bA\land cA\land dA\land \lnot b=c\land \lnot b=d\land \lnot c=d </math> (Every line has at least 3 points)

Euclid did not state all the axioms for Euclidean geometry explicitly, and the first complete list was given by Hilbert in [[Hilbert's axioms]]. This is not a first-order axiomatization as one of Hilbert's axioms is a second order completeness axiom. [[Tarski's axioms]] are a first-order axiomatization of Euclidean geometry. Tarski showed this axiom system is complete and decidable by relating it to the complete and decidable theory of real closed fields.

==Differential algebra==
* The theory DF of [[differential field]]s.
The signature is that of fields (0, 1, +, −, ×) together with a unary function ∂, the derivation.
The axioms are those for fields together with
:<math>\forall u\forall v\,\partial(uv) = u \,\partial v + v\, \partial u</math>
:<math>\forall u\forall v\,\partial (u + v) = \partial u + \partial v\ .</math>
For this theory one can add the condition that the characteristic is ''p'', a prime or zero,
to get the theory DF<sub>''p''</sub> of '''differential fields of characteristic ''p'' '''(and similarly with the other theories below).

If ''K'' is a differential field then the '''field of constants''' <math> k = \{u \in K : \partial(u) = 0\}.</math>
The theory of '''differentially perfect fields''' is the theory of differential fields together with the condition that the field of constants is perfect; in other words, for each prime ''p'' it has the axiom:
:<math>\forall u \,\partial(u)=0 \land p 1 = 0\rightarrow \exists v\,  v^p=u</math>
(There is little point in demanding that the whole field should be a [[perfect field]], because in non-zero characteristic this implies the differential is 0.)
For technical reasons to do with [[quantifier elimination]], it is sometimes more convenient to force the constant field to be perfect by adding a new symbol ''r'' to the signature with the axioms
:<math>\forall u \,\partial(u)=0 \land p 1 = 0 \rightarrow r(u)^p=u</math>
:<math>\forall u \,\lnot \partial(u)=0\rightarrow r(u)=0.</math>
* The theory of '''[[differentially closed field]]s''' (DCF) is the theory of differentially perfect fields with axioms saying that if ''f'' and ''g'' are  [[differential polynomial]]s and the [[separant]] of ''f'' is nonzero  and ''g''≠0 and  ''f'' has order greater than that of ''g'', then there is some ''x'' in the field with ''f''(''x'')=0 and ''g''(''x'')≠0.

==Addition==
The '''theory of the natural numbers with a successor function''' has signature consisting of a constant 0 and a unary function ''S'' ("successor": ''S''(''x'') is interpreted as ''x''+1), and has axioms:
# ∀x &not; Sx = 0
# ∀x∀y Sx = Sy → x = y
#Let ''P''(''x'') be a [[Well-formed formula|first-order formula]] with a single [[free variable]] ''x''. Then the following formula is an axiom:
:(''P''(0) &and; &forall;''x''(''P''(''x'')&rarr;''P''(''Sx''))) &rarr; &forall;''y'' ''P''(''y'').
The last axiom (induction) can be replaced by the axioms
*For each integer ''n''>0, the axiom ∀x SSS...Sx ≠ x (with ''n'' copies of ''S'')
* ∀x &not; x = 0 → ∃y Sy = x

The theory of the natural numbers with a successor function is complete and decidable, and is &kappa;-categorical for uncountable &kappa; but not for countable &kappa;.

'''[[Presburger arithmetic]]''' is the theory of the natural numbers under addition, with signature consisting of a constant 0, a unary function ''S'', and a binary function +. It is complete and decidable. The axioms are 
# ∀x &not; Sx = 0
# ∀x∀y Sx = Sy → x = y
# ∀x x + 0 = x
# ∀x∀y x + Sy = S(x + y)
#Let ''P''(''x'') be a first-order formula with a single free variable ''x''. Then the following formula is an axiom:
:(''P''(0) &and; &forall;''x''(''P''(''x'')&rarr;''P''(''Sx''))) &rarr; &forall;''y'' ''P''(''y'').

==Arithmetic==
Many of the first-order theories described above can be extended to complete recursively enumerable consistent theories. This is no longer true for most of the following theories; they can usually encode both multiplication and addition of natural numbers, and this gives them enough power to encode themselves, which implies that [[Gödel's incompleteness theorem]] applies and the theories can no longer be both complete and recursively enumerable (unless they are inconsistent).

The signature of a theory of arithmetic has:
*The constant 0;
*The [[unary function]], the [[successor function]], here denoted by prefix ''S'', or by prefix &sigma; or postfix &prime; elsewhere;
*Two [[binary function]]s, denoted by infix + and &times;, called "addition" and "multiplication."
Some authors take the signature to contain a constant 1 instead of the function ''S'', then define ''S'' in the obvious way as  ''St'' = 1 + ''t''.

'''[[Robinson arithmetic]]''' (also called '''Q'''). Axioms (1) and (2) govern the distinguished element 0. (3) assures that ''S'' is an [[Injective function|injection]]. Axioms (4) and (5) are the standard recursive definition of addition; (6) and (7) do the same for multiplication.  Robinson arithmetic  can be thought of as  Peano arithmetic without induction. '''Q''' is  a weak theory for which [[Gödel's incompleteness theorems|Gödel's incompleteness theorem]] holds.
Axioms:
# ∀''x'' &not; S''x'' = 0
# ∀''x'' &not; ''x'' = 0 → ∃''y'' S''y'' = ''x''
# ∀''x''∀''y'' S''x'' = S''y'' → ''x'' = ''y''
# ∀''x'' ''x'' + 0 = ''x''
# ∀''x''∀''y'' ''x'' + S''y'' = S(''x'' + ''y'')
# ∀''x'' ''x'' &times; 0 = 0
# ∀''x''∀''y'' ''x'' &times; S''y'' = (''x'' &times; ''y'') + ''x''.

'''I&Sigma;<sub>n</sub>''' is first-order Peano arithmetic with induction restricted to [[Arithmetical hierarchy|Σ<sub>n</sub> formulas]] (for ''n'' = 0, 1, 2, ...). The theory I&Sigma;<sub>0</sub> is often denoted by I&Delta;<sub>0</sub>. This is a series of more and more powerful fragments of Peano arithmetic. The case ''n''&nbsp;=&nbsp;1 has about the same strength as  '''[[primitive recursive arithmetic]]''' (PRA).
'''[[Exponential function arithmetic]]''' (EFA) is I&Sigma;<sub>0</sub> with an axiom stating that ''x''<sup>''y''</sup> exists for all ''x'' and ''y'' (with the usual properties).

'''First-order [[Peano arithmetic]]''', '''PA'''. The "standard" theory of arithmetic. The axioms are the axioms of [[Robinson arithmetic]] above, together with the axiom scheme of induction:
* <math>\phi(0) \wedge (\forall x \phi(x) \rightarrow \phi(Sx)) \rightarrow (\forall x \phi(x))</math> for any formula &phi; in the language of '''PA'''. &phi; may contain free variables other than ''x''.
[[Kurt Gödel]]'s  1931 paper proved that '''PA''' is incomplete, and has no consistent recursively enumerable completions.

'''Complete arithmetic''' (also known as '''true arithmetic''') is the theory of the standard model of arithmetic, the natural numbers '''N'''. It is complete but does not have a recursively enumerable set of axioms.

For the '''real numbers''', the situation is slightly different: The case that includes just addition and multiplication cannot encode the integers, and hence [[Gödel's incompleteness theorem]] [[Tarski–Seidenberg theorem|does not apply]]. [[Decidability of first-order theories of the real numbers|Complications]] arise when adding further function symbols (e.g., exponentiation).

==Second order arithmetic==
{{Main|Second-order arithmetic}}

'''[[Second-order arithmetic]]''' can refer to a first-order theory (in spite of the name) with two types of variables, thought of as varying over integers and subsets of the integers. (There is also a theory of arithmetic in second order logic that is called second order arithmetic. It has only one model, unlike the corresponding theory in first-order logic, which is incomplete.) The signature will typically be the signature 0, ''S'', +, &times; of arithmetic, together with a membership relation &isin; between integers and subsets (though there are numerous minor variations).  The axioms are those of [[Robinson arithmetic]], together with axiom schemes of [[Mathematical induction|induction]] and [[Axiom schema of specification|comprehension]].

There are  many different subtheories of second order arithmetic that differ in which formulas are allowed in the induction and comprehension schemes. 
In order of increasing strength, five of the most common  systems
are 
*<math>\mathsf{RCA}_0</math>, Recursive Comprehension
*<math>\mathsf{WKL}_0</math>, Weak Kőnig's lemma
*<math>\mathsf{ACA}_0</math>, Arithmetical comprehension
*<math>\mathsf{ATR}_0</math>, Arithmetical Transfinite Recursion
*<math>\Pi^1_1\mbox{-}\mathsf{CA}_0</math>, <math>\Pi^1_1</math> comprehension
These are defined in detail in the articles on [[second order arithmetic]] and [[reverse mathematics]].

==Set theories==
The usual signature of set theory has one binary relation ∈, no constants, and no functions. Some of the theories below are "class theories" which have two sorts of object, sets and classes. There are three common ways of handling this in first-order logic:
#Use first-order logic with two types.
#Use ordinary first-order logic, but add a new unary predicate "Set", where "Set(''t'')" means informally "''t'' is a set".
#Use ordinary first-order logic, and instead of adding a new predicate to the language, treat "Set(''t'')" as an abbreviation for "∃''y'' ''t''∈''y''"

Some first-order set theories include:
*Weak theories lacking [[powerset]]s:
**[[General set theory|S']]  (Tarski, Mostowski, and Robinson, 1953); (finitely axiomatizable)
**[[Kripke–Platek set theory]]; KP;
**[[Pocket set theory]]
**[[General set theory]], GST
**[[Constructive set theory]], CZF
*[[Mac Lane set theory]] and  [[Elementary topos theory]]
*[[Zermelo set theory]]; Z
*[[Zermelo–Fraenkel set theory]]; ZF, ZFC;
*[[Von Neumann–Bernays–Gödel set theory]]; NBG; (finitely axiomatizable)
*[[Ackermann set theory]];
*[[Scott–Potter set theory]]
*[[New Foundations]]; NF (finitely axiomatizable)
*[[Positive set theory]]
*[[Morse–Kelley set theory]]; MK;
*[[Tarski–Grothendieck set theory]]; TG;

Some extra first-order axioms that can be added to one of these (usually ZF) include:
*[[Axiom of choice]], [[axiom of dependent choice]]
*[[Generalized continuum hypothesis]]
*[[Martin's axiom]] (usually together with the negation of the continuum hypothesis), [[Martin's maximum]]
*[[diamondsuit|◊]] and [[clubsuit|♣]]
*[[Axiom of constructibility]] (V=L)
*[[Proper forcing axiom]]
*[[Analytic determinacy]], [[projective determinacy]], [[Axiom of determinacy]]
*Many [[list of large cardinal properties|large cardinal axioms]]

==See also==
{{Portal|Mathematics}}

* {{annotated link|Glossary of areas of mathematics}}
* {{annotated link|List of mathematical theories}}

==References==
{{reflist}}

==Further reading==

* {{ citation | last=Chang | first=C.C. | author2-link=Howard Jerome Keisler|last2=Keisler|first2= H. Jerome | publisher=[[Elsevier]] | title=Model Theory | year=1989 | edition=3| isbn=0-7204-0692-7 }}
* {{ citation | last=Hodges | first=Wilfrid | authorlink=Wilfrid Hodges | publisher=[[Cambridge University Press]] | title=A shorter model theory | year=1997 | isbn=0-521-58713-1 }}
* {{ citation | last=Marker | first=David | title= Model Theory: An Introduction | publisher=Springer | year=2002 | isbn=0-387-98760-6| series=[[Graduate Texts in Mathematics]]|volume= 217}}

{{Mathematical logic}}

[[Category:Model theory|First-order theories, List of]]
[[Category:Mathematical logic|First-order theories, List of]]
[[Category:Mathematics-related lists|First-order theories]]