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?
- Robinson arithmetic Q is a consistent (we hope!), sufficiently strong, effectively axiomatized first-order theory of arithmetic.
- 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.)