# 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. –  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

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.) –  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
show 1 more comment

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.

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

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

-