命題論理における真偽判定問題の計算可能性について

はじめに

はじめまして、mineelと申します。私は理論計算機科学等を普段勉強している学部生です。

今回はタイトルの通り命題論理における真偽判定問題の計算可能性について書きました。
こういった記事を投稿するのは初めてで、至らない部分は多いとは思いますが多めにお願いします。

記事のレベルは各分野の教科書の$10$ページ目くらいの内容を書いた程度のレベルです。なので面倒な部分や説明が下手な部分はあれど、難しい点は特にないので誰でも読める内容だとは思います。(ただし長いです)

ただ、今回は数学的な解説記事というよりはやってみた系の記事の方が近く、今回は個人的な興味についての自己紹介のような記事になればいいなと思っています。
よろしくお願いします。

この記事では$0$は自然数に含めるとします。
また、～番目や～項目などと言うときは必ず$0$番目や$0$項目から始まっていることもご注意ください。

※この記事はスマホからだと死ぬほど見辛いのでPCから見るのを推奨します。
スマホから見るなら横にすればまだ少し見やすいです。

$ \DeclareMathOperator{\Var}{Var} \DeclareMathOperator{\zero}{zero} \DeclareMathOperator{\suc}{suc} \DeclareMathOperator{\add}{add} \DeclareMathOperator{\pred}{pred} \DeclareMathOperator{\input}{input} \DeclareMathOperator{\output}{output} \DeclareMathOperator{\pr}{pr} \DeclareMathOperator{\prime}{prime} \DeclareMathOperator{\pwr}{pwr} \DeclareMathOperator{\dom}{dom} \DeclareMathOperator{\get}{get} \DeclareMathOperator{\divi}{div} \DeclareMathOperator{\ins}{ins} \DeclareMathOperator{\getn}{getn} \DeclareMathOperator{\getl}{getl} \DeclareMathOperator{\getr}{getr} \DeclareMathOperator{\sub}{sub} \DeclareMathOperator{\Lhl}{Lhl} \DeclareMathOperator{\Lhr}{Lhr} \DeclareMathOperator{\Lh}{Lh} \DeclareMathOperator{\f}{f} \DeclareMathOperator{\g}{g} \DeclareMathOperator{\h}{h} \DeclareMathOperator{\p}{p} \DeclareMathOperator{\F}{F} \DeclareMathOperator{\G}{G} \DeclareMathOperator{\P}{P} \DeclareMathOperator{\v}{v} \DeclareMathOperator{\F}{F} $

真偽判定問題とは

論理式の定義

真偽判定問題の前に軽く命題論理の用語の説明から入ります。
いくつか独特な用語や記法を採用しているため、既に命題論理によくなじんでいる方も一応目は通しておおくといいかもしれません。
まずは論理式というものを定義していきます。
命題変項を$p_0, p_1,...$とします。（加算無限個）
命題変項とは、これ以上分解のできない論理式の単位のようなものだと考えていただいて大丈夫です。
また、論理式を表す記号として$A,B,C...$を使います。

$(\lnot A)$は「$A$でない」、$(A\rightarrow B)$は「$A$ならば$B$」のイメージです。ただ実際は論理式の形の定義を与えただけでまだ意味は考えてないです。
括弧がキショすぎますが、後々括弧がある方が扱いやすいのでここでは括弧付き論理式のみ考えます。
また、定義からわかるように$\land$や$\lor$は使わない主義で行きます。
$(A\land B)$とかは$(\lnot (A\rightarrow (\lnot B)))$で意味的には同じになるので別に$\land$や$\lor$はなくても表現力は変わらないです。

論理式の意味付け

また論理式の意味付けを恣意的に行っていきます。
命題変項ごとに真偽を与える関数をここでは意味付け関数と呼ぶこととします。
任意に与えられた意味付け関数に対し、その定義域を拡張して論理式に意味を与えていきます。

ここでは、命題変項全体の集合を$V$, 論理式全体の集合を$Pro$とすることにします。
また、$TV=\{真,偽\}$とし、$TV$内の演算子として否定$\lnot : TV\rightarrow TV$及び選言（＝または）$\lor : TV^2\rightarrow TV$を通常の意味で使うことにします。

この定義によって、各命題変項に対して真or偽を定めてやることで、各論理式に対しても真or偽を定めることができます。

真偽判定問題

以上の概念を用いて命題論理の真偽判定問題を定義します。

先ほどの例における$\f$及び論理式$((p_0)\rightarrow (\lnot(p_1)))$を入力としたとき出力は偽であるというようになります。

ここからこの問題がコンピュータによって計算可能であるのかを考えていきます。

計算可能性

真偽判定問題の計算可能性

問題が計算可能であるとは、その問題を解くアルゴリズムがあるということです。
真偽判定問題はどうでしょうか？

先ほどの例でも実演した通り、$\rightarrow$や$\lnot$を定義に沿って$(p_i)$という形が出てくるまで分解していき、最後は$TV$内における$\lnot$と$\lor$の定義に従って真偽を求めていけばそれで行けそうですね。ナイスアルゴリズムです！
それではお疲れさまでした！

　
　
　
　
は？？？
そんな雑な説明が認められるのでしょうか？そもそもアルゴリズムって何ですか？

ここから「アルゴリズムがある」という曖昧な言葉をしっかり数学的に定義していきます。

原始再帰的関数・再帰的関数

計算可能性を定義するためにはいくつかの方法がありますが、ここでは再帰的関数及びNプログラムという$2$つの計算モデルを提示します。まずは（原始）再帰的関数から見ていきます。
（原始）再帰的関数とは数学的に定義された自然数上の関数です。以下のように定義しますが、定義は長いのでイメージさえ分かれば大丈夫です。

あまり計算論の話を深堀するつもりはないので定義の紹介にとどめておきます。イメージとしてはさまざまな関数を繰り返しによって定義しようという感じです。

一応プログラムとの対応関係のイメージとして、最小解関数がプログラムで言うwhile文、すなわち、繰り返し回数が事前にわからないループに対応します。なので無限ループに陥り計算が止まらない可能性があるというわけです。
そういうわけで定義からも分かるように最小解関数のみが未定義を引き起こす要因となり、原始再帰的関数と違い再帰的関数は入力によっては未定義（＝無限ループ）となる可能性を持っています。
　
　
ここでようやく計算可能性の定義に移れます。

先ほど再帰的関数のイメージはさまざまな関数を繰り返しを用いて定義することと話したことと併せて考えると、計算不可能な関数とはとても繰り返しじゃ定義できないような関数というイメージとなります。
(※本来計算可能性という概念は計算モデルに依存しない普遍的な概念であるはずなので様々に同値な定義がありますが、数学的に定義が理解しやすい再帰的関数による定義をここでは採用させていただきます)　

ここで着目してほしい点が、原則として計算可能性というのはあくまで自然数上の関数にのみ定義される概念であるため、先ほどの真偽判定問題の計算可能性を判断するにはそもそも入力の論理式及び意味付け関数を自然数へとコーディングする必要があるという点です。

(※補足:と私はずっと思い込んでいたのですが、チューリング機械による計算可能性の定義が「コンピュータによって計算可能」本来の姿であり、文字列の集合上の関数に対しても計算可能性は定義されます。本当に申し訳ございませんでした)

ただ、その話に入る前にもう少し計算モデルの話を進めます。
再帰的関数の概念は計算可能関数の数学的な性質を扱うにはとても便利な概念なのですが、もう少しプログラムチックにして直感的に扱いやすい形で計算可能関数を表現してみることにします。

Nプログラム

Nプログラムとは原始再帰的関数を用いた数学的にはラベル付き有向グラフとして定義されるプログラムです。
記事の一番下の具体的なNプログラムを先に見ておけば雰囲気をつかみやすいかもしれません。
より詳しいことは参考文献の『計算論』（高橋）をご覧ください。Nプログラムの概念はこちらの本から拝借させていただきました。

すなわち、Nプログラムは変数に式の値を代入する代入命令及び二つの式の値を比較する判定命令によって構成されるプログラムのようなものとなります。
また、定義からわかる通り、Nプログラムも再帰的関数と同様に自然数の組を受け取り自然数を返す自然数上の関数となっています。
そして最も重要な点が、Nプログラムで書ける関数はすべて再帰的関数であり、再帰的関数はすべてNプログラムで書ける関数であるという点です。（ここでは証明は省きます）
これにより、再帰的関数の代わりに直感的に扱いやすいNプログラムを用いて計算可能性について考察することができるということとなります。

さて、ここから先ほどの真偽判定問題の計算可能性をちゃんと証明していきます。

真偽判定問題の計算可能性の証明（本題）

コーディング

ここからが本題となります。改めてやるべきことをまとめます。
①計算可能性は自然数上の関数にのみ定義されるので、真偽判定問題の入力である論理式及び意味付け関数を自然数へとコーディングする
②コーディングされた自然数を受け取って、正しく$0$または$1$を返す関数をNプログラムで書く
という２つのことができれば真偽判定問題の計算可能性が証明できます。

ますコーディングの話から進めていくことにします。
論理式に使われる各記号に対して自然数を割り当てるコーディング関数$\alpha$を定義します。すなわち、$\alpha$によって各論理式は自然数列へと変換されます。

これにより論理式を自然数列へと変換することができました。目標にはかなり近づいてきましたが、まだ論理式の長さによって変換後の数列の長さが異なっており扱いにくいです。
そこで、自然数列をさらに一つの自然数にまとめるゲーデル関数というものを考えます。

すなわち、ゲーデル関数とは自然数列を一つの自然数へとまとめることができ、かつ一意に元の自然数列を復元できる関数ということになります。
また、各$\G_i$をゲーデル関数$\G$の逆関数と呼びます。

このゲーデル関数及び先ほどのコーディング関数を組み合わせることで、各論理式を一意に復元できる形で一つの自然数へとコーディングできるようになります。各論理式に対応する自然数をその論理式のゲーデル数と呼ぶことにします。
これで論理式に対する操作や言明をその論理式ゲーデル数への操作や言明、すなわち記号ばかりだったのを、とうとうただの自然数に関する話へとすり替えることができました。いよいよ数学っぽくなってきました。

ところでゲーデル関数は性質だけ示してその存在はまだ示していません。そこで具体的な構成によって存在を示してみます。
ただ、ゲーデル関数の構成方法は一通りでなく、おのおの好きなように実装してもらって構わないです。
ここでは構成方法の一例をあげ、そのゲーデル関数を用いて話を進めていきます。

$\G$がゲーデル関数の性質を満たすことの証明は長くなるのでイメージだけ書きます。

証明のイメージ）
まず、$x$が素数の時$1$を返す関数$\prime (x)$は$x$未満の数$y,z$のすべての組み合わせに関して$x=y\cdot z$か調べればいいので事前に上限がわかる繰り返しで表現できるため原始再帰的です。
$\pr (x)$は$\prime $を用いて、$\pr (x-1)$から始めて$\pr (x-1)+1$は素数か、$\pr (x-1)+2$は素数かと順に調べていけばわかるため原始再帰的です。繰り返し回数の上限は「$n$より大きい最小の素数は$n!+1$以下」という事実よりわかります。
また、$\pwr(x,y)$として$x$の素因数分解における$\pr (y)$のべきを返す関数（$x=0$なら$0$を返す）とすれば、$\G_i(x)=\pwr(x,i)$により逆関数を定義できます。（素因数分解の一意性より一意に定まる）
これは、$x$は$\pr (y)$で割り切れるか、$x$は$\pr (y)^2$で割り切れるか、と順に調べていき割り切れなくなるタイミングを調べればわかるので原始再帰的です。繰り返し回数の上限はx回とすれば大丈夫です。
ついでに「割り切れるか」というのも証明は省きますがちゃんと原始再帰的です。

また、意味付け関数もコーディングする必要がありますが、$\f(\alpha)$は第$i$項目が以下のようになる$0,1$からなる自然数列を返すようにコーディング関数の定義域を拡張して、それに対して上記のゲーデル関数を用いればコーディングが完了します。
$\phantom{　}$$(\alpha (f))_i =\left\{\begin{array}{ll} 1 & (\f(p_i)が真のとき) \\ 0 & (\f(p_i)が偽のとき) \end{array} \right. $
ただし、$0 \leq i \leq \left| \dom (f)\right| -1 $です。

以上により、①のステップは完了しました。
ここから②のステップへと移っていきます。

Nプログラムの構成

コーディングにより真偽判定問題を自然数上の関数として定式化することができました。
すなわち、真偽判定問題は、$x\in \mathbb{N}$を論理式のコード、$y\in \mathbb{N}$を意味付け関数のコードとして、
$\phantom{　}$$ \P(x,y)=\left\{\begin{array}{ll} 1 & (xに対応する論理式がyに対応する意味付け関数の下で真のとき) \\ 0 & (xに対応する論理式がyに対応する意味付け関数の下で偽のとき) \end{array} \right. $
という関数$\P:\mathbb{N}^2 \rightarrow \mathbb{N}$によって定式化することができたということになります。

故に、これから示すべきことは関数$\P$が計算可能関数であるということになります。
当然、$\P$が再帰的関数であることを直接示せればよいのですが、再帰的関数の概念は直感的に扱いにくいので、同等な概念であるNプログラムを用いることによって$\P$が計算可能であることを示していきたいと思います。

証明用のNプログラムの構成の方針は以下の通りです。簡単に言えば論理式の構文木に沿って左から順にみていき、真理値を更新していく感じです。

順に説明していきます。

手順① 与えられた論理式の形を判断する

本来ならそこそこ面倒な問題だと思われますが、論理式にキショい括弧を付け続けた真価がここでついに発揮されます。
コーディング関数の定義を見直してみましょう。

よく見ると自然数列へと変換した後の、第$1$項目に特徴が表れていませんか？
（ただし数列は第$0$項目がスタートとしている）
$A$が$(\lnot B)$のときは$7$となっています。
$A$が$(B\rightarrow C)$のときは分かりにくいですが、$B$がどんな形でも$\alpha (B)$の第$0$項目は定義から必ず$3$となっていることがわかります。そしてそれ以外のときは$A$が$(p_i)$となります。
すなわち、$A$が$(B\rightarrow C)$のときは第$1$項目は$3$となっていることになります。

つまり、各論理式のコードの第$1$項目（＝$\G_1(x)$）の値を調べればすぐに論理式の形が判断できるわけです。括弧を省略しなくてほんとよかったですね！

ところで、なぜ論理式の形を知る必要があるのかということなのですが、これは論理式には合成性という、その部分論理式について調べれば全体がわかるという性質があるためになります。
故に、形を判断した後はその部分論理式を取得しなければなりません。
ただ、その前に手順②に移ります。

手順② 論理式の形をリストに記録する

記録する意義、記録をどう使うかについては後に改めて説明します。

論理式の形を記録するというのは、論理式を部分論理式に分解していくときに各部分論理式の形をメモしていくというようなイメージです。
ここではその記録の方法について説明をします。

まず、そもそもNプログラムにおいてはリストなど定義されておりません。
ではリストをどう扱うのか。
ここでは、$1$以上の自然数そのものをリストとして見るということをしてみることにします。
具体的には、自然数を素因数分解したときのべきの部分に着目し、$2$のべきが$3$ならリストの第$0$項目は$3$、$3$のべきが$0$ならリストの第$1$項目は$0$として見るといった具合です。例を見てみましょう。

例からも分かる通り、自然数は無限リストとなっており上限を気にしなくてもよいのはとても便利です。ただし、格納できるのは$0$以上の自然数のみとなっております。

また、要素の取得、挿入あたりの操作も一緒に原始再帰的関数で実装します。（削除は特に使わないので今回は無視します）

まず、取得について。
リスト$L\in \mathbb{N}$に対して$\get (L,i)$という$L$の$i$番目の要素を取得する原始再帰的関数を考えます。
これは、$\get (L,i)=\pwr(L,i)$とすることで問題なく定義できます。
（$\pwr(L,i)$の定義は$L$の素因数分解において$i$番目の素数のべきを返すというものでした）

続いてリストへの挿入について。
リスト$L\in \mathbb{N}$に対して$\ins (L,i,j)$という$L$の第$i$項目に$j\in \mathbb{N}$を挿入する原始再帰的関数を考えます。
これは、$L$の$i$番目の要素$\get (L,i)$を取得して、$i$番目の素数$\pr (i)$の$j$乗をかけて、$\pr (i)$の$\get (L,i)$乗で割ることで挿入ができます。具体的には、
$\phantom{　}$$\ins (L,i,j)=\divi (\ exp(\pr (i),\get (L,i)),\ mult(L,exp(\pr (i),j))\ )$
によって問題なく定義できます。
証明は省きますが、$mult(x,y)=x\cdot y$、$exp(x,y)=x^y$、$\divi (x,y)=y\div x$（割り切れないときは$0$を返す）はすべて原始再帰的であり、その合成なので$\ins (L,i,j)$も原始再帰的です。
流石に見づらいのでもう少しわかりやすく書くと
$\phantom{　}$$\ins (L,i,j)=(L\cdot \pr (i)^j)\div \pr (i)^{\get (L,i)}$
となります。

以上によりリストに対する要素の取得、要素の挿入が定義できました。
　
　
話を戻します。論理式の形をリストに記録するという話でしたが、各形式の論理式に対して具体的にどんな自然数を記録すればよいのでしょうか。

論理式が否定形だったら$\alpha (\lnot )=7$より$7$を記録すれば、記録を見返したときに否定形だったことがすぐ分かるので良さそうです。
含意形（$(B\rightarrow C)$の形）だったらどうでしょう。一見$\alpha (\rightarrow )=11$なので$11$を記録すればよいのでは？となりますが、実は問題があります。

今回の証明の方針では論理式の構文木を"左から"見ていくという方針をとっており、含意形の論理式に対して手順③においては左の部分論理式しか取得しません。
その後に、手順⑥においてさかのぼっていく際に含意形の記録を見つけたら右の部分論理式について見ていくという方針にしています。
故に、含意形の論理式を記録する際には右側の部分論理式の情報も同時に記録する必要があるわけです。
これがこの手順で論理式を記録する必要性が出てくる理由の１つとなります。

そのために、含意形の記録だとわかり、なおかつすぐに右側の部分論理式の情報も得られるような記録といったら、右側の部分論理式のコードをそのまま記録するのが一番良いでしょう。実は記録用リストに記録する情報は否定形か含意形かの$2$種類の情報しか記録しません。
なので、記録が$7$と等しいか等しくないかさえ分かれば十分なので、含意形の記録の際に右側の部分論理式のコードを記録すれば問題ないというわけです。（なので正直否定形の方も$7$を記録することに本質的な意義はありません）

ところで、論理式が$(p_i)$の形だったらどうするんだ、となりますが、そこは構文解析の終着点であり、そこまで着いたら記録をさかのぼるステップに入るので特に記録は必要ないです。

ちなみに、まだこの段階は論理式の構文を解析してるだけの段階なので、肝心の論理式の真理値についてはまだ何も触れていません。
手順⑤以降で真理値の更新をしていきます。

手順③ 論理式の形に添って部分論理式を取得する

論理式が$(\lnot B)$の形だったら$B$のコード得る$\getn (x)$を、$(B\rightarrow C)$の形だったら$B$のコードを得る$\getl (x)$と$C$のコードを得る$\getr (x)$が必要となります。ただし、すべて原始再帰的でなければなりません。

それぞれ実装していく前に、論理式の長さを取得する関数$\Lh :\mathbb{N} \rightarrow \mathbb{N}$を実装しましょう。論理式の長さとは括弧も含めた記号の数のことを言います。これは
$\phantom{　}$$\Lh (x)=\sum_{i\lt x} \sub (1,\sub (1,\divi (\pr (i),x)))$
により定義できます。もう少しわかりやすく書くと
$\phantom{　}$$\Lh (x)=\sum_{i\lt x} \{1-(1-x/\pr (i))\}$
のような感じとなります。

それでは説明に入ります。細かい部分の証明は基本省きます。
まず、原始再帰的関数の有限和及び有限積は原始再帰的です。そして、$\sub $は
$\phantom{　}$$ \sub (x,y)=\left\{\begin{array}{ll} x-y & (x\geq y) \\ 0 & (x\lt y) \end{array} \right. $
によって定義されます。マイナスにはならない点には注意してください。故に、$\sub (1,\sub (1,x))$は
$\phantom{　}$$ \sub (1,\sub (1,x))=\left\{\begin{array}{ll} 1 & (x\gt 0) \\ 0 & (x=0) \end{array} \right. $
となります。$x$に適当に$5$など入れて確認してみてください。
また、$\divi $の定義は
$\phantom{　}$$ \divi (x,y)=\left\{\begin{array}{ll} y\div x & (yがxで割り切れる) \\ 0 & (yがxで割り切れない) \end{array} \right. $
でした。

すなわち、改めて、$\sub (1,\sub (1,\divi (\pr (i),x)))$は
$\phantom{　}$$ \sub (1,\sub (1,\divi (\pr (i),x)))=\left\{\begin{array}{ll} 1 & (xが\pr (i)で割り切れる) \\ 0 & (xが\pr (i)で割り切れない) \end{array} \right. $
というように解釈できます。当然、原始再帰的関数の合成なのでこれも原始再帰的です。

ところで、自然数$x$の表す論理式のコードは、
$\phantom{　}$$2^{\G_0 (x)}\cdot 3^{\G_1 (x)}\cdot \ ...\ \cdot \pr (\Lh (x)-1)^{\G_{\Lh (x)-1} (x)}\ \ \ \ \ (当然これはxと等しい)$
という形になっており（各$\G_i$はゲーデル関数の逆関数）、論理式のコード$x$が$\pr (0)$（＝$2$）で割り切れるか、$\pr (1)$（＝$3$）で割り切れるか、を調べていき、割り切れたら$1$を足すということを繰り返せば論理式の長さが得られることとなり、上述の$\Lh $の定義が得られます。
繰り返しの回数は少なくとも$\pr (x)$まで調べればさすがに大丈夫です（かなり余裕を持った上限の取り方になっています）

また、$B\rightarrow C$においての左の部分論理式の長さを得る原始再帰的関数$\Lhl :\mathbb{N} \rightarrow \mathbb{N}$も定義しましょう。
$\Lhr$さえ分かれば、右の部分論理式の長さを得る原始再帰的関数$\Lhr :\mathbb{N} \rightarrow \mathbb{N}$は$\Lhl $を用いて
$\phantom{　}$$\Lhr (x)=\sub (\Lh (x),\suc ^3(\Lhl (x)))$
により得ることができます。そして、$\Lhl $は以下のようにして得ることができます。
$\phantom{　}$$\Lhl (x)=\mu _{z\lt x} (\sub (\sum_{i\lt z} \sub (\suc (\divi (3,\pwr(x,\suc (i)))),\divi (5,\pwr(x,\suc (i))),\suc (i)))=0)$
鬼のように見づらいので、もう少しわかりやすく書くと
$\phantom{　}$$\Lhl (x)=\mu _{z\lt x} [\ \sum_{i\lt z} \{1+\G_{i+1}(x)/3-\G_{i+1}(x)/5\}=i+1\ ]$
となります。各$\G_j$はゲーデル関数の逆関数です。$\mu _{z\lt x}$については後述します。

では、$\Lhl $の説明に入ります。
まず、イメージとしては左から順に記号を見ていって、左括弧を見たら$1$を足す、右括弧を見たら$1$を引くというようにして、合計が$0$になった時点の位置を出力するといった具合です。すなわち、右括弧の数がそれまでの左括弧の数と等しくなった位置が左の部分論理式の終わりの位置という考えを利用しました。
詳しく見てみると、まず、$1+\G_{i+1}(x)/3-\G_{i+1}(x)/5$の部分が、自然数$x$に対応する論理式の$i+1$番目の記号が「$($」ならば$2$、「$)$」ならば$0$、「$($」でも「$)$」でもないならば$1$を返す関数となっていることがわかります。すなわち、左括弧の数と右括弧の数が等しくなるタイミングで
$\phantom{　}$$\sum_{i} \{1+\G_{i+1}(x)/3-\G_{i+1}(x)/5\}=i+1$
となることがわかります。

今$i$は$0$から$z-1$まで動かして和を取るようになっているため、ちょうど上の式が成り立つタイミングで終わるような$z$がもらえればよいことになりますが、それを実現してくれるのが限定最小解関数$\mu _{z\lt x}$となるわけです。
つまり、$\mu _{z\lt x}$というのは、$z$を$0$から調べていき、括弧の中身の式が初めて成立するような$z$を返す関数となります。
再帰的関数の定義にあった通常の最小解関数との違いは、$z$の探索範囲に上限があるという点です。（今回の上限は$x$）
こちらも証明は省きますが、括弧の中身の式が原始再帰的ならば最小解関数も原始再帰的となります。
また、ここでは詳しくは説明しませんが、$=$は実は原始再帰的述語と呼ばれるものであり、しっかり原始再帰的です。すなわち、$\Lhl $全体も原始再帰的ということとなります。

これで準備が完了したので、いざ$\getn ,\getl ,\getr $を実装していきましょう。
$\phantom{　}$$\getn (x)= \prod_{i\lt \sub (\Lh (x),3)} exp(\pr (i),\pwr(x,\suc ^2 (i))$
$\phantom{　}$$\getl (x)=\prod_{i\lt \Lhl (x)} exp(\pr (i),\pwr(x,\suc (i))$
$\phantom{　}$$\getr (x)=\prod_{i\lt \Lhr (x)} exp(\pr (i),\pwr(x,\add (i,\suc ^2(\Lhl (x))))$
により得られます。全てもう少し見やすく書くと、
$\phantom{　}$$\getn (x)= \prod_{i\lt \Lh (x)-3} \pr (i)^{\G_{i+2} (x)}$
$\phantom{　}$$\getl (x)=\prod_{i\lt \Lhl (x)} \pr (i)^{\G_{i+1} (x)}$
$\phantom{　}$$\getr (x)=\prod_{i\lt \Lhr (x)} \pr (i)^{\G_{i+(\Lhl (x)+2)} (x)}$
となっています。

これについては、自然数$x$に対応する論理式のコードが
$\phantom{　}$$2^{\G_0 (x)}\cdot 3^{\G_1 (x)}\cdot \ ...\ \cdot \pr (\Lh (x)-1)^{\G_{\Lh (x)-1} (x)}\ \ (=\ \ \prod_{i\lt \Lh (x)}\pr (i)^{\G_i (x)}\ \ )$
という形となっていることを思い出せばほとんど見たまんまですが、例えば$\getn $は部分論理式の長さが全体の長さ$\Lh (x)$から$($と$\lnot$と$)$の$3$つを抜いた$\Lh (x)-3$なので$i$は$0$から$\Lh (x)-4$まで動かせばよく、各$\pr (i)$のべきは元の論理式から$($と$\lnot$の$2$個分ずらしていけば否定形の部分論理式を得ることができます。また、原始再帰的関数の有限積は原始再帰的でしたので当然$\getn $も原始再帰的です。
残り二つについても全く同様です。

非常に目が疲れるパートでしたがこれで手順③の目標は達成できたこととなります。

手順④ 取得した論理式について①～③を論理式の形が$(p_i)$になるまで繰り返す

これは与えられた論理式のコードを手順③で得た論理式のコードに書き換えて、同じことを繰り返すだけです。手順①で論理式の形が$(p_i)$になっていることがわかったら、手順⑤に進みます。

手順⑤ $\f(p_i)$の値に沿って真理値を更新する

やっと真理値に触れることができます。終わりまでもう少しです。

まず、そもそも$\f(p_i)$を求める方法を考えます。
ただこれは簡単で、意味付け関数$\f$は、第$i$項目が命題変項$p_i$の$\f$における真偽（$0$または$1$）となる$0$と$1$の自然数列（のコード）として与えられるので、その第$i$項目が$\f(p_i)$ということになります。
意味付け関数のコードは自然数$y$で与えられているため、$\pwr(y,i)$により命題変項$p_i$の真偽（$0$または$1$）を取り出すことができます。
すなわち、
$\phantom{　}$$\f(p_i)=真 \Longleftrightarrow \pwr(y,i)=1$
と書けます。
ただし、$\pwr(y,i)$は$y$の素因数分解における$\pr (i)$（＝$i$番目の素数）のべきを返す関数でした。

しかし、$p_i$の$i$は直接与えられるわけではありません。論理式$(p_i)$のコード$x\in \mathbb{N}$から$i$を取り出さなければいけません。
コーディング関数の定義より$\alpha (p_i)=13+2i$であり、また、$(p_i)$のコード$x$から$p_i$のコードの部分を取り出すには$\pwr(x,1)$とすればよいので、$i$は
$\phantom{　}$$\divi(\sub (\pwr(x,1), 13), 2)$
により論理式のコード$x$から取り出すことができます。
ただし、$\pred $は$\pred (x)=x-1$（$x=0$なら$0$を返す）でした。
故に、$i$にこの式を当てはめることで改めて、
$\phantom{　}$$\f(p_i)=真 \Longleftrightarrow \pwr(y,\divi(\sub (\pwr(x,1), 13), 2))=1$
となることがわかります。
ただし、少し長いので$\v(x,y)=\pwr(y,\divi(\sub (\pwr(x,1), 13), 2))$と書くことにします。
（$x$は入力の論理式のコード、$y$は入力の意味付け関数のコードでした）

これで$\f(p_i)$を求める方法がわかりましたので、真理値を更新方法を考察していきましょう。
真理値を格納する変数を$tv$とし、初期値は$0$とします。
更新の方法は、元の$tv$の値に直接$\f(p_i)$の値を代入するという方法で$tv$の値を更新していきます。なぜこのように真理値を更新していけばよいのかは後に解説します。
したがって、具体的な真理値の更新を表す式は
$\phantom{　}$$tv:=\v(x,y)$
とすれば大丈夫です。
「$:=$」はNプログラムにおける代入命令に使われる記号で、左の変数に右の式を代入するという意味でした。

手順⑥ 論理式の形を記録したリストを後ろからさかのぼり、形に添って真理値を更新していく

この手順が真偽判定問題の答えを得るための核となる手順です。
この手順で手順②において論理式の形を記録したリストを活用していくこととなります。

リストについて振り返ると、リストの中身は、形が$\lnot$であることを記録した$7$及び形が$\rightarrow$であることと右の論理式の情報を記録した$\getr (x)$の二種類しかありません。
なので、論理式の分解が終わり記録をさかのぼって真理値を更新していく際には、この二種類の記録に対してそれぞれどう$tv$を更新していけばよいかを考えれば十分だとわかります。
リストの自然数がどちらの記録なのかは、その自然数が$7$であるかどうかを調べればわかるのでした。

まず、$7$を見たときについて。
今見ている論理式が$(\lnot B)$という形だったとします。
今、リストをさかのぼって$\getr (x)$まで戻ってきたということは、論理式$B$の真理値の解析は終わっており、その値は$tv$に格納されている状況にあることになります。なので、$(\lnot B)$の真理値を知りたかったら$tv$の値を逆転させればよいです。すなわち具体的な更新の式は
$\phantom{　}$$tv:=\sub (1,tv)$
とすることで$tv$の値を逆転させることができます。

続いて、$\getr (x)$を見たときについて。
今見ている論理式が$(B\rightarrow C)$という形だったとします。
今、論理式を分解していくときは左からみていくという方針を取っていました。
なので、リストをさかのぼって$\getr (x)$まで戻ってきたということは、論理式$B$の真理値の解析は終わっており、その値は$tv$に格納されている状況にあることになります。

もし、$B$の真理値が偽だったとしましょう。
この場合はラッキーで、$\F((B\rightarrow C)) = \lnot \F(B) \lor \F(C)$だったことを思い出せば、$B$が偽なら$(B\rightarrow C)$全体の真理値も真だということとなります。故に、もはや$C$のことなど忘れて、即座に$tv$の値を$1$に更新すればよいこととなります。

では、$B$の真理値が真だったとしましょう。
こちらの場合は$(B\rightarrow C)$全体の真理値はまだわかりません。ただしかし、この場合には実は$C$の真理値と$(B\rightarrow C)$全体の真理値が完全に一致することはわかります。
なので、この場合には論理式$B$のことなど完全に忘れてもう一度$1$から論理式$C$について解析しなおせばよいわけです。つまり、与えられた論理式を$C$として手順①からやり直せばよいということとなります。

ちなみに、この時点でリストをさかのぼっている状態から、またリストに書き込む状態に戻るため今までの記録が邪魔になるように思えますが、別に削除とかはしなくても$\ins $関数で上書きすればよいだけなので特に気にしなくても大丈夫です。

これで真理値の更新の仕方がわかりました。

ところで、手順⑤で今までの$tv$の値を無視して$tv$には直接$\f(p_i)$の値を代入すると説明しましたが、今までの$tv$の値を利用するタイミングというのはこの手順でリストの$\lnot$や$\rightarrow$の記録を見た時だけなので、論理式を$(p_i)$まで分解していったときは、今までの値に関係なく新しく解析中の部分論理式の真理値がわかればよいので、そのまま直接$\f(p_i)$の値を使ってもよいというためになります。

手順⑦ リストの初めまでさかのぼったら、その時の真理値を出力する

基本は書いてある通りで特に説明することもないのですが、今まで触れなかったカウンターについてここで説明します。
ここでのカウンターは、その時点でリストの第何項目を見ているのかを表すカウンターとなります。なので、リストに対する要素の取得や挿入の操作をする際には、カウンターにより位置を確認します。
カウンターは手順③で部分論理式を取得した直後に$+1$し、手順⑥で一つさかのぼるごとに$-1$します。

カウンターについての説明はこの程度です。そして、カウンターを見て終了タイミングを把握し、その時の$tv$を取得すれば大丈夫となります。

実際のNプログラム

今までのことをすべて一つのNプログラムにまとめて、証明終了となります。
ただ、今の私の知識では複雑なNプログラムを$TeX$で表現することが難しく、非常に見にくい図となってしまっています。申し訳ございません。
$\begin{xy} (0,0) *+{\input (x,y)}*\frm{-}="w0", (0,-20) *+{L:=1\\c:=0\\tv:=0}*\frm{-}="w1", (0,-40) *+{\varphi :=x}*\frm{-}="w2", (0,-60) *+{\pwr(\varphi ,1)=3?}*\frm{-}="w31", (59,-60) *+{L:=\ins (L,c,\getr (\varphi ))}*\frm{-}="w32", (107,-60) *+{\varphi :=\getl (\varphi )}*\frm{-}="w33", (142,-70) *+{c:=\suc (c)}*\frm{-}="w4", (0,-80) *+{\pwr(\varphi ,1)=7?}*\frm{-}="w51", (52,-80) *+{L:=\ins (L,c,7)}*\frm{-}="w52", (107,-80) *+{\varphi :=\getn (\varphi )}*\frm{-}="w53", (0,-100) *+{tv:=v(\varphi ,y)}*\frm{-}="w6", (37,-100) *+{c:=\pred (c)}*\frm{-}="w71", (78,-100) *+{\get (L,c)=7?}*\frm{-}="w72", (118,-100) *+{tv=0?}*\frm{-}="w73", (160,-100) *+{\varphi :=\get (L,c)}*\frm{-}="w74", (78,-120) *+{tv:=\sub (1,tv)}*\frm{-}="w81", (118,-120) *+{tv:=1}*\frm{-}="w82", (78,-145) *+{c=0?}*\frm{-}="w91", (142,-145) *+{\output (tv)}*\frm{-}="w92", (142,-40) *+{}="w10", (160,-40) *+{}="w11", (15,-55) *+{}="w12", \ar "w0";"w1" \ar "w1";"w2" \ar "w2";"w31" \ar^{true\phantom{\ \ \ \ \ \ \ \ \ \ }} "w31";"w32" \ar "w32";"w33" \ar "w33";"w4" \ar^{false} "w31";"w51" \ar^{true\phantom{\ \ \ }} "w51";"w52" \ar "w52";"w53" \ar "w53";"w4" \ar^{false} "w51";"w6" \ar "w6";"w71" \ar "w71";"w72" \ar^{\phantom{\ \ \ \ \ \ \ \ }false} "w72";"w73" \ar^{false\phantom{\ \ \ \ \ \ \ \ \ \ }} "w73";"w74" \ar^{true} "w72";"w81" \ar^{true} "w73";"w82" \ar "w81";"w91" \ar "w82";"w91" \ar^{true\phantom{\ \ \ \ \ \ }} "w91";"w92" \ar "w4";"w10" \ar "w74";"w11" \ar "w11";"w12" \ar^{false} "w91";"w71" \end{xy}$

$L$がリストを表す自然数、$c$がカウンターを表す自然数、$\varphi$が論理式のコードを格納している自然数となっています。
今までのことをまとめただけなので特に説明することもありませんが、一応二つ目のノードに関しては$L,c,\varphi$を並列に初期化していますが、実際はNプログラムに並列な計算は定義されていません。ただ今回は逐次的に連続してこの三つの計算を行えばよく、特に順番も重要でないためこのような書き方をしました。
ちなみに今更ですが裸の定数は実際は$\suc^n(\zero()):\mathbb{N}^0\rightarrow\mathbb{N}$（$\suc$の$n$回合成）という定数関数で、ちゃんと原始再帰的です。

これで真偽判定問題を表す関数$\P$が計算可能であることの証明完了となります。
本当は構成したNプログラムが要件を満たすのか確認しなければなりませんがどうかお許しを。。。

おわりに

ここまで見てくださってありがとうございました。
とても見やすい記事とは言えないとは思いますが、楽しんでいただけたら何よりです。

もしこの記事で書いたような内容が面白いと感じたならば、理論計算機科学という分野を学んでみることをお勧めします。
ざっくりいうと論理学や、計算理論、圏論などを用いてプログラミング言語などについて考察していく分野だと僕は思っています。

本当にありがとうございました。お疲れさまでした。