2021年 7月15日 「10.3.3 スコーレム 関数」 を読む × 閉じる


 次の二項関係を考えてみます──

    ∀x∃y R (x, y).

 たとえば、この論理式の 「解釈」 として、「すべての男には 好みの女性(の容姿)が いくつか存する」 ということを考えてもいいでしょう www.

 さて、この論理式は 2つの変数 (束縛変数 x, y) をもっています。2つの変数を 1つの変数で記述できれば便利ですね──例えば、プログラミングでは 2つの変数を いちいち定義して コード を書くのは面倒くさいので [ コード 数が増えて、生産性・メンテナンス 負荷が高くなるので ]、しかも y の量化は存在演算子なので、それを全称演算子の束縛変数 x で表すことができれば、コード 数も コンパクト になって便利です。そこで、x と y とのあいだに なんらかの対応 (写像) があれば、y を f (x) 使って存在演算子を除去することができる──

    ∀x R (x, f (x) ).

 スコーレム 氏は、この f を 「スコーレム 関数」 として導入しました──すなわち、x および f (x) において、x を起点にして、なんらかの構成を再帰的に定義すればいいという考えです。この考えかたが 「原始再帰的 (原始帰納的) 関数」 の考えかたへと展開されていきます (原始帰納的関数については、第 11章にて後述します)。 □

 




  × 閉じる