Formation rule

Aformal language is an organized setofsymbols the essential feature being that it can be precisely defined in terms of just the shapes and locations of those symbols. Such a language can be defined, then, without any reference to any meanings of any of its expressions; it can exist before any interpretation is assigned to it—that is, before it has any meaning. A formal grammar determines which symbols and sets of symbols are formulas in a formal language.

Aformal system (also called a logical calculus, or a logical system) consists of a formal language together with a deductive apparatus (also called a deductive system). The deductive apparatus may consist of a set of transformation rules (also called inference rules) or a set of axioms, or have both. A formal system is used to derive one expression from one or more other expressions. Propositional and predicate calculi are examples of formal systems.

The formation rules of a propositional calculus may, for instance, take a form such that;

• if we take Φ to be a propositional formula we can also take ${\displaystyle \neg }$ Φ to be a formula;
• if we take Φ and Ψ to be a propositional formulas we can also take (Φ ${\displaystyle \wedge }$  Ψ), (Φ ${\displaystyle \to }$  Ψ), (Φ ${\displaystyle \lor }$  Ψ) and (Φ ${\displaystyle \leftrightarrow }$  Ψ) to also be formulas.

Apredicate calculus will usually include all the same rules as a propositional calculus, with the addition of quantifiers such that if we take Φ to be a formula of propositional logic and α as a variable then we can take (${\displaystyle \forall }$ α)Φ and (${\displaystyle \exists }$ α)Φ each to be formulas of our predicate calculus.

• Finite state automaton