WIKI :: A formal system is used for inferring theorems from axioms according to a set of rules. Each formal system uses primitive symbols (which collectively form an alphabet) to finitely construct a formal language from a set of axiomst through inferential rules of formation. The system thus consists of valid formulas built up through finite combinations of the primitive symbols—combinations that are formed from the axioms in accordance with the stated rules.