院試の勉強がてら教科書を読み直しているのですが、英語をちゃんと追うモチベが消失しかけそうなのでブログにまとめながら読み進めることによりモチベを回復させようと思います。

完全性の証明がメインなので他の説明は雑めです。また、意図的に数式を減らし言葉で説明しています（数式を読んで理解できる人は教科書だけで足りると思います）。一番いいのは教科書の数式と照らし合わせながら読むことですが、この記事だけでも理解ができるように書いたつもりです。

等式論理とは

たとえば $(x + y)^2=x^2 + y^2 + 2xy$ であることをコンピュータにどう証明させるか、ということを考えます。

話は次のような段階に分けられます。

文法的な点のみに着目して導出木を作る（そのために文法をちゃんと定義する）
導出木で文法的に導出される結果は実は意味的にも正しい（つまり、式の意味を考えず文法的な変換をしているだけなのに間違った式が導出されることがない）
正しい式には必ずそれを導出するような導出木が存在する

まずは1ですね。

Algebraic Specification

Algebraic Specificationとは、等式論理で用いられる演算子と公理をまとめたものです。この公理に加え、反射律や対称律などの推論規則がこの等式論理での導出規則になります（具体的に何があるかなどは省略します）

2の証明は、導出木の高さに関する帰納法（もしくは構成に関する帰納法）を使うことで比較的楽に示すことができます

ここまでの議論は、よく注意してみるとわかるように、式の意味を一切考えずになされています。式の意味というとわかりにくいかもしれませんが、要は $(x + y)^2=x^2 + y^2 + 2xy$ や $x + y = x + y^2$ のように正しい式と誤った式をまだ区別していない、という意味です。

そろそろ意味付けをしてあげましょう。

モデル

モデル（もしくは $\Sigma$ -algebra）とは、変数がとれる値の集合（これをキャリア集合と呼ぶことにする。いまの場合、たとえば実数など）と、演算子の解釈のことです。これまではまだ"+"という記号が足し算という意味をもつとは一言もいわれていませんでした（実は掛け算でした、みたいなことも否定できません）。

あるモデルのもとでの変数の評価とは、変数からキャリア集合への値の対応のことをいいます。具体的には、 $x = 1$ とする、という場合や $x = 2$ とする、という場合は（同じモデルの）別の評価ということになります。

変数の評価ができると、演算子の解釈が定義されていることから、項全体の値をも計算することができます。これを項の評価と呼ぶことにしましょう。

こうして、式が正しいとはどういうことか形式的に定義することができるようになりました。モデル $\mathbb{X}$ のもとである等式 $\mathbb{s} = \mathbb{t}$ が正しいとは、任意の変数の評価の組み合わせに対して、左辺（全体を項とみなしたとき）の評価と右辺の評価が一致する”が成り立つことをいいます。

Algebraic Specificationのもとで正しい式

ある式が、Algebraic Specificationの正しいとは、あらゆる妥当なモデルのもとでその式が正しいことをいいます。妥当なモデル（ $(\Sigma, E)$ -Algebraのこと）とは、Algebraic Specificationの公理にある任意の等式がすべてそのモデルのもとで正しいようなモデルです。

完全性の証明

いよいよ本題です。次のことを証明します。

（目標）導出できないような等式について、ある妥当なモデルが存在して、ある評価が存在し、そのもとでの左辺の評価と右辺の評価が異なる

証明は、実際にその評価が異なるようなモデルを構築することにより行われます。読みやすさのため概略を先に言っておくと、構築するモデルのキャリア集合は、これまでの例で見た実数全体のような集合ではなく、”あらゆる項全体からなる集合”を”項1 = 項2が導出できる”の同値関係で割った同値類、とします。評価は、項からその同値類への写像とします。そうすると導出できない等式について、左辺と右辺は別の同値類に分類されることになり、それがとる値（キャリア集合の要素）は自明に異なるので、左辺と右辺の評価が異なるようなモデルが実際にでき、証明完了ということになります。

騙されたような感じがする証明ですが、その感覚は正しく、実はもっとも重要なポイントは、こうして定義されたモデルが”妥当”であることの証明パートです。それを何も書かなかったため概略だけピンとこないのは当然です。

さて、細かく見ていきましょう。

まず、導出できる等式 $\mathbb{s} = \mathbb{t}$ について、同値関係 $\mathbb{s} \sim_E \mathbb{t}$ を考えます（これが同値関係となる証明は省略）。また、さらに演算子の解釈の定義がこの同値関係についてwell-definedであることを示すことができます。すなわち、演算子の引数をその同値類で置き換えても結果は変わらない、ということです。たとえば、 $(x + y)^2 + z$ の $(x + y)^2$ を $x^2 + y^2$ に置き換えても大丈夫ですよね。

あらゆる項をこの同値関係で割った同値類を考えましょう。各同値類をキャリア集合としたモデルを考えます（演算子の解釈は任意ですが、妥当なモデルであるためにはもちろんいくらかの制約がかかります）。

さて、次のような変数の評価 $J_c$ を考えましょう。すなわち、変数の評価をその変数が属する同値類、ということにします。このとき、項の構成に関する帰納法により、項の評価は、項が属する同値類であることが証明できます。ここで目標をもう一度見てみましょう。

（目標）導出できないような等式について、ある妥当なモデルが存在して、ある評価が存在し、そのもとでの左辺の評価と右辺の評価が異なる

モデルが妥当であると仮定すれば、評価として、 $J_c$ を考えると、導出できない等式の両辺では明らかに対応する値が異なるので目標を達成できます。

さて、こうして定義されたモデルが妥当であることを言えば、上述したとおり、まさにこれが”導出できない等式”の左辺と右辺の評価を（自明に）異なるものにするモデルとなります。復習ですが、モデルが妥当であることを証明するには、定義よりAlgebraic Specificationにある任意の公理がそのモデルのもとで正しいことを言えばよいです。 $J$ を任意の”変数の評価”とします。すなわち、 $J(x)$ は同値類のいずれかをとります。ここで、変数 $x_i$ が属する同値類の代表元を $u_i$ とおくことにします。このとき、左辺の $J$ での評価は、左辺に現れる $x_i$ をすべて $u_i$ で置き換えたもの、を $J_c$ で評価したものとなることが証明できます。代入に関する導出規則により、新たな等式、「公理の左辺に現れる $x_i$ をすべて $u_i$ で置き換えたもの = 右辺に現れる $x_i$ をすべて $u_i$ で置き換えたもの」が成り立ち、右辺に現れる $x_i$ をすべて $u_i$ で置き換えたものの評価は、右辺の $J$ での評価になるので、結局公理にある任意の等式について、左辺の評価と右辺の評価は一致します。つまりいまのモデルは妥当です。