述語抽象化

論理学において、述語抽象化は、式から述語を作成した結果です。Q が任意の式である場合、その文から形成される述語抽象は (λx.Q) です。ここで、λ は抽象化演算子であり、Q で自由に出現する x はすべて (λx.Q) で λ によって束縛されます。結果として得られる述語 (λx.Q(x)) は、 (λx.Q(x))(t) のように項t を引数として取ることができるモナド述語であり、これは 't' で示されるオブジェクトが Q となるような特性を持つことを示します。

の抽象化の法則は、 (λx.Q(x))(t)≡Q(t/x)と述べており、Q(t/x)はQ内のxの自由な出現すべてをtに置き換えた結果である。この法則は、少なくとも2つの場合には一般には当てはまらないことが分かっている:(i)tが非参照である場合、および(ii)Qに様相演算子。

様相論理学では「de re  /  de dicto の区別」は次のように述べられる。

1. (DE DICTO):${\displaystyle \Box A(t)}$

2. (DE RE): . ${\displaystyle (\lambda x.\Box A(x))(t)}$

(1)では、様相演算子は式A(t)に適用され、項tは様相演算子の範囲内にあります。(2)では、tは様相演算子の範囲内に ありません。

述語抽象化の意味論とさらなる哲学的発展については、Fittingと Mendelsohn の『First-order Modal Logic』（Springer、1999 年） を参照してください。