View source for Formation rule

{{Short description|Rule defining the correct structure of expressions in formal grammar}}
{{Formal languages}}

In [[mathematical logic]], '''formation rules''' are rules for describing [[Formal language#Definition|well-formed words]] over the [[Alphabet (computer science)|alphabet]] of a [[formal language]].<ref>{{Cite book |last=Hinman|first=Peter|title=Fundamentals of Mathematical Logic |date=2005 |url=https://www.routledge.com/Fundamentals-of-Mathematical-Logic/Hinman/p/book/9781568812625 |access-date=2022-11-17 |publisher=A K Peters/CRC Press |language=en |quote=Specifying the syntax of any language L follows a common pattern. First a set of symbols is given, and we define an L-expression to be any finite sequence of these symbols. Then we specify one or more sets of L-expressions which we regard as meaningful. The meaningful expressions are generally described as those constructed by following certain rules or algorithms, and the set of them is characterized as the smallest set of expressions which is closed under these formation rules.}}</ref> These rules only address the location and manipulation of the strings of the language. It does not describe anything else about a language, such as its [[semantics]] (i.e. what the strings mean). (See also [[formal grammar]]).

==Formal language==
{{Main|Formal language}}
A ''formal language'' is an organized [[set (mathematics)|set]] of [[symbol]]s 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 [[meaning (linguistics)|meaning]]s of any of its expressions; it can exist before any [[interpretation (logic)|interpretation]] is assigned to it—that is, before it has any meaning. A [[formal grammar]] determines which symbols and sets of symbols are [[Formula (mathematical logic)|formula]]s in a formal language.

== Formal systems ==
{{main|Formal system}}

A ''formal 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 rule]]s (also called ''inference rules'') or a set of [[axiom]]s, or have both. A formal system is used to [[Proof theory|derive]] one expression from one or more other expressions. Propositional and predicate calculi are examples of formal systems.

== Propositional and predicate logic ==
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 {{not}}Φ to be a formula;
* if we take Φ and Ψ to be a propositional formulas we can also take (Φ {{and}}  Ψ), (Φ {{imp}}  Ψ), (Φ {{or-}}  Ψ) and (Φ {{eqv}}  Ψ) to also be formulas.

A [[predicate calculus]] will usually include all the same rules as a propositional calculus, with the addition of [[Quantifiers (logic)|quantifiers]] such that if we take Φ to be a formula of propositional logic and α as a [[variable (mathematics)|variable]] then we can take ({{all}}α)Φ and ({{exist}}α)Φ each to be formulas of our predicate calculus.

==See also==
*[[finite-state automaton]]

== References ==
<references />{{Mathematical logic}}

[[Category:Formal languages]]
[[Category:Propositional calculus]]
[[Category:Predicate logic]]
[[Category:Rules]]
[[Category:Syntax (logic)]]
[[Category:Logical truth]]