Semi-decidability of First Order Logic

Question

I studied the concepts of decidability, semi-decidability and undecidability. I know the practical consequences of semi-decidability of first order logic. What i dont understand are the profound reasons for which the First Order Logic is semi-decidable. That is , why can i verify the validity of a theorem in a finite number of steps, but if the formula is not a theorem the procedure proceed to infinity ? I searched a lot in this website and i found great answers to my question ( like here), but they seem too superficial to me...

Answer 1

First of all, it is not true that if some FOL statement is not a theorem then whatever method you are using (that is sound and complete in figuring out that statements are theorems) will always proceed indefinitely: for some statements the procedure may stop without having determined that the statement is a theorem and you'll then know it is not a theorem.

However, it is true that such a procedure will indeed proceed indefinitely for some invalid FOL statements.

OK, but why is that?

Well, first let's look at some actual method and show that indeed they sometimes go into infinite loops. For example, take a look at this website that uses the truth tree method to try and figure out validity:

https://www.umsu.de/logik/trees/

It has some examples valid statements you can click on and it will show the truth tree that demonstrates it (like resolution, it works like a proof by contradiction: it tries to derive a contradiction from the negation of the statement)

OK, so now let's see an example of an invalid statement that it figures out does not lead to a contradiction. So, just enter this:

\forallxFx

(this is $\forall x Fx$)

You'll see that it quickly finds a counterexample to this statement.

OK, but now enter:

\neg(\forallx\forally\forallz((Rxy\landRyz)\toRxz)\land\forallx\negRxx\land\forallx\existsyRxy)

You'll see that it just keeps going and going and going ....

Why is that? Well, the statement is the negation of:

$$\forall x\forall y\forall z((Rxy\land Ryz)\to Rxz)\land \forall x\neg Rxx\land\forall x\exists y Rxy$$

which says that $R$ is a partial order (it's transitive and irreflexive), and that there is always a 'larger' element. Now, if you think about that, note that for any finite sized domain, there will not always be a larger element, as you go 'up' the order. So, we cannot satisfy this statement using a finite sized domain, which means that there is no finite sized counterexample to the statement we just fed into the truth tree checker. Hence, any counterexample to that statement will have to be of infinite size, and there clearly are such counterexamples: just take the numbers as the domain and interpret $R$ as $<$. So, while the statement we just fed this checker is not valid, this checker (and pretty much any existing systematic method) will forever be trying to find a counterexample, as it is simply adding one object to the domain at a time, and thus never reaches an infinite domain.

OK, so that's part of the answer: sometimes you need infinite sized counterexamples to show that some statement is not valid.

OK, fine, but why can't there be a method that can find infinite sized counterexamples? After all, we humans can. And, in fact, you can define techniques that can detect this. You could, as an extreme example, have a method that detects exactly this specific combination of sentences that I just provided. But, we know that there cannot be a general method that covers all cases.

OK, but again, you ask, why exactly is that? Well, maybe this helps: First of all, if we can solve the halting problem, then we could detect that our procedure that is sound and complete for validity would go into an infinite loop for some input statement, and since that can only happen for invalid statements, we would then have our answer: the statement is invalid. Indeed, as such we have that:

If we can solve the Halting Problem, then FOL is decidable

But, as I am sure you well know, we can't solve the Halting problem. Now, that of course still doesn't mean that we cannot solve the general decision procedure (if you think it does, you're making the fallacy of denying the antecedent: $P \rightarrow Q$, $\neg P$, therefore $\neg Q$ would be the fallacy), but once again it does point to another piece of the puzzle: the undecidability of FOL has something to do with the unsolvability of the Halting problem.

In fact, we can make the link between the halting problem and FOL even stronger: it turns out that we can describe the behavior of machines in terms of FOL sentences, and thereby reduce the halting problem to a problem in FOL. In fact, as such, we can show the converse of the previous statement as well:

If FOL is decidable, then we can solve the Halting problem.

And, now we can of course do a simple Modus Tollens: we cannot solve the Halting problem, and therefore we cannot decide FOL.

Finally, from this, it follows that it has to be true that procedures that are sound and complete as far as FOL validity goes, go into an infinite loop for at least some invalid sentences. And that is because if these procedures do always halt for any FOL problem, and if it does not end up saying that the statement is valid, then that must mean the statement is invalid, and we would have a full decision procedure after all... which we know cannot exist (well, assuming the Church-Turing thesis).

Hope that helps ...