- 保証〈warranty〉 ： derivation T → A
- 反駁〈refutation〉 ： derivation A → ⊥
- 証拠〈witness〉 ： 存在記号導入に使う要素、項
- 事例〈instance〉 ： 全称記号消去に使う要素、項
- 存在スタート条件〈existential starting condition〉 ： 存在記号消去に伴う開始時条件
- 全称エンド条件〈universal ending condition〉 ： 全称記号導入に伴う終了時条件
- 存在変数〈existential variable〉 ： 存在記号消去に伴う型付き変数
- 全称変数〈universal variable〉 ： 全称記号導入に伴う型付き変数
次の双対性がある。
- 保証 ←→ 反駁
- 証拠 ←→ 事例
- 存在スタート条件 ←→ 全称エンド条件
- 存在変数 ←→ 全称変数
存在と全称の双対性は、存在ボックスと全称ボックスの双対性。
