A formal proof is a deductively derived expression that supports the validiaty of a statement based upon a set of axioms. A formal proof is a finite sequence of well-formed formulas each of which is an axiom or follows from the preceding formulas in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system. Formal proofs are useful because their theorems can be interpreted as true - certain - propositions. Because formal systems are based on deductive logic they have a number of important properties. Firstly: consistency, which means that no theorem of the system contradicts another. Secondly: validity, which means that the system’s rules of proof never allow a false inference from true premises. Thirdly: completeness, which means that if a formula is true, it can be proven, i.e. is a theorem of the system. Fourth: soundness, meaning that if any formula is a theorem of the system, it is true. This is the converse of completeness.