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.
 A: 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.
A: 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

A: 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.
A: 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. 
A: 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.  
A: 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
