I am relatively new to logic, so forgive my ignorance. My question is: Are there any formal systems that are deemed complete? If so, how did we prove they were complete and which are they?
-
3"Complete" in what sense? There are certainly first-order theories which are complete (e.g. the theory of dense linear orders without endpoints), but these are not capable of encoding "mathematics" wide and large. – user642796 Sep 27 '13 at 04:22
1 Answers
Inconsistent theories are trivially complete, so I'm going to assume that you're looking for systems that are both consistent and complete.
One such system is Presburger Arithmetic (PreA), which resembles the usual Peano Arithmetic, but has no multiplication.
A common technique for showing completeness is quantifier elimination: a theory admits quantifier elimination if every quantified formula corresponds to a logically equivalent quantifier-free formula.
Strictly speaking, PreA does not admit quantifier elimination, but a finite extension does: the resulting procedure is Cooper's algorithm.
Quantifier elimination, by itself, does not mean that your theory is complete: you also need to show that all quantifier-free statements are either provable or refutable. In the case of PreA and its extension, this follows by a simple structural induction.