MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Hello, I would like to ask you if there is a mathematical theory, that is complete (in the sense of Goedel's theorem) but practically applicable. I know about Robinson arithmetic that is very limited but incomplete already. So, I would like to know if there is some mathematics that could be practically used (expressiveness) and reduced to logics (completeness).

I'm very new to the site and to the maths as well, so please tell me if that's a silly question.

share|cite|improve this question
Propositional logic. – Mikola Jul 10 '10 at 5:54
That means no natural numbers? – Bubba88 Jul 10 '10 at 5:59
@Mikola: Propositional logic (with no non-logical axioms) is not a complete theory. For example, it neither proves nor disproves the propositional sentence "A". – Carl Mummert Jul 10 '10 at 12:04
up vote 28 down vote accepted

You probably intended to restrict the question to effectively axiomatizable theories. Otherwise, for example, the first-order theory of the standard model of arithmetic is a complete theory, as is the theory of the standard model of ZFC.

Gödel's incompleteness theorem establishes some limitations on which effective theories can be complete. It shows that no effective, complete, consistent theory can interpret even weak theories of arithmetic such as Robinson arithmetic. However, there are many mathematically interesting theories that do not interpret the natural numbers.

Examples of complete, consistent, effectively axiomatizable theories include:

  • For any prime $p$, the theory of algebraically closed fields of characteristic $p$
  • The theory of real closed ordered fields, mentioned by Ricky Demer
  • The theory of dense linear orderings without endpoints
  • Many axiomatizations of Euclidean geometry
share|cite|improve this answer
(The algebraically closed field example also works for characteristic 0.) – François G. Dorais Jul 10 '10 at 13:29
Other important basic examples of complete decidable theories are the theory of the integers as an additive ordered group and the theory of the $p$-adic numbers as a valued field. – Dave Marker Jul 10 '10 at 16:39
Thanks for the additions. – Carl Mummert Jul 10 '10 at 22:18
They're not the same. A theory is effectively axiomatizable if the theory is generated by some computable set of axioms. A stronger condition, mentioned by Dave Marker, is decidability: there is a computable function that correctly determines whether an arbitrary formula is a logical consequence of the axioms. – Carl Mummert Jul 11 '10 at 11:00
@Bubba88: The standard model of ZFC has a countable set of axioms. There's only a countable set of possible sentences. But, it is definitely not effectively axiomatizable. – George Lowther Jun 6 '11 at 22:46

The real closed field axioms can directly answer the question of whether a polynomial with algebraic coefficients has a zero in an interval with algebraic endpoints, and classify for what coefficients and endpoints the polynomial has a zero in the interval.

It can interpret geometry and the complex field, and, for any particular k, the vector spaces R^k and C^k with matrices operating on them.

share|cite|improve this answer
Thank you, that's really great. – Bubba88 Jul 10 '10 at 6:35
The theory of elementary plane geometry is decidable. This goes back to Tarski. It is really the same as this "real closed field" material. – Gerald Edgar Nov 24 '10 at 15:26
I recall reading somewhere that the completeness and/or decidability of the theory of real closed fields, through its intimate connections with Geometry, has found applications in the area of Computer Vision. Hopefully someone in the know can shed light on this. – Ali Enayat Jun 7 '11 at 2:22

Presberger arithmetic is used in practice for software verification, e.g. to prove that a program fragment is free of array subscript overflows. Basically the program has expressions like a[3*i+k] and you want to prove that the subscript never greater than the array size. If you have something like a[m*n+k] the multiplication of two variables m and n can only be expressed in Peano arithmetic, which is undecidable, but it's often possible to write programs without such multiplications of variables in subscripts. (Multiplication by constants can be expressed by repeated addition, of course). Wikipedia's article on Presburger arithmetic has some info of that.

Also, compilers of fancy programming languages rely on decidability of even weaker theories to handle type inference and type equality. Similarly for model checking in hardware design, etc. This stuff is becoming more and more important in the real world, and not that many programmers and engineers know much about it. I think this is a good time to be a logician even if you can't get a job in academia.

share|cite|improve this answer
Good info, thanks :) – Bubba88 Jan 12 '11 at 7:09

Perhaps it is worth adding some comments to the list of non-trivial complete theories given by Carl Mummert. One remark is that the completeneness of Euclidean geometry is a consequence of that of the real closed ordered fields (exploiting the possibility to "arithmetize" geometry using cartesian coordinates). The other is that the completeness of the theory of dense linear orderings without endpoints is only one in a set consisting of related theories. Actually, all the 4 possible theories of dense linear orderings, that is, those without endpoints, having both first and last elements, having only first, and having only last element are complete. Analogously all the 4 possible theories of discrete linear orderings (with the additional requirement of infiniteness in the case of having both first and last elements) are also complete. Moreover, there is a nice analogy between linear orderings and Boolen algebras (BA's) in this respect: atomless BA's correspond to dense orderings, atomic BA's to discrete orderings. Indeed, both the theory of atomless BA's and the infinite atomic ones are complete.

share|cite|improve this answer

This answer is possibly unhelpful and definitely under-informed, but a good source to look into might be the book Complete Theories by Abraham Robinson. I haven't read it, I just happened to see it as I was perusing the mathematics section in my library. If you have done any research, you may have come across this book. If not, it would be worth checking out.

share|cite|improve this answer

Not exactly complete in the sense of Goedel, but more in the sense of Garrett Birkhoff (yes, I am talking about equational logic, where the theories considered are often, but not always, universally quantified equations such as associativity and distributivity). Term rewriting systems occur in computer science and occasionally work with complete equational theories. While not as expressive as logics with relation predicates other than equality, equational theories are complete in equational logic, sometimes are recursive, sometimes have a finite set of equations which (along with the rules for equational logic) generate all the other equations belonging to a theory, and have nice classes of models (cf Birkhoff's HSP Theorem).

Gerhard "Likes To Study Inequalities Too" Paseman, 2011.06.06

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.