Formal Logic and Belief

As I studied mathematics I gradually learned about proofs. The first proofs were simple and required no mathematical background; it was mere common sense—rather like the proof that the square root of 2 is not the quotient of two integers. You were aware of the math but not of the proof.

Gradually the patterns of proofs began to come to your attention. Perhaps a high school geometry course explicitly discussed the form of proofs that Euclid closely followed. College logic courses first used precise definitions of logical propositions and also what it takes to be a proof. They may also provide metatheorems about proofs. A common pattern is proofs that proofs for certain propositions exist when those latter proofs are too big to write down. Another pattern is a proof that every proposition of some particular form has a proof.

I saw the study of this subject matter as a way to improve mathematics by making it more reliable. I was thus disoriented when I sat in on some graduate logic courses where the thrust was to use informal mathematical methods to discover what sorts of things a given formal system could prove, rather than exploitation of metatheory to become more certain of conventional mathematics.

The contrast was between:

Applying logic to math—(Applying formal logic to do better mathematics);
Applying math to logic—(Using conventional mathematical reasoning to elucidate various axiomatizations of mathematics).

Only the latter was in a position to discover some of the famous limitations of the mathematical method, such as undecidability and incompleteness metatheorems.