A formal system is a language defined by a grammar together with a set of axioms, and a set of rules of inference. The rules of inference should refer only to the language and grammar, not any particular interpretation. An interpretation is sound if the axioms are true in that interpretation and the rules of inference when applied to true statements generate only true statements. Statements which can be derived from the axioms using the rules of inference are called theorems and any such derivation is called a proof of the theorem. Theorems are true in any sound interpretation. A true statement in a particular sound interpretation need not be a theorem though. This will certainly be the case if there is another sound interpretation in which the statement is false.
The above definition of theorem and proof are the one used by logicians. Mathematicians tend to use the terms somewhat differently. Mathematicians typically refer to something as a theorem only after a proof has been found. They refer to a proof in the logician’s sense as a formal proof. By an informal proof they mean a convincing argument that the statement is true in the intended interpretation. This is necessarily somewhat vague. What’s convincing to one person may not be to another. More worryingly, there’s no way to compare interpretations directly. The writer and reader of an informal proof may have subtly different interpretations and the statement may be true in the writer’s interpretation and false in the reader’s. Intermediate between formal and informal proofs we have semiformal proofs. A semiformal proof is a convincing argument that a formal proof exists. This might include, for example, an algorithm for producing such a formal proof. That’s a viable strategy in cases where it’s easier to verify that the algorithm is correct than actually to run it. We’ll see examples later.
Should you have more faith in a formal proof than an informal one? Possibly, but not necessarily. Formal proofs have many advantages. They can be checked mechanically. They imply that the statement is true in any sound interpretation. But mechanically checking only works if the checking algorithm is correct. The interpretation is only sound if the axioms are true and the rules of inference preserve truth. What assurance do we have on any of these points? Usually an informal proof! Formal proofs therefore don’t really rest on any firmer philosophical foundations than informal ones. They can still be practically useful though. Checking the soundness of an interpretation or the correctness of a verification algorithm is generally a lot of work but it only needs to be done once. In this way the situation is analogous to the one we encountered earlier with parser generators.
In reality we typically start with a language and interpretation and then look for a set of axioms and rules of inference. We shouldn’t include any false axioms or rules of inference which allow us to derive false statements from true ones. Otherwise we wouldn’t have a sound interpretation. It would be nice to have finite sets of axioms and rules of inference but sometimes it’s convenient to consider systems where one or both of those sets are infinite. We should at least insist on an algorithm for deciding whether or not a statement is an axiom or can be derived from a list of other statements via the rules of inference though.
Ideally we’d like a set of axioms and rules of inference which are large enough so that all true statements are theorems. For our module enrollment language it’s possible to accomplish this but there are many settings where it’s not possible. In fact it’s not even possible in what’s just about the simplest mathematical setting imaginable: the arithmetic of non-negative integers.