形式体系

形式体系（けいしきたいけい、Formal System）とは、論理学や数学における概念であり、形式言語と推論規則（または変換規則）から構成される。形式体系は完全に抽象的に構築される場合もあるが、何らかの実際の現象や客観的な現実の一面を説明するために構築される場合もある。

数学では、公理と推論規則から成る形式体系から形式的証明が生み出される。この場合、定理は形式的証明の最終行に現われる。このような観点を総じて、数学は「形式主義」的であると称することもあるが、より適切には「有限主義」的であると言える。ダフィット・ヒルベルトは形式体系を論じる学問分野として超数学を起こした。形式体系を論じるために使われる言語をメタ言語と呼ぶ。メタ言語は自然言語そのものである場合もあるし、何らかの形式化がなされている場合もある。しかし、一般に研究対象である形式システムを構成する形式言語ほどには形式化されていない。

人によっては「形式主義」と「形式体系」をほぼ同義に扱うが、「形式主義」は数学や論理学以外にも適用される用語である。例えば、ポール・ディラックのブラ-ケット記法は物理学における形式主義である。

数学における形式体系は以下の要素から構成される:

1. 式を構成するのに使われる有限個の記号（アルファベット）。
2. 文法。すなわち、正しい式を記号から構成するための方法。例えば、論理学で言えば任意の式（記号を適当に並べたもの）が整論理式かどうかを決定する何らかの手順が存在する。
3. 公理群または公理スキーマ。各公理は整論理式でなければならない。
4. 推論規則群。
5. 定理群。これには全ての公理も含まれ、公理や既に存在する定理に推論規則を適用して得られる整論理式も定理に含まれる。整論理式の文法とは異なり、ある整論理式が定理であるか否かを決定する手順は必ずしも存在しない。