Philosophy Stack Exchange is a question and answer site for those interested in logical reasoning. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Why doesn't completeness imply decidability for first order logic?

First order logic is complete, which means (I think) given a set of sentences A and a sentence B, then either B or ~B can be arrived at through the rules of inference being applied to A. If B is arrived at, then A implies B in every interpretation. If ~B is arrived at, then A implies ~B in every interpretation.

First order logic is undecidable, which means (again, I think) that given a set of sentences A and a sentence B, there is no procedure for determining whether A implies B (i.e. it's not the case that A are true and B is false) in all interpretations.

Why doesn't this work: Enumerate all strings x. If x encodes the valid derivation of B from A, accept. If x encodes the valid derivation of ~B from A, reject.

Because of completeness, eventually this process will stumble across an x which is either a proof of B or ~B from A. If B, then A implies B in all interpretations. If ~B, then it is not the case that A implies B in all interpretations. So FOL is decidable. But it's not, so I must have the wrong definition of either completeness or decidability.

share|improve this question
For some reason, I think that "It is not the case that B can be derived from A" implies "~B can be derived from A." I think that's where I'm misunderstanding completeness. That's clearly not true, because when A is {R(x)} and B is S(x), there there exists an interpretation in which A are true and B is false, and in which A are true and B is true. So neither B or ~B can be proven from A. – Taylor Hornby Aug 28 '14 at 15:26
So, is this a better understanding? There's a procedure that will tell us, supposing either (1) B is implied by A in every interpretation or (2) ~B is implied by A in every interpretation, which of (1) or (2) is the case, but in the case where neither (1) or (2) or true, there is no procedure for deciding if B is true in a specific interpretation. – Taylor Hornby Aug 28 '14 at 15:41
This is not an issue of philosophy but of mathematics. Therefore, this should be on Computer Science (because computability is part of CS) or maybe Mathematics. – Raphael Apr 1 '15 at 11:48

NO, completeness of first-order logic does not imply decidability.

You are mixing two use of completeness.

The first use regards the completeness of "standard" proof systems for first-order logic.

This is Gödel's Completeness Theorem, that says :

The completeness theorem says that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula.

Gödel's completeness theorem says that a deductive system of first-order predicate calculus is "complete" in the sense that no additional inference rules are required to prove all the logically valid formulas. A converse to completeness is soundness, the fact that only logically valid formulas are provable in the deductive system. Together with soundness (whose verification is easy), this theorem implies that a formula is logically valid if and only if it is the conclusion of a formal deduction.

It is easily generalized to the relation of logical consequence between a set Γ of first-order formulas and a formula φ, in symbols :

Γ ⊨ φ.

In this case we have that :

Γ ⊨ φ iff Γ ⊢ φ (i.e. φ is provable from Γ).

For simplicity, we will consider the case when Γ is the emptyset; in this case we have the previous version :

⊨ φ (i.e. φ is valid) iff ⊢ φ (i.e. φ is provable).

Your fallacy regards the "basic property" of validity :

it is not true that if φ is not valid then ¬φ is valid.

Consider the formula :

∃x∃y ¬(x = y).

It means : "there are at least two thing x and y such that they are not equal". This formula is not true in a universe with only a single element. Thus, it is not valid (validity means : true in every universe).

Its negation is :

¬∃x∃y ¬(x = y)

which amounts to :

∀x∀y (x = y).

It means "all things are equal". Neither this formula is valid, because it is not true in a universe with more than one element.

Compare with propositional logic, where a valid formula is called a tautology (the negation of a tautology is called a contradiction : a formula which is always false).

In this case, we have a decision procedure : the truth-table algorithm (it is highly "inefficient", but it works ...).

Apply it to a formula A whatever : if in its column you have all "T", then the formula is a tautology.

Also in this case there is a completeness theorem : if A is a tautology, we can find a proof of it in the "usual" proof systems, like Natural Deduction.

But note that also in this case it is not true that, for a formula A whatever, A is a tautology or ¬A is.

The formula :

p V q

is neither a tautology nor a contradiction.

The second meaning of completeness regards theories, and is the key to the famous Gödel's incompleteness theorems which says that :

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system.

This (negative) result concerns another aspect of intuitive "completeness" (in the sense of adequacy) : for a mathematical theory, like arithmetic or set theory, it is a reasonable expectation that the axioms (formalized with first-order logic) are able to "capture" all the mathematical truth expressible in that theory.

For most of "little bit complex" mathematical theories, this is not possible.


Decidability is linked to the second meaning of completeness.

If a theory T is complete (in the second sense, plus a second "technical" condition : effectively axiomatized), i.e. T is able to prove all true sentences φ expressible in the language of the theory, due to the fact that either φ is true in T or ¬φ is true in T, then T is decidable.

[Note. If we consider the two formulae above, and we consider their meaning regarding the single arithmetical interpretation, now we have that one of them is true and the other is false. Due to the fact that there are infinite natural numbers (and so, more than one), we have that the formula : ∃x∃y ¬(x = y) is true in the arithmetical interpretation (consider e.g. 1 and 2), while its denial ∀x∀y (x = y) is obviously false (not all numbers are equal)].

Going back to decidability, why a complete theory is so ?

Exactly because the "procedure" described in your question works : start proving theorems in T. After a finite amount of time, if φ is true, you will find the proof of it; if it is not, then ¬φ is true and you will find a proof of it.

As said before, this "procedure" does not work for validity because it is not true that either a formula or its denial are valid.

Gödel's incompleteness theorem proves that formalized theories having enough "capability" for expressing arithmetical facts are not complete in the second sense : they are not able to "capture" all true arithmetical facts.

Thus the above theories are not decidable.

What is the "link" between the two uses of completeness ?

Consider a first-order theory T which include the language of arithmetic.

The "underlying" f-o logic is complete (first sense) : i.e. it is able to prove all logical consequences of the axioms of the theory T.

But the theory T is incomplete (according to Gödel's incompleteness theorem), i.e. there is a true arithmetical sentence φ not provable from the axioms of T.

So what ?

It is not a contradiction. Consider the def of logical consequence applied to T :

T ⊨ φ iff φ is true in every model of T.

Being φ true in the "intended model" of arithmetic (the "usual" numbers) we conclude that it is not true in some other model [see Francis Davey's comment]: there are non-standard model of arithmetic.

Being so, it is not a logical consequence of the axioms of T and this is the reason why its unprovability in T does not conflict with the completeness of the underlying logic.

share|improve this answer
Does it follow that a Gödel sentence is true in some interpretations, but false in others? – Theodore Norvell Aug 28 '14 at 21:15
Yes, that is exactly right. It demonstrates that there are non-standard models of arithmetic. – Francis Davey Aug 28 '14 at 21:48
Thanks, it's starting to make a lot more sense. I was confusing the two different completenesses. So, the first means: if a formula is valid (true in every interpretation), then it is provable. Decidability is about whether a formula is true in a specific interpretation, which is possible without it being valid. The second meaning of "completeness" is used in a claim within a specific (but arbitrary, therefore generalizable) set of axioms. – Taylor Hornby Aug 28 '14 at 23:23
Is it possible for a system to be complete by the first meaning, but have interpretations which are incomplete by the second meaning? Or am I comparing apples to oranges by asking that question? – Taylor Hornby Aug 28 '14 at 23:26
The second meaning of 'complete' (that there exist closed sentences that are not provable and whose negations are also not provable) applies to theories, not to interpretations. – Theodore Norvell Sep 2 '14 at 18:34

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.