式、値、行為

次の3つは区別されるべき。

1. 計算指示としての式 例：算術式
2. 計算結果としの値 例：自然数値＝算術値
3. 計算する行為

計算をオペレーションと言い直すと：

1. オペレーション指示としての式
2. オペレーション結果としの値
3. オペレーションする行為

値はオペレーション結果だけではなく、オペレーションの対象物でもある。

上記のことを、証明というオペレーションに当てはめてみると：

1. オペレーション指示としての証明式
2. オペレーション結果としの証明値
3. オペレーションする証明行為

証明式という言葉は使わないので、リーズニング式、証明値は証明オブジェクトとすると：

1. オペレーション指示としてのリーズニング式（シーケント証明図）
2. オペレーション結果としの証明オブジェクト（自然演繹証明図）
3. オペレーションするリーズニング行為

算術と証明がとても違っているのは、算術の計算結果から計算式や計算行為を再現できないのに対して、リーズニング結果である自然演繹証明図から、リーズニング行為を再現できる。なので、リーズニング式／リーズニング行為を無視する傾向があるが、それが事態を分かりにくくしている。

リーズニングの基本オペレーションは

1. いくつかの証明図はビルディングブロックとして最初から与えられている。例：A |- A
2. ： 2つの証明図を併置で結合する。（モノイド積＝テンソル積）
3. ; ： 2つの証明図を連接で結合する。
4. 証明図をT（連言の単位対象）で水増しする。
5. 証明図をカリー化する。含意導入。
6. 証明図を適用する。含意消去。

算術は自然数の計算術、演繹は命題の計算術。演繹の計算対象は命題ともいえるが、むしろ直接的な計算対象は証明図。

	算術	演繹
値	自然数	命題
演算	算術演算	基本推論規則
式	算術式	証明図
変数	自然数変数	命題変数
法則	算術法則	リーズニング法則
操作	算術式の操作	証明図の操作

キッチリとした対応関係は難しいかな。