ブログラムはProver

Σを論理式の集合(考えているのはclauseの集合でしかないけど)とし、そこに入力、出力の指定/条件をつけくわえると、あるプログラムPの仕様と考えることができるだろう。

このとき、ある入力の値に対して計算結果を得るPの計算過程は、もとのΣのある証明に対応する。対応するというのは、証明から計算過程を機械的につくれるし、計算過程から証明も機械的に作れるという意味でいう。

このような個別の証明は入力の値にそれぞれ存在するもので、決してプログラム自体が証明なのではない。そういう証明の集合がプログラムだと考えるのはちょっと無理があるようにも思える。
こう考えるとプログラムPはΣからの証明についてのproverに相当するものと言えるのではないだろうか。

プログラムの計算過程に個々の証明が対応するとして、プログラムの正当性の証明というものは、そのようなPの計算過程に対応する証明全体が、Σからの証明しか含まないし、そのような証明のすべてを含んでいるというようなことを示しているのではないか。

そもそもProverはプログラムなので、プログラムがProverだという言い方にはおかしさがあるけれど、Proverといっているは、「証明を作り出す仕組み」ということであり、Σの証明を作り出すものに対する証明論がわの概念が何かという観点では、それほどおかしな話ではないと思う。