正式なシステム

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

1921年、デイヴィッド・ヒルベルトは数学における知識の基礎として形式体系を用いることを提案した。^[2]

形式主義という用語は、形式システムとほぼ同義語として使われることもありますが、ポール・ディラックのブラケット表記法など、特定の表記法を指すこともあります。

正式なシステムには次のものがあります: ^{[3] [4] [5]}

• 形式言語 は、アルファベットの記号の文字列であり、形式文法(生成規則または形成規則で構成)によって形成された、整形式の式の集合です。
• 演繹システム、演繹装置、または証明システム。公理を採用し定理を推論する推論規則を持ち、どちらも形式言語の一部です。

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

形式言語とは、形式的なシステムによって定義される言語です。言語学における言語と同様に、形式言語には一般に 2 つの側面があります。

• 構文とは、言語がどのように見えるか（より正式には、言語で有効な発話となる可能性のある表現の集合）である。
• 意味論とは、言語の発話が何を意味するかである（言語の種類に応じてさまざまな方法で形式化される）

通常、形式言語の構文のみが形式文法の概念を通じて考慮されます。形式文法の2つの主なカテゴリは、言語内の文字列の記述方法に関する規則の集合である生成文法と、文字列が言語のメンバーであるかどうかを判断するために文字列を分析する方法の規則の集合である分析文法（または還元文法^{[6] [7]}）です。

演繹システムは演繹装置とも呼ばれ、^[8]システムの定理を導き出すために使用できる公理（または公理スキーマ）と推論規則で構成されています。 ^[9]

このような演繹システムは、システムで表現される式に演繹的な性質を保持します。通常、私たちが関心を持つ性質は、虚偽ではなく真実です。ただし、正当化や信念などの他の様相が代わりに保持される場合もあります。

演繹の完全性を維持するために、演繹装置は言語の意図された解釈を参照せずに定義可能でなければなりません。目的は、導出の各行が、その前の行の論理的帰結にすぎないことを保証することです。システムの演繹的性質に関係する言語の 解釈の要素があってはなりません。

論理的基礎によるシステムの論理的帰結（または含意）は、抽象的なモデルに何らかの基礎を持つ可能性のある他のシステムと形式システムを区別するものです。形式システムは、モデル理論などの現代数学の用法と一致して、より大規模な理論または分野（ユークリッド幾何学など）の基礎となるか、またはそれらと同一視されることがよくあります。 [説明^が必要]

演繹システムの例としては、第一階述語論理で使用される推論規則や等式に関する公理が挙げられます。

演繹システムには、証明システムと形式意味論という2つの主要なタイプがあります。^[8]

形式的な証明は、公理であるか、証明シーケンス内の前の WFF に推論規則を適用した結果である、整形式の式(略して WFF)のシーケンスです。シーケンス内の最後の WFF は、定理として認識されます。

形式体系が与えられると、その形式体系内で証明できる定理の集合を定義できます。この集合は、証明があるすべての WFF で構成されます。したがって、すべての公理は定理と見なされます。WFF の文法とは異なり、与えられた WFF が定理であるかどうかを判断するための決定手順が存在するという保証はありません。

形式的な証明を生み出すことが数学のすべてであるという見方は、しばしば形式主義と呼ばれる。形式体系を議論するための学問として、ダヴィド・ヒルベルトがメタ数学を創始した。 形式体系について話すために使用する言語は、すべてメタ言語と呼ばれる。 メタ言語は自然言語である場合もあれば、それ自体が部分的に形式化されている場合もあるが、一般に、検討中の形式体系の形式言語コンポーネントほど完全には形式化されていない。形式体系の形式言語コンポーネントは、オブジェクト言語、つまり、問題となっている議論の対象と呼ばれる。 ここで定義した定理の概念を、形式体系に関する定理と混同してはならない。混乱を避けるために、形式体系に関する定理は通常、メタ定理と呼ばれる。

論理システムとは、演繹システム（最も一般的には一階述語論理）と追加の非論理公理を組み合わせたものです。モデル理論によれば、論理システムには、特定の構造（式を特定の意味にマッピングしたもの）が適切な式を満たすかどうかを記述する解釈が与えられます。形式システムのすべての公理を満たす構造は、論理システムの モデルとして知られています。

論理システムとは次のようなものです。

• 公理から推論できる各整形式の式が論理システムのすべてのモデルによって満たされる場合、健全です。
• 論理システムのすべてのモデルによって満たされる各整形式の式が公理から推論できる場合、意味的に完全です。

論理システムの例としては、ペアノ算術があります。算術の標準モデルは、議論の領域を非負の整数に設定し、記号に通常の意味を与えます。^[10]算術には非標準モデルも存在します。

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

デイヴィト・ヒルベルトは、数学の根本的な危機に対する解決策としてヒルベルト・プログラムと呼ばれる形式主義運動を扇動したが、これは最終的にゲーデルの不完全性定理によって和らげられた。^[2] QED宣言は、既知の数学を形式化するその後の、まだ成功していない努力を表していた。

• 形式システムの一覧
• 形式手法 - 数学的プログラム仕様Pages displaying short descriptions of redirect targets
• 形式科学 – 形式体系によって記述される抽象構造の研究
• 論理翻訳 – テキストを論理システムに変換する
• 書き換えシステム – 式内の部分項を別の項に置き換えるPages displaying short descriptions of redirect targets
• 置換インスタンス – 論理の概念Pages displaying short descriptions of redirect targets
• 理論（数学的論理）  – 形式言語による文の集合

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

無料辞書のウィクショナリーで「形式化」を調べてください。

• ウィキメディア・コモンズの形式体系に関連するメディア
• ブリタニカ百科事典、正式なシステム定義、2007年。
• ダニエル・リチャードソン、形式体系、論理、意味論
• ウィリアム・J・ラパポート『形式システムの構文と意味論』
• PlanetMath、形式システム
• Pr∞fWiki、定義:形式システム
• Pr∞fWiki、定義:演繹装置
• 数学百科事典、形式体系
• Peter Suber、「形式システムとマシン: 同型性」、Wayback Machineで 2011-05-24 にアーカイブ、1997 年。
• レイ・タオル、形式システム
• 形式システムとは何か?: John Haugeland の『人工知能: その概念』(1985) 48 ～ 64 ページからの引用。