形式体系

形式体系（または演繹体系）とは、推論規則を用いて公理から定理を演繹するために使用される公理体系の抽象的な構造と形式化である。^{[ 1 ]}

1921年、デイヴィッド・ヒルベルトは数学の知識の基礎として形式体系を用いることを提案した。^{[ 2 ]} しかし、1931年にクルト・ゲーデルは、基本的な算術を表現するのに十分な力を持つ一貫性のある形式体系は、その完全性を証明することはできないと証明した。これは事実上、ヒルベルトの提案が述べられたとおりには不可能であることを示した。

形式主義という用語は、形式体系の同義語として使われることもありますが、ポール・ディラックのブラケット記法のように、特定の記法スタイルを指す場合もあります。

形式システムは、少なくとも以下の構成要素を備えています。^{[ 3 ] [ 4 ] [ 5 ]}

• 形式言語とは、形式文法（生成規則または形成規則から構成される）によって形成される、アルファベットからの記号の列である整形式の式の集合である。
• 演繹体系、演繹装置、または証明体系とは、公理を入力として定理を推論する推論規則を持つ体系であり、公理と定理はどちらも形式言語の一部である。
• 場合によっては、まず単純なケースを確立し、次にそれを一般化することによって証明を導き出す帰納的システムが使用される。

形式体系は、公理の集合と推論規則の集合がそれぞれ決定可能集合または半決定可能集合である場合、再帰的（すなわち有効）または再帰的に列挙可能であると言われる。

初期の論理体系には、パーニニのインド論理学、アリストテレスの三段論法、ストア派の命題論理学、そして公孫隆（紀元前325年頃～250年頃）の中国論理学などがある。より近代においては、ジョージ・ブール、オーガスタス・ド・モルガン、ゴットロープ・フレーゲなどが貢献した。数学的論理学は19世紀のヨーロッパで発展した。

デイヴィッド・ヒルベルトは、数学の基礎的危機に対する解決策としてヒルベルト・プログラムと呼ばれる形式主義運動を提唱したが、それは最終的にゲーデルの不完全性定理によって緩和された。^{[ 2 ]} QEDマニフェストは、既知の数学を形式化しようとするその後の試みであったが、まだ成功していない。

• 形式体系の一覧
• 形式手法– 数理プログラム仕様リダイレクト先の簡単な説明を表示するページ 
• 形式科学― 形式体系によって記述される抽象構造の研究 
• 論理翻訳– テキストを論理体系に変換すること 
• 書き換えシステム– 数式内のサブ項を別の項に置き換えるリダイレクト先の簡単な説明を表示するページ 
• 置換インスタンス– ロジックにおける概念リダイレクト先の簡単な説明を表示するページ 
• 理論（数理論理学）– 形式言語における文の集合 

• ハンター、ジェフリー（1996）[1971]。メタロジック：標準一階述語論理のメタ理論入門。カリフォルニア大学出版局（1973年刊行）。ISBN 9780520023567OCLC 36312727​​ （視覚障害のある利用者も利用可能です。）

• ホフスタッター、ダグラス、1979年。『ゲーデル、エッシャー、バッハ：永遠の黄金の鎖』ISBN 978-0-465-02656-2777ページ。
• クリーネ、スティーブン・C.、1967年。『数理論理学』ドーバー社より2002年に復刻。ISBN 0-486-42533-9。
• スムリアン、レイモンド・M.、1961年。『形式体系の理論：数学研究年報』、プリンストン大学出版局（1961年4月1日）、156ページ、ISBN 0-691-08047-X。

• ウィキメディア・コモンズにある形式システム関連のメディア
• ブリタニカ百科事典、形式体系の定義、2007年
• ダニエル・リチャードソン著、『形式システム、論理学、意味論』
• PlanetMathの形式体系。
• 数学百科事典、形式体系
• ピーター・スーバー著『形式システムと機械：同型性』

Wayback Machineに2011年5月24日にアーカイブされました。917。

• レイ・タオル、形式システム
• 形式システムとは何か？ 2011年6月7日にWayback Machineにアーカイブされました：ジョン・ハウゲランドの「人工知能：その概念」（1985年）48～64ページからの引用。