形式体系
形式体系（けいしきたいけい、Formal System）は、数学のモデルに基づいた任意の well-defined な抽象思考体系と定義される。エウクレイデスの『原論』は史上初の形式体系とされることが多く、形式体系の特徴をよく表している。その論理的基盤による体系の命題と帰結の関係（論理包含）は、他の抽象モデルを何らかの基盤とする体系から形式体系を区別するものである。形式体系は大きな理論や分野（例えばユークリッド幾何学）の基盤またはそのものとなることが多く、現代数学ではモデル理論などと同義に扱われる。ただし形式体系は必ずしも数学的である必然性はなく、例えばスピノザの『エチカ』はエウクレイデスの『原論』の形式を模倣した哲学（倫理学）書である。
形式体系には形式言語があり、その形式言語は基本的な記号（シンボル）で構成される。形式言語の文（式）は公理群を出発点として、所定の構成規則（推論規則）に従って発展する。従って形式体系は基本的な記号群の有限の組み合わせを通して構築された任意個の数式で構成され、その組み合わせは公理群と構成規則群から作り出される[1]。
数学における形式体系は以下の要素から構成される:
- 式を構成するのに使われる有限個の記号（アルファベット）。
- 文法。すなわち、正しい式を記号から構成するための方法。例えば、論理学で言えば任意の式（記号を適当に並べたもの）が整式かどうかを決定する何らかの手順が存在する。
- 公理群または公理スキーマ。各公理は整式でなければならない。
- 推論規則群。
- 定理群。
形式体系が帰納的であるとは、公理群と推論規則群が（文脈によって）帰納的集合または帰納的可算集合である場合を意味する。
人によっては「形式主義」と「形式体系」をほぼ同義に扱うが、「形式主義」は数学や論理学以外にも適用される用語である。例えば、ポール・ディラックのブラ-ケット記法は物理学における形式主義である。
目次 |
関連する主題 [編集]
論理体系 [編集]
「論理体系」または「論理」はある種の意味論（通常、モデル理論的解釈の形態）を伴った形式体系であり、形式言語の文（自由変数を含まない論理式）に真理値を割り当てる。ある論理が健全であるとは、導出される全ての文が真と解釈されることをを意味し、ある論理が完全であるとは、逆に全ての真の文を導出できることを意味する。
形式証明 [編集]
形式証明は整式の連なりである。証明を構成する整式は、公理かまたは証明内の前の整式に推論規則を適用して導出されたものである。一連の整式の最後の整式が定理と認識される。
このような観点を総じて、数学は「形式主義」的であると称する。ダフィット・ヒルベルトは形式体系を論じる学問分野として超数学を起こした。形式体系を論じるために使われる言語を「メタ言語」と呼ぶ。メタ言語は自然言語そのものである場合もあるし、何らかの形式化がなされている場合もある。しかし、一般に研究対象である形式体系を構成する形式言語ほどには形式化されていない。
ある形式体系が与えられたとき、定理群を定義でき、それらをその形式体系内で証明できる。形式体系は証明が存在する全ての整式で構成される。すなわち全ての公理は定理とみなされる。公理や既に存在する定理に推論規則を適用して得られる整式も定理に含まれる。整式の文法とは異なり、ある整式が定理であるか否かを決定する手順は必ずしも存在しない。ここでいう定理は「形式体系についての定理」ではなく、混同をさけるため後者をメタ定理とも呼ぶ。
形式言語 [編集]
詳細は「形式言語」を参照
数学、論理学、計算機科学において、形式言語は厳密に数学的に（あるいは機械が処理可能な形で）定義された言語である。言語学が扱う言語と同様、形式言語にも一般に次の2つの観点が存在する。
数学および計算機科学の一分野として、形式言語の統語論を専門に扱う形式言語論という分野がある。形式言語論では、言語の統語論のみを扱い、意味論は考慮しない。
形式文法 [編集]
詳細は「形式文法」を参照
計算機科学および言語学において形式文法とは、文字列の集合である形式言語を正確に規定したものである。形式文法は、言語に属する文字列の生成方法を規則化した生成文法と、与えられた文字列がある形式言語に属するかどうかを判定する方法を規則化した分析的文法に大別される。分析的文法は言語の「読み方」を、生成文法は言語の「書き方」を規定したものと言うことができる。
脚注 [編集]
- ^ Encyclopædia Britannica, Formal system definition, 2007.
参考文献 [編集]
- 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.
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||
