Loading article…
数理論理学では、証明計算または証明システムは、文を証明するために構築されます。
概要
証明システムには以下の構成要素が含まれる: [1] [2]
- 形式言語:命題論理や一階述語論理など、システムによって認められる式の集合L。
- 推論規則: 公理と定理から定理を証明するために使用できる規則のリスト。
- 公理: L内の式は有効であると想定されます。すべての定理は公理から導出されます。
証明システムにおける整形式の式の正式な証明とは、その整形式の式が証明システムの定理であることを推論する証明システムの公理と推論規則の集合である。[2]
通常、与えられた証明計算は、単一の特定の形式体系以上を包含する。これは、多くの証明計算が不十分な決定性を持ち、根本的に異なる論理に使用できるためである。たとえば、典型的な例はシークエント計算であり、これは直観主義論理と関連性論理の両方の結果関係を表現するために使用できる。したがって、大まかに言えば、証明計算とは、特定の形式の形式推論によって特徴付けられるテンプレートまたは設計パターンであり、特定の形式体系を生成するために、具体的には、そのような体系の実際の推論規則を指定することによって特化することができる。この用語をどのように定義するのが最善かについては、論理学者の間でコンセンサスが得られていない。
証明計算の例
最も広く知られている証明計算は、現在でも広く使用されている古典的な計算です。
- ヒルベルトシステムのクラス[2]。その中で最も有名な例は1928年のヒルベルト・アッカーマン一階述語論理システムである。
- ゲルハルト・ゲンツェンの自然演繹計算は、構造証明理論の最初の形式主義であり、論理と関数型プログラミングを関連付ける式と型の対応の基礎となっています。
- ゲンツェンのシーケント計算は、構造証明理論の中で最も研究されている形式主義です。
他の多くの証明計算も、独創的であったか、あるいは独創的であったかもしれないが、今日では広く使用されていない。
- アリストテレスの 『オルガノン』に示された三段論法は、容易に形式化できる。項論理の庇護の下で行われる三段論法には、現代でも依然として関心が寄せられている。
- ゴットロープ・フレーゲの『 Begriffsschrift 』（1879年）の2次元表記は、通常、論理に量指定子の現代的な概念を導入したものと見なされています。
- もし歴史が違った展開を見せていたら、CS ピアースの存在論的グラフは容易に影響力のあるものになっていたかもしれない。
現代の論理学の研究には、ライバルとなる証明計算が溢れています。
- 通常のテキスト構文を何らかのグラフィカル構文に置き換えるシステムがいくつか提案されています。証明ネットや巡回計算はそのようなシステムの一例です。
- 最近、構造証明理論に関心を持つ多くの論理学者が、表示論理、ハイパーシークエント、構造計算、束ねられた含意など、深い推論を伴う計算を提案しています。
参照
参考文献
- ^ アニタ・ワシレフスカ。 「一般的な証明システム」(PDF)。
- ^ abc 「定義:証明システム - ProofWiki」。proofwiki.org 。 2023年10月16日閲覧。