一階述語論理(1) - エレファント・コンピューティング調査報告

「論理計算と随伴関手」と「半環上のフラクタル代数」の中でプログラミング言語 Prolog のプログラムを論理計算 LK に変換しようとしていましたが、間違っていました。Prolog のプログラムが証明に対応しているのは事実で、最終的に LK に変換できればどのような対応なのかわかると思うのですが、変換が失敗しています。これは後で書き直すことにします。

ここでは数理論理学と Prolog の対応を考えます。数理論理学の中で変換に必要と思われる部分を Prolog のような計算でやってみることにします。

「数理論理学―合理的エージェントへの応用に向けて」と「数理論理学 (コンピュータ数学シリーズ)」という本を参考にします。Prolog に必要な部分だけを見たいので本をじっくり読むことはできないため、以下のサイトも参考にします。ただし記法は LK がわかりやすいという気がするので基本的には LK に従いますが、ここでは書くのが難しい記法もあるのでその場合は独自の記法で書きます。LK の記法にもいろいろあるようなので基本的には Wikipedia に従います。

Prolog の説明のために数理論理学の理論のどこまで必要なのか調べています。ある論理式とスコーレム標準形の関係がわかれば良いと思うのですが、そのために何が必要なのかまだよく知らないので調べています。

「数理論理学―合理的エージェントへの応用に向けて」によると「スコーレム標準形への変換は、充足不能性のみを保存する変換になります。」スコーレム標準形への変換は「逆変換は不可能」となります。充足不能性とは、「どのような解釈の下でも真になる論理式は恒真な論理式、ある解釈の下で真になる論理式を充足可能な論理式、どのような解釈の下でも偽になる論理式は充足不能な論理式といいます。」

「数理論理学 (コンピュータ数学シリーズ)」によると「ある式が恒真的であることと、そのスコーレム標準形が恒真的であることとは同値である。(定理5.1)」「任意の $D, M, \rho$ に対して $M[[A]]_\rho$ が true となるとき $A$ は恒真的であるという。 $A$ が恒真的でないとき、すなわち、ある $D, M, \rho$ に対して $M[[A]]_\rho$ が false となるとき、反証可能という。また、ある $D, M, \rho$ に対して $M[[A]]_\rho$ が true となるとき、充足可能という。(定義2.4)」