等式的推論の推論規則

推論の構造規則

回路図ではジャンクション。

1. 無（恒等、NOP）
2. 増（重複、コピー）
3. 換（クロス）

放電器は入れない。また定数true（T、I）も入れないことにする。面倒になる割に恩恵が少ないから。

推論の論理規則

略記号	役割	対応する射
Sel1	∧-消去1	π1
Sel2	∧-消去2	π2
And	∧-導入	(-, -)
MP	⊃-消去	・
DT	⊃-導入	Λ, λ

∧の交換律を入れれば、∧-消去が1つになるが、対称性を重視して左右の消去を入れておく。

等式の推論規則

1. 公理・定理のインスタンス化 Inst
2. 等式を前提とした置換 Subst

他に、等号に関する公理を入れる。

有理数の公理

足し算に関する公理、掛け算に関する公理、分配法則も入れる。定数演算記号は、+, *, 0, 1 以外に ~, (-)^-1 を入れておく。実際には、有理数を特定するわけではなくて、単に体の公理。