Can we prove any statement in the first order logic operating only in the space of prenex normal forms?

Question

Let's assume that we have a set of statements written in first order logic (axioms and maybe some proven theorems). Now we want to prove that a given "new" statement is true.

My naive approach to the prove would be like follows:

1. Take all statements that are used as inputs (axioms and proven theorems) and connect them with and (conjunction) so that we get just one large statement (sentence in FOL).
2. Bring this "large" statement to a prenex normal form using simple deterministic rules (for example as explained here).
3. Similarly, bring the statement that you want to prove to the prenex normal form as well.

Now, use formulas like:

$\forall x. P(x) \implies \exists x . P(x)$

to show that the "output" expression (written in the prenex normal form) follows from the "input" expression (also written in the prenex normal form). In other words, we will use only transformations that preserve the prenex normal form. So, all our derivations will be in the space of the prenex normal form.

So, now my questions is if such an approach would work. I guess that it is not the case, because it would be too simple. So, the second part of the question is: Why this approach would not work? Where can if fail?

Answer 1

That's a famous problem, called the Entscheidungsproblem. "is first order logic decidable?", that is: if we're given a sentence is there an effective method for determining whether or not it is valid?

Turing and Church proved (the first with his machines the second with lambda calculus) that it is not the case.

---

Roughly:

By the Church-Turing thesis every computable function is Turing-computable. Also consider the Halting Problem: the function $h(e,w)$ that halts with output $1$ if the Turing-machine described by $e$ halts on input $w$ and outputs $0$ otherwise, is not Turing-computable.

The strategy is to reduce the decision problem to the Halting problem.

So we create two Turing-machines: For every input $w$ and a Turing Machine $M$; one sentence is $\tau (M,w)$ which represents the instructions of $M$ and the input $w$ another sentence is $\alpha (M,w)$ expressing "M eventually halts" such that: $$\vDash \tau (M,w) \to \alpha (M,w) \;\; \text{iff} \;\; \text{M halts for input}\, w$$

Proving that reduces the decision problem to the halting problem, all that remains to do is to code first order logic into numbers so that Turing machines can operate on them.