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

1921年、ダヴィト・ヒルベルトは数学における知識の基盤として形式体系を用いることを提案した。[2] しかし、1931年、クルト・ゲーデルは、基本的な算術を表現できるほど強力な一貫した形式体系は、それ自体の完全性を証明できないことを証明した。これは、ヒルベルトの計画が提示された通りに不可能であることを事実上示した。

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

概念

この図は、形式言語から構築できる統語的実体を示しています。記号と記号列は、大きく分けて無意味な式と整形式の式に分けられます。形式言語は、その整形式の式の集合と同一であると考えることができます。整形式の式は、大きく分けて定理と非定理に分けられます。

正式なシステムには、少なくとも以下の構成要素が含まれる: [3] [4] [5]

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

正式な言語

形式言語とは、特定のアルファベットから選ばれた記号からなる文字列の集合と、それらを用いて文を構成する演算を用いる言語です。言語学における言語と同様に、形式言語には一般的に2つの側面があります。

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

通常、形式言語の構文のみが形式文法の概念を通して考察されます。形式文法には、言語における文字列の記述方法に関する規則の集合である生成文法と、文字列が言語の構成要素であるかどうかを判断するために文字列を解析する方法に関する規則の集合である解析文法（または還元文法[6] [信頼できない情報源？ ] [7]）という2つの主要なカテゴリがあります。

演繹システム

演繹体系（演繹装置とも呼ばれる）[8]は、体系の定理を導き出すために使用できる公理（または公理スキーマ）と推論規則から構成されます。 [1]

演繹的完全性を維持するために、演繹装置は言語のいかなる解釈にも依存せずに定義可能でなければならない。その目的は、導出の各行が、その前にある行の論理的帰結に過ぎないことを保証することである。システムの演繹的性質に関与するような言語の解釈要素は一切存在すべきではない。

形式体系を、その論理的基盤による論理的帰結（あるいは含意）こそが、抽象モデルに何らかの根拠を持つ可能性のある他の体系と区別するものです。形式体系は、モデル理論などの現代数学の用法と整合し、より大規模な理論や分野（例えばユークリッド幾何学）の基礎となる、あるいは同一視されることさえあります。 [要説明]

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

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

証明システム

正式な証明は、公理であるか、証明シーケンス内の前の WFF に推論規則を適用した結果である、 整形式の式 (略して WFF) のシーケンスです。

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

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

論理体系の形式意味論

論理体系とは、演繹体系（最も一般的には一階述語論理）に非論理的な公理を加えたものである。モデル理論によれば、論理体系には、与えられた構造（式を特定の意味にマッピングしたもの）が整形式式を満たすかどうかを記述する解釈が与えられる場合がある。形式体系のすべての公理を満たす構造は、論理体系の モデルと呼ばれる。

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

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

論理体系の一例として、ペアノ算術が挙げられます。算術の標準モデルは、非負整数を議論領域とし、記号に通常の意味を与えます。[10]算術には非標準的なモデルも存在します。

歴史

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

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

参照

参考文献

  1. ^ ハンター1996、7ページより。
  2. ^ ab ザック、リチャード (2003年7月31日). 「ヒルベルトのプログラム」.ヒルベルトのプログラム, スタンフォード哲学百科事典. スタンフォード大学形而上学研究室.
  3. ^ 「形式システム」。PlanetMath。
  4. ^ ラパポート、ウィリアム・J.（2010年3月25日）「形式システムの構文と意味論」バッファロー大学。
  5. ^ 「形式体系」。Pr fWiki 。
  6. ^ 「還元文法」。『科学技術用語辞典』（第6版）McGraw-Hill。還元文法：（コンピュータサイエンス）文字列を解析し、その文字列が言語内に存在するかどうかを判断するための一連の構文規則。
  7. ^ Rulifson, Johns F. (1968年4月). 「XDS 940用のツリーメタ」(PDF) . Augmentation Research Center . 2024年11月30日閲覧.形式言語定義コンパイラ記述スキームには2つの種類があります。最も一般的なのは生成文法アプローチです。生成文法は、主に言語のあらゆる可能な文字列を生成する方法を記述する一連の規則で構成されています。一方、簡約文法または解析文法技法は、任意の文字列を分析し、その文字列が言語に含まれるかどうかを判断する方法を記述する一連の規則を規定します。
  8. ^ ab "Deductive Apparatus". Pr fWiki . 2024年11月30日閲覧。
  9. ^ van Fraassen, Bas C. (2016) [1971]. 形式意味論と論理(PDF) . Nousoul Digital Publishers. p. 12.メタロジックは、証明理論と形式意味論の2つの部分に大まかに分けることができます。…この区分は厳密なものではなく、多くの問題が両方の観点から扱われており、証明理論的な方法と結果は意味論に不可欠です。
  10. ^ ケイ、リチャード (1991). 「1. 標準モデル」.ペアノ算術のモデル. オックスフォード: クラレンドン・プレス. p. 10. ISBN 9780198532132。

出典

  • ハンター、ジェフリー(1996) [1971]. 『メタロジック：標準一階述語論理のメタ理論入門』カリフォルニア大学出版局 (1973年出版). ISBN 9780520023567. OCLC  36312727。（印刷障害のある利用者もアクセス可能）

さらに読む

無料辞書のウィクショナリーで「形式化」を調べてください。
  • ウィキメディア・コモンズの形式体系に関連するメディア
  • ブリタニカ百科事典、形式システムの定義、2007年。
  • ダニエル・リチャードソン『形式体系、論理、意味論』
  • PlanetMathの形式システム。
  • 数学百科事典、形式体系
  • Peter Suber、「形式システムとマシン: 同型性」、Wayback Machineに 2011-05-24 アーカイブ、1997 年。
  • レイ・タオル、形式システム
  • 形式システムとは何か?: John Haugeland の『人工知能: その概念』(1985 年) 48 ～ 64 ページからの引用。