If a theory is incomplete, does that mean there is a formula which is undecidable in that theory?

Question

If a theory is incomplete (meaning there exists a formula $A$ and $\neg A$ which neither of them is logically entailed from axioms of that theory), does that mean there exist a formula which is not decidable (meaning $A$ nor $\neg A$ is provable) from the axioms of that theory?

Or do I misunderstand the definition of a formula being undecidable from a set of axioms of a theory?

Answer 1

The confusion seems to arise from two different notions of "completeness" and what exactly decidability means, so let me start by clarifying the terminology:

Semantic soundness: For all $\Gamma, \phi$, if $\Gamma \vdash \phi$, then $\Gamma \vDash \phi$.

Soundness just means that the calculus doesn't prove nonsense: If there is a proof of $\phi$ from premises $\Gamma$, then the inference $\Gamma \vDash \phi$ is actually semantically valid.

Semantic completeness: For all $\Gamma, \phi$, if $\Gamma \vDash \phi$, then $\Gamma \vdash \phi$.

Semantic completeness means that every valid inference can be proven in the calculus. Note that this says nothing about the non-inferences.

Syntactic completeness: Given a set of axioms $\Gamma$, for all $\phi$, $\Gamma \vdash \phi$ or $\Gamma \vdash \neg \phi$.

Syntactic completeness means that for any formula $\phi$, either the formula itself or its negation can be proven from the axioms $\Gamma$. A formula of which this does not hold is said to be independent of the theory. I think that syntactic incompleteness is what you mean by (incorrectly) saying "undecidability".

Semi-decidablity: A theory $T$ is semi-decidable iff there is an algorithm that for every suitable input $\phi$ terminates with "yes" if $\phi$ is a theorem of the theory, and returns "no" or gives no answer if it is not.

Semi-decidability of logical inference only requires that all the inferences that are valid are detected; invalid ones may or may not be recognized as such (e.g., the algorithm may run into an infinite loop on some of the invalid sequents without ever yielding an answer). It may be that the algorithm fails to give an answer on none, some or all of the invalid inputs; in any case, all the valid inferences have to be detected.

Co-semi-decidability: A theory $T$ is co-semi-decidable iff its complement $\overline{T}$ is semi-decidable.

Co-semi-decidability of inference means that the formulas which are not theorems are detected as such; inferences which do hold may or may not be recognized by the algorithm.

Decidability: A theory $T$ is decidable iff $T$ is semi-decidable and co-semi-decidable. Otherwise $T$ is undecdiable.

Decidability of logical inference requires that all the theorems and all the non-theorems are recognized after finite time.
A theory is called undecidable as soon as one of the requirements fails; it may still be that $T$ is semi-decidable, or that its complement is, but at least the algorithm won't terminate on all the inputs. Of course, a theory is also undecidable if neither its theorems nor its non-theorems will always be recognized.

The calculus of semantic trees on FOL is

• semantically sound: If there is a closed tree for an inference, then it is indeed semantically valid: $\Gamma \vdash \phi\ \Longrightarrow\ \! \Gamma \vDash \phi$.
• semantically complete: If an inference is semantically valid, there is a closed tree: $\Gamma \vDash \phi\ \Longrightarrow\ \!\Gamma \vdash \phi$. The tree procedure will terminate on any input that is among the valid inferences.
• syntactically incomplete: Not for all formluas $\phi$ the tree procedure will either close on $\phi$ or on $\neg \phi$; there are formulas for which both trees will remain open given an empty or non-empty set of premises $\Gamma$. Syntactic completeness is a different kind of completeness than semantic completeness and is a stronger requirement: If the calculus were syntactically complete, then, asuming that it is is also sound, this would imply that every formula is either tautological (= i.e. true in all structures) or contradictory (= i.e. false in all structures) in that theory. This holds neither of classical propositional nor predicate logic: There are formulas which are contingent, i.e. neither the formula nor its negation are universally valid. For example, any atomic formula $P$ is contingent: There are some structures in which it is true, and others in which is it false. And given that the calculus is semantically sound, then for these neither valid nor invalid formulas, neither the formula nor its negation should be provable (= have a closed truth tree).
  Coming back to your original question, if a theory $\Gamma$ is incomplete (i.e. for some formulas $\phi$, neither $\Gamma \vDash \phi$ nor $\Gamma \vDash \neg \phi$), then if the calculus is sound w.r.t. the theory, yes, it will be syntactically incomplete (i.e. for some formulas $\phi$, neither $\Gamma \vdash \phi$ nor $\Gamma \vdash \neg \phi$). However, this is not the same as undecidability.
• semi-decidable: If an inference is valid, then the tree procedure will always close in finite time, thereby showing that the formula follows from the axioms.
• not co-semi-decidable: For FOL, there are invalid inferences on which the tree procedure runs into infinite loops, thereby never yielding an answer as to whether or not the formula follows from the axioms. (Note that for propositional logic, the semantic tree calculs is also co-semi-decidable: It will also terminate on all the invalid inferences.)
• undecidable: The semantic tree won't terminate on all inputs: It works on all valid theorems, but not on all non-theorems. (Again, this situation is different for statemement logic, which is decidable.)

The important point to realize is that neither syntactic incompleteness nor undecidability contradicts semantic completeness:

- That the proof system is not syntactically complete just means (in combination with soundness) that not all formulas are either universally valid or contradictory in the theory. It is still the case that all those formulas which the axioms do semantically entail are provable ($\rightsquigarrow$ semantic completeness).
- That FOL inference is undecidable just means that the sequents which are not valid are not always recognized as such by the proof system. Again, it is still the case that all those formulas which do follow from the axioms are provable ($\rightsquigarrow$ semantic completeness).