形式体系とは？
けいしきたいけい
形式体系とは、記号・公理・推論規則を明示的に定め、機械的な規則のみによって定理を導き出せるように設計された論理の枠組みです。
形式体系（けいしきたいけい、formal system）は、数理論理学において、曖昧さを排した記号の集合・文法規則・公理・推論規則の四要素を厳密に定義した体系です。ここでは意味（セマンティクス）に依存せず、記号の形式的な操作だけによって証明や演繹を行うことができます。
形式体系を構成する要素は次のとおりです。
- アルファベット（記号の集合）：体系で用いる文字・記号の一覧
- 文法（構文論）：記号を組み合わせて正しい式を作るための規則
- 公理（axioms）：証明なしに真として認める出発点の式
- 推論規則（inference rules）：既存の式から新たな式を導く操作の規則
形式体系では、公理から推論規則を繰り返し適用することで導かれる式を「定理」と呼びます。この過程は機械的・アルゴリズム的に行えるため、コンピュータによる自動証明（定理証明支援系）に直結します。
形式体系の研究は20世紀初頭のヒルベルトの「形式主義」プログラムを契機に発展しました。しかしゲーデルの不完全性定理（1931年）は、十分に豊かな形式体系には「証明も反証もできない命題」が必ず存在することを示し、形式体系の限界を明らかにしました。この結果は数学・論理学・計算機科学の基礎に深い影響を与えています。
使い方・例文
プログラムの正しさを自動で検証する定理証明支援ツール（Coqなど）は形式体系を使ってソフトウェアのバグを証明によって排除する場面で活用されます。
この用語をシェア
最終更新: