に対応する で決まる証明図の逆方向の写像を とします。
を と定義します。これは証明図の逆方向の写像となります。
を と定義します。これは証明図の方向の写像となります。
を を満たすものとします。 として を の元 に変換する(切り詰める)ことを考えます。 の元が一つだけのときは決まりますが、複数ある場合は に最も近いものをとることができるのかを調べていきます。
図で書くと以下のような状況です。右方向が証明図の方向です。
は の形のもの(シークエント)の全体で自由生成された と を含む可換半環で を満たすものでした。しかし と の扱い方をどうするかはっきり決めていませんでした。 の元の標準形をどうするか考えてみます。 の元は以下の「選言標準形」にすることができます。
ここでそれぞれの はシークエントです。まず と によって各行は
- も も含まない式
のどれかにすることができます。この結果に対して と を使うことによって
- も も含まない選言標準形
のどれかにすることができます。これを の元の標準形とします。]
と に対して を以下のように定義します。
- でも でもない場合は標準形の各シークエント を に変換したものの標準形
と に対して を は の変数に変数を含まない項を代入したもの全体の集合と定義します。
まず がホーン節
の和であるとき(大文字で始まるものが変数)、 を とおくと が成り立つことを見ていきます。 を と書くことにします。
は
の変数に変数を含まない項を代入したもの全体の集合になります。ここで同じ行にある同じ名前の変数には同じ項を代入します。したがってすべての変数を変数を含まない項に変更したときにも成功となるか失敗となるかという結果には影響を与えないということが言えます。 は と が一致するとき 、一致しないとき となります。変数を含まない と に対して は または となります。
以下 が となる行は省略して書くことにします。また、関係のない行の変数は変数のまま書くことにします。これは変数に変数を含まない項を代入したものすべての和を表すものとします。
は
を元として持つことがわかります。1行目は となるので となります。
は
を元として持つことがわかります。 であったので となります。
と仮定します。
は
を元として持つことがわかります。仮定より であったので すなわち となります。
以上の議論から帰納法によりすべての自然数 に対して であることがわかります。
次に を考えます。この式の標準形は というシークエントを含むので、それを に変換すると証明図を切り詰めることができます。(どうすれば良いか?)