Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
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?
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.
