Understanding the Entscheidungsproblem

Question

As a part of my self learning about Logic and Computability Theory, I'm trying to fully understand the Entscheidungsproblem and its unsolvability. However, it seems to me that many online resources do a rather poor job introducing it clearly.

I'd like to ask about the exact formulation of the problem. wikipedia describes it as

finding an algorithm that considers, as input, a statement and answers "Yes" or "No" according to whether the statement is universally valid, i.e., valid in every structure satisfying the axioms.

" I'm assuming that "a statement" just means "a first-order sentence". But still, I don't understand what are "the axioms" reffered here. Should they also be an input for the algorithm? If so, this is quite limiting since we can only introduce a finite number of axioms. Or maybe the Entscheidungsproblem asks for such an algorithm *given a set of axioms, so we essentially have a different "Entscheidungsproblem" for each set of axioms.

An Introduction to Godel's Theorems by Peter Smith describes the problem as deciding whether a given first-order sentence is "a theorem of first-order logic". I've never come across such notion before; I know what a theorem of a first-order theory is, but what is a theorem of first-order logic itself? In what first-order language would that sentence be written?

Answer 1

See Entscheidungsproblem and the original 1928 formulation by Hlbert and Ackermann (§12. The Decision Problem):

determining whether or not a given formula of the predicate calculus is universally valid.

Due to Gödel Completeness Theorem, we have that a formula is universally valid iff it is provable in the calculus: $\vDash \varphi \text { iff } \vdash \varphi$.

Thus, the problem amounts to determining whether or not a given formula of the predicate calculus is derivable form the axiom of predicate calculus.

The unsolvability of the problem for predicate logic was showed by Alonzo Church in 1936: "A note on the Entscheidungsproblem", Journal of Symbolic Logic, (1936).

---

Consider the corresponding problem for propositional calculus: it is solved (in the positive) by the truth table method.

Answer 2

Mauro answered the historical question. As for the axioms, the limitation in these types of theorems is generally that the axioms are computable. That is there exists an algorithm to tell whether something is an axiom.

And indeed computable axioms can be infinite, for example

$$\forall \phi : \phi(0) \land (\forall n: \phi (n) \rightarrow \phi (n+1))\rightarrow \forall n \phi (n), $$

the axiom schema for induction, is an infinite computable axiom schema. In second order logic we often have axioms of the type "for all sets this holds", but then what is a "set" is left open or based on intuition or circumstances of the time. This is NOT what we are considering here, although is how some schools of mathematics operate.