Why is predicate logic semidecidable?

Question

Could someone explain clearly why predicate logic is said to be "semidecidable"? I know that the set of invalid formulas of a predicate language is not effectively numerable, which implies that predicate logic is not decidable (a set of expressions is decidable iff both it and its relative complement - in this case the set of invalid formulas - are effectively numerable). Instead, the set of valid formulas of a predicate language is effectively numerable. Does "semidecidable" simply means that the set of valid formulas of predicate logic is effectively numerable?

A further question: which are the main "reasons" for the undecidability of predicate logic?

Thanks a lot for your help.

Fish

Answer 1

It is said to be semi-decidable because while it is not (fully) decidable, there is an algorithm that correctly classifies all the valid first-order logic statement as valid ... but this algorithm will go into an infinite loop when presented with certain invalid statements. And yes, this is the same as saying that the set of valid formulas of predicate logic is effectively numerable.

The fact that there is such an algorithm is closely related to the completeness of first-order logic, first proved by Kurt Godel in 1929.

One way to see that first-order logic is undecidable (meaning that there is no algorithm that correctly classifies all valid first-order logic statement as valid and correctly classifies all invalid first-order logic statement as invalid) is by looking at Alan Turing's work, and in particular the Halting problem:

It turns out that you can describe any halting machine and its behavior using first-order logic. Therefore, if first-order logic is decidable, we can solve the halting problem: For any machine M and input I we can describe using first-order logic that machine and input (using a big-ass, but still finite statement $S_{M,I}$), and we can also create a statement $H$ of what it would mean for that machine to halt. We then use the First-order logic decision procedure to decide whether $S_{M,I} \rightarrow H$ is valid or not: if it is valid, then the machine M with input I halts, and if it is invalid, then it does not halt. But since we know the Halting problem is unsolvable, the decision problem for first-order logic (what David Hilbert called the Entscheidungsproblem) is likewise unsolvable.

As to the 'cause' of all this ... one issue is of course that to see whether a first-order logic formula is valid is to see whether it is true in all possible interpretations ... but there infinitely many interpretations. That is not a proof (and indeed there are many times we handle infinities just fine), but if there were only finitely many interpretations, then it would be decidable just fine, so this can be seen as a 'cause' of sorts.

Answer 2

Yes, it just means that the set of valid formulas of predicate logic are effectively enumerable. The algorithm is simple: search through all possible sequences of sentences, and check each one to see if it is a proof using the standard deductive steps; if so, enumerate the conclusion of the proof into your set.

It's hard to say what the "cause" is - mathematical phenomena have proofs, not causes. But the key reason for the undecidability is that predicate logic is too powerful; it's powerful enough to describe the algorithm you might try to use, so it can circumvent it.

Answer 3

Does "semidecidable" simply means that the set of valid formulas of predicate logic is effectively numerable?

Yes, "semidecidable," "effectively numerable," "recursively enumerable," and "computably enumerable" are all synonyms.

Now, as to the phrase "predicate logic is semidecidable": usually when we refer to a logic as being semidecidable, what we mean is that the inference problem - "does $p\vdash q$?" - is semidecidable (the set of pairs $(p, q)$ such that $p\vdash q$ is semidecidable). For strong enough logics, though, $p\vdash q$ iff $\vdash p\implies q$, so the logic is semidecidable iff the set of validities is. (For an example where this is not true, take e.g. a logic that doesn't even have a symbol for implication - like equational logic, which might sound artificially weak but is actually in certain ways the "right" logic for universal algebra.)