「規則」はテクニカルタームで、証明規則または導出規則〈リーズニング規則〉である。規則は、基本的〈basic | primitive | atomic | elementary〉で組み込み〈builtin〉な関数またはマクロのこと。$`
\newcommand{\Imp}{\Rightarrow}
\newcommand{\LL}{\langle} % List Left
\newcommand{\LR}{\rangle} % List Right
\newcommand{\T}[1]{\text{#1} }
\newcommand{\hinfer}{ \rightrightarrows }% horizontal meta rule (infer)
\newcommand{\num}[1]{\:\text{ - - }#1 } % numbering, labeling
`$
外部変数の約束
外部変数、つまり、人と人とのコミュニケーションにおいて、説明のための地の文〈じのぶん〉に登場する変数の約束を述べる。今ここでは、システム〈形式的体系〉とその内部言語を外から観察・記述する立場。主観位置を変えて、自分（人）がシステムになったとして、システムの動作を人がやること（生きている人間によるシステムのシミュレーション）も、もちろんある -- つうか、それが現実の証明の人による作成行為。
- ラテン文字小文字： $`a,b, x, y`$ など。内部の名前を表す外部変数、内部の名前が番号（$`{\bf N}`$ の要素）のときもある。
- アルファベットなかほどのラテン文字小文字： $`f, g`$ など。証明（名前なし関数または名前付き関数＝定理）を表す外部変数。名前付き関数の場合は、名前と本体〈名前に割り当てられた項〉を適宜置き換えてよい。
- ラテン文字大文字： $`A, B, P, Q, X, Y`$ など。内部の型項（型を表す記号表現）または命題項〈論理式〉を表す外部変数、命題は型の特殊なものとみなす（Propositions-As-Types）。
- ラテン文字小文字列 立体〈ローマン体〉： $`\T{abc}`$ など。証明規則の名前〈固有名〉、変数ではない。
- ラテン文字大文字列 立体〈ローマン体〉： $`\T{ABC}`$ など。導出規則の名前〈固有名〉、変数ではない。
- ギリシャ文字小文字 ： $`\varphi`$ など。内部のなんらかの項〈記号的表現〉を表す外部変数。
- ギリシャ文字大文字 ： $`\Gamma, \Delta`$ など。宣言（後述）のリストを表す外部変数。
リストの最後に項目を追加する演算の演算子記号は $`\cdot`$ 、リストの連接の演算子記号は $`\odot`$ 。リストの囲み記号は $`\LL\;\LR`$ とするが、適宜省略する。また、$`(\;)`$ と $`\LL\;\LR`$ を常に使い分けるわけではない（テキトーである、とてもイイカゲンである）。
内部構文の約束
内部構文（システムが使用するプログラミング言語＝内部言語の構文）の記述には外部変数が使われる（システムを外部から見ているので）。内部言語は自然言語ではない。人と人とのコミュニケーションに使用するときは自然言語〈日本語〉に翻訳して使う。
- 名前の型宣言は $`(a: A)`$ の形。ここで、$`a`$ は名前（番号かも知れない）、A は型項（命題項含む）。囲み丸括弧は適宜省略可能。
- $`(A \num{a})`$ は、$`(a: A)`$ の別表記。まったく同じ！
- 名前（番号かも知れない）の型宣言を並べたリストは、 $`\LL(a_1:A_1), \cdots, (a_n:A_n)\LR`$ の形で書く。これがコンテキスト。囲み記号 $`\LL\; \LR`$ は、関数のデカルトペアリングとコンフリクトしている。
- 計算〈名前なし関数〉、関数〈名前付き計算〉のプロファイルは $`\to`$ で書く。証明は計算、定理は関数〈名前付き計算〉。
- 高階計算〈名前なし高階関数〉、高階関数〈名前付き高階計算〉のプロファイルは二本矢印 $`\hinfer`$ で書く。導出は高階計算、マクロは高階関数〈名前付き高階計算〉。
略称（短縮名）
| 略称 | フルスペル | 使用場面・意味 |
|---|---|---|
| mp | modus ponens | 証明規則の固有名、おそらく最も有名 |
| qt | quantification | 限量すること。固有名の一部に使う |
| ex | exsistential | 形容詞で「存在に関わる」。固有名の一部に使う |
| univ | universal | 形容詞で「全称に関わる」。固有名の一部に使う |
| exam | example | 実例。固有名の一部に使う |
| contra | contradiction | 矛盾。固有名に使う |
規則の一覧
導入規則（表の第三列）と消去規則（表の第ニ列）に対称性〈symmetry〉がある、というのはコジツケのデタラメ。双対性はあるが、表の左右ではない。
| 命題の論理記号 | 仮定として使いたいとき | 結論として欲しいとき |
|---|---|---|
| $`\land`$ | $`\T{select}`$ | $`\T{AND}`$ |
| $`\lor`$ | $`\T{CASE}`$ | $`\T{insert}`$ |
| $`\Imp`$ | $`\T{mp}`$ | $`\T{CURRY}`$ |
| $`\lnot`$ | $`\T{mp}`$ | $`\T{CONTRA}`$ |
| $`\top`$ | $`\T{terminal}`$ | |
| $`\bot`$ | $`\T{initial}`$ | |
| $`\forall`$ | $`\T{univ-to-exam}`$ | $`\T{UNIV-QT}`$ |
| $`\exists`$ | $`\T{EX-USE}`$ | $`\T{exam-to-ex}`$ |
規則の仕様と使い方
よく使われる（気がする）順で並べる。日本語翻訳例はあくまで一例であり、極めて多様な言い回しがある（なにしろ日本語だから）。
モダスポネンス mp
カタカナ表記は「モーダス」が多いかも。
名前： $`\T{mp}`$
プロファイル： $`(A\num{a}), (A\Imp B \num{b}) \to (B\num{c})`$
日本語翻訳例：
$`a`$ であった。ここで $`b`$ を使えば、$`B`$ が言える（これを $`c`$ とする）。
連言の構成 AND
名前： $`\T{AND}`$
高階プロファイル：
$`\quad f: \Gamma \to (A\num{a})\\
\quad g: \Gamma \to (B\num{b})\\
\hinfer \LL f, g\LR : \Gamma \to (A\land B \num{c})
`$
日本語翻訳例：
$`a`$ は言えている。また、$`b`$ も言えている。よって、$`A \land B`$ が言える（これを $`c`$ とする）。
含意の構成 CURRY
名前： $`\T{CURRY}`$
高階プロファイル：
$`\quad f: \Gamma \cdot (A\num{a}) \to (B\num{b})\\
\hinfer {^\cap f} : \Gamma \to (A\Imp B\num{c})
`$
日本語翻訳例：
さて、ここで $`a`$ を仮定しよう。
‥‥ $`f`$ ‥‥
これで $`b`$ が言えた。
よって、$`A \Imp B`$ が示せた（これを $`c`$ とする）。
全称の構成（全称限量） UNIV-QT
名前： $`\T{UNIV-QT}`$
高階プロファイル：
$`\quad f:\Gamma \cdot (x: X) \to (P(x) \num{a} )\\
\hinfer \LL f_x \LR_{x:X} : \Gamma \to (\forall x:X. P(x) \num{b})
`$
日本語翻訳例：
さて、ここで $`x: X`$ としよう。
‥‥ $`f`$ ‥‥
これで $`a`$ が言えた。
$`x`$ は任意だったから、$`\forall x:X. P(x)`$ が示せた（これを $`b`$ とする）。
場合分け CASE
名前： $`\T{CASE}`$
高階プロファイル：
$`\quad f: \Gamma\cdot (A \num{a}) \to (C \num{b})\\
\quad g: \Gamma\cdot (B \num{c}) \to (C \num{d})\\
\hinfer [f, g] : \Gamma\cdot( A\land B \num{s}) \to (C \num{t})
`$
日本語翻訳例：
$`s`$ から $`t`$ を示したい。そのために、$`s`$ を場合分けしよう。
まず、$`a`$ の場合を示す。
‥‥ $`f`$ ‥‥
これで、$`b`$ （$`t`$ と同じだが）が示せた。
次に、$`c`$ の場合を示す。
‥‥ $`g`$ ‥‥
これで、$`d`$ （$`t`$ と同じだが）が示せた。
以上により、$`s`$ から $`t`$ が言えた。
存在の利用 EX-USE
名前： $`\T{EX-USE}`$
高階プロファイル：
$`\quad f: \Gamma\odot\LL (y:X), (P(y)\num{a}) \LR \to (A\num{b})\\
\hinfer [f_x]_{x:X} : \Gamma\cdot(\exists x:X. P(x) \num{c}) \to (A \num{d})
`$
日本語翻訳例：
$`c`$ から $`d`$ を示したい。
$`P(x)`$ である $`x`$ は存在するので、そのような $`x`$ を（念の為、名前を変えて） $`y`$ とする。
すると、次のようになる。
‥‥ $`f`$ ‥‥
これで、$`b`$（$`d`$ と同じだが）が示せた。
以上により、$`c`$ から $`d`$ が言えた。
事例の作成 univ-to-exam
名前： $`\T{univ-to-exam}`$
プロファイル：
$`\quad (\varphi : X), (\forall x:X.P(x) \num{a}) \to (P(\varphi) \num{b})`$
日本語翻訳例：
$`\varphi`$ は $`X`$ のインスタンスである。
$`a`$ により、$`X`$ の任意のインスタンスは $`P`$ なのだから、当然に $`P(\varphi)`$ である（これを $`b`$ とする）。
事例から存在 exam-to-ex
名前： $`\T{exam-to-ex}`$
プロファイル： $`(\varphi : X), (P(\varphi) \num{a}) \to (\exists x:X. P(x) \num{b})`$
日本語翻訳例：
$`\varphi`$ は $`X`$ のインスタンスである。
そして、$`\varphi`$ は $`P`$ を満たす（$`a`$ により）。
したがって、$`\varphi`$ を事例として $`b`$ が言えた。
背理法 CONTRA
否定は $`\lnot A \equiv A \Imp \bot`$ と考える。$`\T{CONTRA}`$ は、$`\T{CURRY}`$ の特別な場合。
名前： $`\T{CONTRA}`$
高階プロファイル：
$`\quad f: \Gamma \cdot (A\num{a}) \to (\bot \num{b})\\
\hinfer {^\cap f} : \Gamma \to (A\Imp \bot\num{c})
`$
日本語翻訳例：
背理法を使って示す。
否定したい命題 $`A`$ を仮定しよう（$`a`$ とする）。
‥‥ $`f`$ ‥‥
矛盾 $`b`$ が言えた。
よって、$`A \Imp \bot`$ が示せた。
つまり背理法により $`\lnot A`$ が言えた（これを $`c`$ とする）。
連言の一部抜き出し select
名前： $`\T{select-left}`$
プロファイル： $`(A\land B \num{a}) \to (A \num{b})`$
日本語翻訳例：
$`A \land B`$ であった。当然に $`A`$ は言える（これを $`b`$ とする）。
$`\T{select-right}`$ も同様、省略。
選言の構成 insert
名前： $`\T{insert-left}`$
プロファイル： $`(A \num{a}) \to (A\lor B \num{b})`$
日本語翻訳例：
$`A`$ であった。当然に $`A\lor B`$ である（これを $`b`$ とする）。
$`\T{insert-right}`$ も同様、省略。
矛盾の構成 mp
否定は $`\lnot A \equiv A \Imp \bot`$ と考える。
名前： $`\T{mp}`$
プロファイル： $`(A\num{a}), (A\Imp \bot \num{b}) \to (\bot\num{c})`$
日本語翻訳例：
$`a`$ であった。ここで $`b`$ を使えば、矛盾が言える（これを $`c`$ とする）。
自明に真 terminal
使う機会はほぼないだろう。
名前： $`\T{terminal}`$
プロファイル： $`(A\num{a}) \to (\top \num{b})`$
日本語翻訳例：
$`a`$ であった。前提に無関係に真は結論できるから、$`{b}`$ が言える。
矛盾からの結論 initial
使う機会はほぼないだろう。
名前： $`\T{initial}`$
プロファイル： $`(\bot \num{a}) \to (A \num{b})`$
日本語翻訳例：
矛盾からは何でも結論できるから、$`{b}`$ が言える。
証明作成と伝達〈コミュニケーション〉方法
正確に証明したいなら、システム〈形式的体系〉（人ではない）の振る舞いを、生きている人間がシミュレーションする。システム（人ではない）は、証明項（あるいは証明図）と導出図を出力できる。そのシステムをシミュレートする行為で、生きている人間も証明項（あるいは証明図）と導出図を出力できる。
証明項（あるいは証明図）と導出図は自然言語〈外部言語〉ではないので、そのままでは、人と人のコミュニケーションには使えない。システムの内部言語を外部言語である自然言語に翻訳する。そのとき、一部の内部言語（よく知られた論理記号とか）は外部言語としてもそのまま使える。
どこまで内部言語を外部言語に混ぜてよいかは、コミュニケーションする相手による。例えば '$`\land`$' を知らない相手なら、日本語「かつ」に置き換える。形式的表現のリテラシーが高い相手なら、内部言語を多く使える。そうでない相手だと、日本語翻訳が多くなる。
