形式システムとは、名前、文、またはその他の方法で解釈できる一連の式または形式表現です。これらは論理と数学の基本的なセットです。
例
- 整数、有理数、代数などの数値の集合は形式的な系として定義できますが、実数または複素数のすべての超越数を含む集合は定義できません。
一般的な問題
形式システムの一般理論は、主に理論を研究するために論理学者によって設計されました。この観点から、私たちはそれらを一般的なメタ理論、すべての理論の理論として考えることができます。
形式システム理論の 3 つの基本的な問題は次のとおりです。 – 一連の公式をどのように定義するか? – 数式や数式の集合について語る数式をどのように解釈すればよいでしょうか? – 一連の公式についての真実をどのように証明するのでしょうか?
形式的な観点では制限が生じます。言葉や記号の意味にはほとんど注意が払われません。理論は現実世界への窓とはみなされません。それらは不透明です。それらには単語の集合のみが含まれており、私たちは主にその意味ではなくその形式に関心を持っています。したがって、形式主義的な観点と呼ばれます。
公理的な理論
形式的なシステムは、多くの場合、一連の公理を与え、通常の論理を使用してこれらの公理から推論することによって構築されます。たとえば、公理的集合論は形式的なシステムです。まず、公理とは、推論の出発点となる証明されていない命題であることを思い出してみましょう (たとえば、「2 点を通過すると 1 本の線だけが通過する」はユークリッド幾何学の公理です)。定理は、論理規則に従って、有限数のステップで公理から演繹される命題です。演繹規則が有効である場合、公理が真である限り、定理は真です。
公理や公式の真理は、公式が解釈されるモデル、つまり可能な宇宙に関連して定義されます。
公理理論の数え切れないほどの可能性
基本的な形式システムは数えられる集合です。直感的には、これらはすべて、そのすべての要素を列挙するための機械的なプロセスを与えることができるセットです。
公理理論は次の理由から常に数え切れないほどです。
- 公理のリストは、有限であっても無限であっても、常に決定可能です。なぜなら、何が公理であり、何が公理ではないのかを正確に知りたいからです。
- 形式的な方法では、演繹規則が機械的な性質を持ち、機械によって盲目的に適用できることが必要です。したがって、一連の正式な証明は常に決定可能です。適切にプログラムされたコンピュータに形式化された証明を提示すると、証明が正しいかどうか、公理で始まり演繹規則に従っているかどうかが応答されます。
理論、つまり定理の集合、または公理から証明可能な公式は数えることができます。なぜなら、すべての有限な公式リストの集合に対して順序を定義できるからです。それが定理であるかどうかを知りたい式 F について考えてみましょう。コンピューターは有限な数式リストを 1 つずつ調べて、それが正式な証明であるかどうかを判断します。 「はい」の場合、リストの最後の式は定理です。この式が F の場合、コンピュータは停止し、F は定理であると応答します。他の場合には、コンピュータは次の有限リストを検査します。
F が本当に定理である場合、このようにプログラムされたコンピューターは、考えられるすべての形式的な証明を調べるため、常に答えを見つけます。しかし、この方法が私たち人間にとって本当に効果的になるには、長い時間がかかり、あまりにも長すぎます。
F が定理でない場合、コンピューターは決して停止せず、新しいリストを調べ続け、新しい証明を見つけますが、F は定理ではないため、F の証明は決して見つかりません。したがって、公理理論は常に数え上げ可能ですが、それが決定可能であるかどうかはアプリオリに確実ではありません。
「優れた」形式システム S は一貫性がなければなりません。
S が矛盾の証明を許さない場合、S は首尾一貫しています (形式的には、S が A ではなく A を証明するような命題 A が存在しない場合)
それが一貫しておらず、不条理な推論の原則が論理演繹の規則の中で受け入れられている場合、すべての公式は証明可能です。すべてを証明するシステムと、その反対のシステムはまったく何も証明しません。
クルト・ゲーデルは、今世紀初頭に、たとえわずかに複雑な形式体系であっても、真ではあるが証明できない命題を含んでいることを示しました（ゲーデルの不完全性定理を参照）。
