Undecidability
lThere is no tool that
can determine whether an arbitrary predicate logic formula is
valid.
lIf there were, the
halting problem would be solvable.
lThis is because the
computation by a Turing machine can be captured
as an appropriate logical formula, one which is valid iff the Turing machine fails to halt.