Mechanization of Mathematics

Question

Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false.

By the completeness theorem of first-order logic, a statement is universally valid if and only if it can be deduced from the axioms, so the Entscheidungsproblem can also be viewed as asking for an algorithm to decide whether a given statement is provable from the axioms using the rules of logic.

From Wikipedia.

But In my AI course, we learned of an algorithm to prove or disprove new statements using the axioms known as Resolution by refutation. Simply take the a negation of the statement you want to prove, and use the axioms to show it either leads to an empty clause (true) or non-empty clause (false).

So my question is: What am I missing from these two seemingly contradictory statements? On one hand the literature states there exists no algorithm to determine if a statement is provable from the axioms, and on the other hand, I am presented with an algorithm that proves (or disproves) a statement from the axioms. What am I confused or incorrect about here?

Answer 1

You're missing what resolution refutation works for -- namely, just propositional logic.

For example, try using that algorithm on "There exist integers x, y, z such that ​x³ + y³ + z³ ​= ​33."

There are sets of axioms for which the set of theorems is decidable -- the real closed field axioms are the most important example of that, and they in fact also allow quantifier elimination.

There are sets of axioms for which the set of theorems is not decidable -- by undecidability of Diophantine equations, all Σ₁-sound extensions of Robinson arithmetic are examples of that.