Symbolic logic

Symbolic logic, is a subset of both philosophy and mathematical logic. Although the layperson may think that the term mathematical logic refers to the logic of mathematics, the truth is rather that it more closely resembles the mathematics of logic. It comprises those parts of logic that can be modeled mathematically. Although the fact is not emphasized in traditional treatments (although this may change as software advances and exposition then starts to catch up), much of the subject relies on the existence of efficient proof-checking algorithms.

Some important results, all discovered during the 1930s, are:

• Putative proofs of universal validity of first-order formulas can be checked quickly for validity, algorithmically. In technical language, the set of proofs is primitive recursive. Essentially, this is Gödel'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.

• The set of valid first-order formulas is not computable, i.e., there is no algorithm for checking for universal valitiy. There is, however, an algorithm that behaves as follows: Given a first-order formula as its input, the algorithm eventually halts if the formula is universally valid, and runs forever otherwise. If the algorithm has been running for a trillion years, the answer remains unknown. In other words, this set is "recursively enumerable", or, as it is sometimes more suggestively put, "semi-decidable".

• The set of all universally valid second-order formulas is not even recursively enumerable. This is a consequence of Gödel's incompleteness theorem.

A superb exposition of this topic, comprehensible to any mathematician, is to be found in Boolos and Jeffrey's book Computability and Logic.