形式体系

形式体系（けいしきたいけい、Formal System）は、数学のモデルに基づいた任意の well-defined な抽象思考体系と定義される。エウクレイデスの『原論』は史上初の形式体系とされることが多く、形式体系の特徴をよく表している。その論理的基盤による体系の命題と帰結の関係（論理包含）は、他の抽象モデルを何らかの基盤とする体系から形式体系を区別するものである。形式体系は大きな理論や分野（例えばユークリッド幾何学）の基盤またはそのものとなることが多く、現代数学では証明論やモデル理論などと同義に扱われる。ただし形式体系は必ずしも数学的である必然性はなく、例えばスピノザの『エチカ』はエウクレイデスの『原論』の形式を模倣した哲学（倫理学）書である。

形式体系には形式言語があり、その形式言語は基本的な記号（シンボル）で構成される。形式言語の文（式）は公理群を出発点として、所定の構成規則（推論規則）に従って発展する。従って形式体系は基本的な記号群の有限の組み合わせを通して構築された任意個の数式で構成され、その組み合わせは公理群と構成規則群から作り出される。

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

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

形式体系が帰納的であるとは、公理群と推論規則群が（文脈によって）帰納的集合または帰納的可算集合である場合を意味する。

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

関連する主題

論理体系

「論理体系」または「論理」はある種の意味論（通常、モデル理論的解釈の形態）を伴った形式体系であり、形式言語の文（自由変数を含まない論理式）に真理値を割り当てる。ある論理が健全であるとは、導出される全ての文が真と解釈されることを意味し、ある論理が完全であるとは、逆に全ての真の文を導出できることを意味する。

形式証明

形式証明は整式の連なりである。証明を構成する整式は、公理かまたは証明内の前の整式に推論規則を適用して導出されたものである。一連の整式の最後の整式が定理と認識される。

このような観点を総じて、数学は「形式主義」的であると称する。ダフィット・ヒルベルトは形式体系を論じる学問分野として超数学を起こした。形式体系を論じるために使われる言語を「メタ言語」と呼ぶ。メタ言語は自然言語そのものである場合もあるし、何らかの形式化がなされている場合もある。しかし、一般に研究対象である形式体系を構成する形式言語ほどには形式化されていない。

ある形式体系が与えられたとき、定理群を定義でき、それらをその形式体系内で証明できる。形式体系は証明が存在する全ての整式で構成される。すなわち全ての公理は定理とみなされる。公理や既に存在する定理に推論規則を適用して得られる整式も定理に含まれる。整式の文法とは異なり、ある整式が定理であるか否かを決定する手順は必ずしも存在しない。ここでいう定理は「形式体系についての定理」ではなく、混同をさけるため後者をメタ定理とも呼ぶ。

形式言語

"「形式言語」"

形式言語は形式的な定義が与えられている言語である（そのような言語は一般に「機械可読」（machine-readable）である）。（非形式的な）自然言語と同様に、形式言語にも一般に次の2つの観点が存在する。

• 統語論は、その言語の見た目を規定し、その言語で考えられる表現の集合である（同じものであるが形式言語の分野では「構文論」と呼ばれることが多い）。
• 意味論は、その言語の各表現の意味を規定する（特にプログラミング言語では、一般的に難しいといった理由もあり（プログラム意味論を参照）意味は形式的にではなく、自然言語による説明といった形で与えられることもある）。

形式文法

参照: 形式文法

参考文献

• Raymond M. Smullyan, 1961. Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (April 1, 1961) 156 pages ISBN 0-691-08047-X
• S. C. Kleene, 1967. Mathematical Logic Reprinted by Dover, 2002. ISBN 0-486-42533-9
• Douglas Hofstadter, 1979,. Gödel, Escher, Bach: An Eternal Golden Braid ISBN 978-0-465-02656-2. 777 pages.

関連項目

• ラムダ計算
• 公理
• 形式手法
• 形式科学
• ゲーデルの不完全性定理

外部リンク

• Encyclopædia Britannica, Formal system definition, 2007.
• What is a Formal System?: Some quotes from John Haugeland's `Artificial Intelligence: The Very Idea' (1985), pp. 48–64.
• Peter Suber, Formal Systems and Machines: An Isomorphism, 1997.