The preceding section referred to formal systems without defining them. A formal system consists of a formal language, a set of axioms and a set of rules of inference. It does not include an interpretation, although we’re usually interested in a formal system because it admits at least one useful interpretation.
The language describes the elements from which statements are built and the grammatical rules which describe how they are built from those elements. A rule of inference describes how a statement can be derived from other statements. A proof in a formal system is a finite sequence of grammatically correct statements, each of which is either an axiom or is derived, in accordance with the rules of inference, from statements earlier in the sequence. A statement is called a theorem if it forms the final statement in such a sequence and that sequence is called a proof of the theorem.
The set of axioms can be empty, finite and non-empty, or infinite. All of these cases occur in commonly used systems. In principle the set of rules of inference can also be empty, finite and non-empty, or infinite, but systems with no rules of inference are uninteresting because the only theorems in such systems are the axioms. Systems with infinitely many rules of inference are not often used.
The rules of grammar and rules of inference are required to be not merely constructive, but analytic. It should be possible not just to build more complicated expressions from simpler expressions but also to analyse a complicated expression to determine uniquely how it was built up. This process should be purely mechanical, relying solely on the structure of the expression and not on any intended interpretation. Similarly the rules of inference should enable us not just to derive statements from other statements but to check that a statement is indeed derivable from earlier statements. If there are infinitely many axioms then it should be possible not just to generate axioms but to verify whether a statement is an axiom. These requirements force us to consider questions of computability in the description of formal languages.