# Complete mathematics

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.

• Propositional logic. Jul 10 '10 at 5:54
• That means no natural numbers? 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". Jul 10 '10 at 12:04

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
• (The algebraically closed field example also works for characteristic 0.) 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. Jul 10 '10 at 16:39
• Hi! Great answer :) Is effective axiomatization equivalent to countable axiomatization? Jul 11 '10 at 6:30
• 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. 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. Jun 6 '11 at 22:46

http://en.wikipedia.org/wiki/Real_closed_field

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.

• The theory of elementary plane geometry is decidable. This goes back to Tarski. It is really the same as this "real closed field" material. 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. 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.

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.

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.

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