形成規則

数理論理学において、形成規則とは、形式言語のアルファベット上で整形式語を記述するための規則である。^{[ 1 ]}これらの規則は、言語の文字列の位置と操作のみを扱う。意味論（つまり、文字列が何を意味するか）など、言語に関するその他の事柄は記述しない。（形式文法も参照）。

形式言語とは、記号の体系化された集合であり、その本質的な特徴は、記号の形状と位置のみによって正確に定義できることである。したがって、形式言語は、その表現の意味を一切考慮することなく定義できる。つまり、解釈が割り当てられる前、すなわち意味を持つ前に存在し得るのである。形式文法は、形式言語においてどの記号および記号の集合が式となるかを決定する。

形式体系（論理計算、または論理システムとも呼ばれる）は、形式言語と演繹装置（演繹システムとも呼ばれる）から構成される。演繹装置は、変換規則（推論規則とも呼ばれる）の集合、公理の集合、またはその両方から構成される。形式体系は、1つまたは複数の他の式から1つの式を導出するために用いられる。命題論理と述語論理は、形式体系の例である。

命題論理の構成規則は、例えば次のような形式をとることができる。

• Φを命題論理式とすると、${\displaystyle \neg }$Φは数式である。
• ΦとΨを命題論理式とすると、(Φ${\displaystyle \wedge }$ Ψ)、(Φ${\displaystyle \to }$ Ψ)、(Φ${\displaystyle \lor }$ Ψ) および (Φ)${\displaystyle \leftrightarrow }$ Ψ) も式である。

述語論理は通常、命題論理と同じ規則をすべて含み、さらに量化子が追加されます。つまり、Φ を命題論理の式、α を変数とすると、(${\displaystyle \forall }$α)Φ および (${\displaystyle \exists }$α)Φ はそれぞれ、我々の述語論理の式である。

• 有限状態オートマトン