一階と高階の拡張

ウィキペディア小見出し辞書

一階と高階の拡張

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 09:51 UTC 版)

「自然演繹」の記事における「一階と高階の拡張」の解説

ここまで述べてきた論理は、単種（single-sorted）論理であり、一種類のオブジェクトだけを扱った命題からなる論理である。この単純なフレームワークの拡張としては、様々なものが提案されてきた。ここでは、個体（individuals）と項（term）という種を導入する。より正確に言えば、新たな判断 "t is a term"（または "t term"）を導入する（t は概略的な表現）。変項（variables）の可算無限集合 V と、関数シンボル（functions symbols）の可算無限集合 F を想定し、項を次のように構築する。 v ∈ V------ var-Fv term f ∈ F t1 term t2 term ... tn term------------------------------------------ app-F f (t1, t2, ..., tn) term 命題を表すため、述語（predicates）の第三の可算無限集合 P を想定し、項群に対する原子述語を次のように定式化する。 φ ∈ P t1 term t2 term ... tn term------------------------------------------ pred-F φ (t1, t2, ..., tn) prop さらに、2種類の量化（全称量化 (∀) と存在量化 (∃)）を導入する。 ------ u x term ⋮ A prop---------- ∀Fu∀x. A prop ------ u x term ⋮ A prop---------- ∃Fu∃x. A prop このような量化された命題には、次のような導入規則と除去規則がある。 ------ u a term ⋮[a/x] A true------------ ∀Iu, a∀x. A true ∀x. A true t term-------------------- ∀E[t/x] A true [t/x] A true------------ ∃I ∃x. A true ------ u ------------ v a term [a/x] A true ⋮∃x. A true C true-------------------------- ∃Ea, u,v C true これらの規則で、[t/x] A と書かれている部分は、A に存在する全ての x の実体を t と置換することを意味する（詳しくはラムダ計算を参照されたい）。規則名の上付き文字は、その規則によって排除される要素を意味している。a という項は ∀I の結論には出現しない（このような項をパラメータと呼ぶ）。また、規則 ∃E における仮説名 u と v は、仮説的導出の第二前提に局所化されている。これまでの節で論じてきた命題論理は決定可能だったが、量化子を加えたことで決定不能となる。 ここまで述べた量化表現は「一階; first-order」である。その場合、量化されるオブジェクトと命題は区別される。高階論理ではその部分が異なり、命題は区別されない。命題の量化には量化の範囲があり、それが規則にも反映される。 ------ u p prop ⋮ A prop---------- ∀Fu∀p. A prop ------ u p prop ⋮ A prop---------- ∃Fu∃p. A prop 高階論理における導入規則と除去規則は、ここでは扱わない。一階論理と高階論理の間には様々な段階がある。例えば、二階論理は、項を量化した命題と、命題を量化したものを命題として扱う。