# What is the link between Church's theorem and the undecidability of predicate logic?

If I'm correct, 1936 Church's undecidability theorem shows that no consistent, sufficiently strong, effectively axiomatized theory of arithmetic is decidable. Here is my (very naive) question: why do we (if we do) take this theorem as showing that "basic" predicate logic (with no proper axioms concerning arithmetic) is undecidable?

Two facts:

1. Robinson arithmetic Q is a consistent (we hope!), sufficiently strong, effectively axiomatized first-order theory of arithmetic.
2. Q is finitely axiomatized. So we can conjoin its axioms into a single sentence $Q$.

Suppose A is an sentence of first-order arithmetic. Then, trivially, $Q \to A$ is a theorem of pure first-order logic if $A$ is a theorem of the first-order theory Q.

If there were a way of mechanically deciding what's a theorem of first-order logic, then there would be a way of mechanically deciding deciding, for any $A$, whether $Q \to A$ is a theorem of pure first-order logic, and hence a way of deciding whether $A$ is a theorem of Q.

But Church's undecidability theorem tells us that the latter is impossible. Hence there can be no way of mechanically deciding what's a theorem of first-order logic.

(Historical note. Church's theorem is mid 1930s. Robinson Arithmetic wasn't isolated until the early 1950s. So this route for getting from Church's theorem to the undecidability of first-order logic wasn't the one Church used in the 1930s. But it is the neat argument most familiar from modern treatments.)

• I haven't done yet all the reading which would be necessary for me to understand your answer thoroughly. But I'll do it soon. – Fishermansfriend Mar 17 '17 at 12:51