一貫性、完全性、正規形
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)
数学的理論は、（仮定なしで）偽を証明可能でないなら一貫性があると言われ、論理の推論規則を使って全ての定理が証明可能なら完全性があると言われる。これは論理一般に言えることで、通常はモデルの何らかの観念に対応する。しかし、それとは別に推論規則の統語的な性質としての一貫性と完全性もあり、こちらはモデルとは無関係である。まず、局所一貫性（あるいは局所還元性）とは、ある結合子の導入規則のすぐ後に同じ結合子の除去規則を使っている導出過程があったとき、その部分を除いた等価な導出過程に変換可能であることを意味する。例として論理積の場合を示す。 ------ u ------wA true B true------------------ ∧I A ∧ B true ---------- ∧E1 A true ⇒ ------ uA true これと対になる局所完全性では、除去規則を使って結合子をその導入規則の入力となる形式に分解できることを意味する。論理積での例を示す。 ---------- uA ∧ B true ⇒ ---------- u ---------- uA ∧ B true A ∧ B true---------- ∧E1 ---------- ∧E2 A true B true ----------------------- ∧I A ∧ B true これらの記法は、ラムダ計算でのβ-簡約やη-変換に正確に対応している。局所完全性では、全ての導出過程がそれに基本的結合子を導入したものと等価であることが示されている。実際、除去の後に導入が行われる順序なら、その導出を「正規; normal」であると称する。正規導出では、全ての除去は導入の前に行われる。多くの論理では、あらゆる導出には等価な正規導出があり、これを「正規形; normal form」と呼ぶ。正規形の存在は、自然演繹だけでは証明が困難だが、1961年の Dag Prawitz の著書などに示されている。間接的には、カット規則のないシークエント計算を使えば、もっと簡単に示すことができる。
※この「一貫性、完全性、正規形」の解説は、「自然演繹」の解説の一部です。
「一貫性、完全性、正規形」を含む「自然演繹」の記事については、「自然演繹」の概要を参照ください。
- 一貫性、完全性、正規形のページへのリンク
