How is first-order logic complete but not decidable?

Question

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.

Answer 1

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.

---

Added

Decidability is linked to the second meaning of completeness.

If a theory T is complete in the second sense above, 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, and is effectively axiomatized, 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.

Answer 2

Since Taylor Hornby already self-corrected the definition of completeness (thanks to Mauro ALLEGRANZA's first definition), I just want to point out where exactly his reasoning goes astray.

Why doesn't completeness imply decidability for first order logic? Taylor Hornby reasons as follows:

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.

what is wrong here is the sentence:

Because of completeness, eventually this process will stumble across an x which is either a proof of B or ~B from A.

Completeness by definition means "If B is logically entailed, then B is provable." It is a conditional statement. Now, in general, we do not know whether a given B is logically entailed or not in advance. So we do not know whether there is a proof of B or not. So what really happens is this:

eventually this process will stumble across an x which is either a proof of B or ~B from A, OR this process will continue to run forever.

That is, this algorithm does not always determine whether B is logically entailed (or equivalently, whether B is provable, thanks to the properties of soundness and completeness of FOL). If either B or ~B is provable, we will eventually find its proof. But if neither B nor ~B is provable then we can never tell whether there is no proof or whether we just need to keep looking. So this algorithm does not give us an answer for every B, but we can ask whether there is a better algorithm that does give us an answer for every B. Turing's halting problem is used to show that there is no algorithm for determining whether B is logically entailed.

First-order logic is complete because all entailed statements are provable, but is undecidable because there is no algorithm for deciding whether a given sentence is or is not logically entailed.

Answer 3

There are ultimate limits to machines, no matter how cleverly they are designed. In 1936, Turing proved mathematically that a general algorithm to solve the problem for all possible program-input pairs cannot exist, ever. That is, no algorithm can be written such that it will always correctly decide, for any given program-input pair, whether the program will or will not halt. In computer science, this is called the halting problem. Turing proved that any algorithm can be made to contradict itself and therefore cannot decide correctly. As an illustration, we may make use of a “pathological” program-input pair designed to do the opposite of what the algorithm predicts it will do.

Turing’s proof implies that it is impossible to predict if the Turing machine programmed to attack certain mathematical problems will ever succeed and come to a halt, or keep on running forever. Actually, an equivalent ultimate limit applies to humans: It is also impossible to predict if mathematicians will ever succeed with regard to solving these same problems.

The crucial question concerns completeness and decidability (as to whether a theorem is either true or false, but not both), which is equivalent to the halting problem in computing science. Incompleteness opens the door to the possibility of undecidability. A successful proof of a particular problem implies that it is not undecidable in the theory (or system) where it is formulated. But such a proof does not imply that the theory itself is complete or decidable. There may be other problems in the theory that are undecidable, in which case no solution exists. In an incomplete theory, there are theorems or equations, for instance, that appears to intuitively true but are unprovable. Therefore, it is impossible to predict if a particular problem formulated in an incomplete theory can ever be solved. Never before in the history of human knowledge has an ultimate limit to predictability been stated with such clarity, with the help of logician-mathematicians in the 20th century.

Answer 4

I'm pretty sure this is correct, but not 100% confident:

One possible confusion is that we may think we are talking about a single model, when we're really talking about all possible models that satisfy a particular set of axioms. So if we are talking about one model, then P or NOT P is true, but if we are talking about multiple then P may be valid, NOT P may be valid or it may be mixed (here valid = always true).

Completeness means that if P is valid we'll prove it eventually and since NOT P is just another proposition, if it is valid same for that. However, this doesn't guarantee anything about the mixed propositions. We can never know that if we didn't just keep looking for longer that we wouldn't find a proof for P or for NOT P.

Or to clarify even more, the following two claims are different:

• "NOT P" is valid
• NOT "P is valid"

The later also includes P being mixed

Answer 5

First order logic is just algebra, in disguise, while higher order logic is analysis. Theories formulated in first order logic can be expressed as algebraic systems: a system which contains a set of operations, a set of distinguished objects, and a set of equational identities; while theories formulated in higher-order logic that are not equivalently expressible or reducible to first-order theories, may be rightly regarded as calculi.

For instance, an Abelian group can be expressed as an algebra containing a single operation ("-" for subtraction), a distinguished object ("0"), and the following identities: 0 - 0 = 0, x - (x - y) = y and x - (y - z) = z - (y - x).

Also, for instance, an Affine Geometry A over a specific field F can be expressed as a two-sorted algebra containing the ternary operators a,f,b ∈ A×F×A ↦ [a,f,b] ∈ A and a,b,c ∈ A×A×A ↦ abc ∈ A that embodies the operations [a,f,b] = (1 - f)a + fb and abc = a - b + c. An example of axioms (suitable, except for the two fields F = GF(2) of size 2 and F = GF(3) of size 3) is: [a,0,b] = a, [a,1,b] = b, [a,rt(1-t),[b,s,c]] = [[a,rt(1-s),b],t,[a,rs(1-t),c]], abc = [[b,1/(1-t),a],t,[b,1/t,c]], where t is arbitrarily chosen as any member of the field F other than 0 or 1.

For algebraic theories, the "free algebra" is the one which contains just the distinguished objects and whatever other objects can be made from them using the algebra's operations. One can also talk about the "free algebra generated from a set X", where the members of the set X are added to the list of distinguished objects. For instance, the subtraction algebra, above, freely generated from the set {1} is one and the same as the algebra of integer subtraction, and contains also the algebra of integer addition by way of the definitions, -x = (x - x) - x, and x + y = x - (-y). (One can prove x - x = 0 using the axioms, namely by: x = 0 - (0 - x) = x - (0 - 0) = x - 0, and x - x = x - (x - 0) = 0, so -x = 0 - x is an equivalent definition, but less self-contained.)

So, first-order theories can always be realized by models, which makes first order logic complete. This is more precisely stated in the abstract, excerpted below, to "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), January 1984 https://www.researchgate.net/publication/38355700_First-order_theories_as_many-sorted_algebras)

Completeness ensures that a proof for any valid statement can be found by a finite search. Failure to find a proof, when a statement is invalid, occurs only after the unending search through all possible proofs never ends. So, you would have to wait for forever to never end, first, before seeing a "no" answer to the query "is it valid?". In order to be decidable, the "no" answer has to be forthcoming some time before forever is never finished happening.

The key excerpt from the abstract:

"In this paper, by developing the study of first-order logic through many-sorted algebras, we show that every first-order theory is a particular algebra verifying axioms in equational form (see Section 2); therefore we are able to apply Birkhoff's theorems concerning the varieties (see Section 1 [and two references contained in the paper]) and to obtain the Henkin models algebraically, whence the completeness theorem of first-order logic (see Section 3)."

Punchline: "Many-sorted" is the key-phrase - so, add in a boolean type and remake predicates as boolean-valued operators.