from an alphabet, formed by a formal grammar (consisting of production rules or formation rules).
* Deductive system, deductive apparatus, or proof system, which has rules of inference that take axioms and infers theorems,