# Can syntactically complete theories be undecidable?

A formal system S is syntactically complete if for each sentence (closed formula) φ of the language of the system either φ or ¬φ is a theorem of S.

My confusion is the following. I've heard that a syntactically complete theory is decidable if it is "axiomizable." But if the system can prove either φ or ¬φ for each φ, doesn't it already imply that it is "axiomizable?" So how could a syntactically complete theory be undecidable?

• Every syntactically complete recursively axiomatizable theory is decidable. Syntactic completeness does not imply recursive axiomatizability, so syntactically complete theories can be undecidable. Sep 22 at 17:20
• @MauroALLEGRANZA You seem to be assuming that the theory in question is axiomatizable (= recursively axiomatizable); if it's not, your initial comment is false. Sep 22 at 18:37
• The phrase syntactically complete is awfully misleading (I suspect it's spread by Wikipedia), the proper one is deductively complete. Syntax specifies how to build well-formed formulas and does not dictate how to derive proofs. Literally syntactically complete signifies that the syntax of a language is capable of inscribing any wff whatsoever of the language. Sep 22 at 21:21
• @TankutBeygu I'm inclined to agree that deductive completeness is a better term, though syntactical completeness is fairly widely used: I found it in the Handbook of Mathematical Logic, for example. I would guess it is popular because of the contrast with the semantic completeness of proof systems. Sep 22 at 22:06
• As an example, "true arithmetic", where every true statement of arithmetic is an axiom, is (trivially) syntactically/deductively complete but undecidable by Gödel's theorem. It is not recursively axiomatizable for the same reason. Sep 22 at 22:58

Short version:

A theory that is syntactically complete may be undecidable. However, a theory that is syntactically complete and recursively axiomatisable is always decidable.

Stated rather colloquially, to say a theory is syntactically complete means the theory knows whether A or ¬A is the case. To say a theory is decidable means we know whether A or ¬A is the case, because we have an algorithm for computing it. The two need not coincide. (To make matters more complex, there are actually degrees of algorithmic solvability.)

Long version:

It is worth noting for clarification that the term 'decidable' has changed in usage over the last 100 years. When Gödel wrote his famous paper "On Formally Undecidable Propositions of Principia Mathematica" it was common to use 'undecidable' to mean a statement such that neither it nor its negation can be proved in a given theory. Today we prefer to say that such a statement is independent of a theory and hence the theory is syntactically incomplete.

Nowadays, decidable is used to describe a problem such that there exists an effective procedure or algorithm that is guaranteed to solve the problem and terminate. In this sense, undecidability should not be confused with incompleteness. A system of logic is decidable if there is an effective procedure that determines for any arbitrary formula of the language whether or not the formula is a theorem. A theory is decidable if there is an effective procedure that determines for any arbitrary sentence whether or not it is a member of the theory. A set of natural numbers is decidable if there is an effective procedure that determines whether or not any given number is a member of the set. By the Church-Turing thesis, a problem is decidable if and only if it is computable or recursive, so decidable, computable and recursive are often used interchangeably.

Sometimes we have an effective procedure such that if there is a solution to a problem the procedure is guaranteed to find it and terminate, but if there is no solution, the procedure may just continue forever. In which case, while the procedure is running, we don't know whether there is some solution that hasn't been found yet, or there is no solution. In this case, a problem is said to be semidecidable, or computably enumerable, or recursively enumerable.

A theory is axiomatisable if there exists at least one subset, an axiom set, such that all of the theorems of the theory are provable from that set. A theory is said to be recursively axiomatisable if there is a recursive axiom set, and finitely axiomatisable if there is a finite axiom set. Since trivially any theory axiomatises itself, the term 'axiomatisable' is often used in practice to mean recursively axiomatisable. By this definition, not all theories are axiomatisable.

If we have a syntactically complete and axiomatisable theory, then for all sentences A, ¬A one or other is a theorem and the axiom set proves that one (and not both, provided the theory is consistent). We can use the axiom set to construct derivations of A and ¬A and since derivations are finite, we will be able to find a proof of A or a proof of ¬A after a finite number of steps. Hence we have decidability.

But if we have a syntactically complete and unaxiomatisable theory, there is no way to construct derivations that is guaranteed to terminate. We can enumerate theorems, but for any specific A or ¬A, an attempt to find a proof may proceed interminably.

• Thank you! So how can we know if a theory knows whether A or ¬A is the case, hence syntactically complete? Did we just assume in the past trivially via law of exclude middle that one of the two must be the case, and only via Godel's incompleteness theorem figure out some theories cannot be syntactically complete? Or is there more to it than that required to know if a theory, for example, True Arithmetic, is syntactically complete? Sep 22 at 21:04
• It would not be safe just to assume that A or ¬A is provable. It has to be proved in each case. A fairly general approach to proving it might be: Devise some canonical form for the sentences in the language of the theory. Demonstrate that the axioms prove or disprove any sentence in this canonical form. Then prove that any sentence is logically equivalent to some canonical form of it. Sep 22 at 21:35