PLP のプログラムが成功するとき、論理式として見ると証明図を書くことができることを帰納法で証明していきます。
となる に関する帰納法で証明します。
から始めます。PLP のプログラムは1個の述語式から始めると定義したので、
のときは書くことができません。もし書けるとしても何も書かないことになります。
のときの証明図は何も書いていないことになるので何も書かないという証明図が書けたということになりわかりにくいです。すなわち本当は
のときにも成り立つのですが、書くのが難しいので省略することにします。
のときは
となります。代入 をとると
は正規化された論理式なので
の中にある連言節
が存在して、すべての
が
の形の式(これをunify式と呼ぶことにします)となります(unify式は今のところ述語式ではありませんがここの議論ではunify式のまま残しておくとします)。
が
増えるごとにunify式は1個追加されるので
だからunify式は1個(すなわち
)となります。
PLP のプログラムを
という論理式(各 は
という形の論理式)と考えます。
まず上記の
を証明するには、
を証明する証明図を書くことができればよいということがわかります(「シークエント計算」の「 右」)。ここで
は、新しい項
を追加して
に現れる
を
にそれぞれ置き換えたものとなります。
次に を証明するには、
を証明すればよいということになります(「
右」)。
を証明するには
をどれかの
に対して証明すればよいということになります(「
左」の繰り返し)。
を証明するには、新しい変数 を追加して
を
でそれぞれ置き換えた
を証明すればよいということになります(「 左」)。
これを証明するには変数に依存した新しい定数 を追加して(PLP では関数で表します)
を
でそれぞれ置き換えた
を証明すればよいということになります(「 左」)。
これを証明するには
と
を証明すればよいということになります(「左」)。
これを証明するには
、
、… 、
と
を証明すればよいということになります(「右」)。
これを PLP の正規化された論理式の記法で書くと
という連言節となります。証明図に使う論理記号と PLP の正規化された論理式に使う論理記号が同じなのでわかりにくいですが、別の記号を使っても煩雑になるので同じ記号を使っていきます。
unify式だけからなる連言節が存在するので、そのインデックスを とすると、
となりその連言節は
となって
と
は一致します。これは証明図の公理となるので、ここから始めることで証明図を書くことができます。