ABSTRACT
The axioms, theorems, and other sentences of a formal system, and also the proofs in the system, can all be taken to be strings of symbols. In mathematics and symbolic logic, various special mathematical symbols are used, but this is just a matter of convenience. Here, we may assume that the symbols we are concerned with are those that we find on a standard keyboard and use in ordinary English text-lower and upper case letters, digits, parentheses, and so on-keeping in mind that an empty space, which on a standard keyboard is generated by pressing the space bar, is also a symbol. The definitions and arguments given in the following apply to any starting set of symbols, as long as there are only finitely many symbols in the set.
