FOL validity is undecidable (the Entscheidungsproblem)

Parent: first-order-logic

Hilbert asked for an algorithm deciding whether any first-order sentence is valid. Church and Turing (1936) proved there is none.

Church–Turing (1936)

There is no algorithm that decides, for an arbitrary first-order sentence, whether it is valid (equivalently, whether it is satisfiable).

Proof

Reduce the halting-problem. From a Turing machine M and input w, effectively build one first-order sentence φ that axiomatizes a run of M on w. Use predicates for the computation: "at time t, tape cell i holds symbol a", and "at time t the head is at cell i in state q". Conjoin:

the initial configuration (w on the tape, head at the start, start state);

one implication per transition of δ — "if the config at time t is such-and-such, the config at t+1 is so-and-so" (with cells away from the head unchanged);

"some time reaches a halting state".

Then a model of φ is exactly a halting computation, so M halts on w ⟺ φ is satisfiable (⟺ a dual sentence is valid). A decider for FOL validity would therefore decide halting — impossible. ∎

Not decidable, but semi-decidable

By Gödel completeness, validity is r.e.: enumerate all proofs and one shows up iff the sentence is valid. So you can confirm validity, never refute it — the one-sided semi-decidability of the r.e. world.

Where the line falls

Propositional logic is decidable (truth tables; SAT is NP-complete but decidable).
Full FOL is not — quantifying over an infinite domain is an unbounded search; that's the tipping point.
Some fragments stay decidable: monadic FOL, the two-variable fragment, Presburger arithmetic (addition only). Undecidability needs the full first-order machinery (essentially, enough to encode a machine).

This is the result Hilbert's program was really testing, and the reason Turing built his machine: to define "algorithm" precisely enough to prove none exists.