Putative proofs of universal validity of first-order formulas can be checked for validity, algorithmically. In technical language, the set of proofs is primitive recursive. Essentially, this is Godel's completeness theorem, although that theorem is usually stated in a way that does not make it obvious that it has anything to do with algorithms.
