| 論理記号 | 導入規則 | 除去規則 |
|---|---|---|
| ∧ | And導入 | And除去左, And除去右 |
| ∨ | Or導入左, Or導入右 | Or導入 |
| ⇒ | Imp導入 | Imp除去 |
| T | True導入 | (通常の証明) |
| ⊥ | (背理法による証明) | False除去 |
| ￢ | Not導入 | Not除去 |
| 1 | And intro | 基本証明 |
| 2 | And elim left | 基本証明 |
| 3 | And elim right | 基本証明 |
| 4 | Or intro left | 基本証明 |
| 5 | Or intro right | 基本証明 |
| 6 | Or elim ☓ | 組み合わせリーズニング |
| 7 | Imp intro | 基本リーズニング |
| 8 | Imp elim ☓ | 基本証明 |
| 9 | True intro ☓ | 基本証明 |
| 10 | False elim | 基本証明 |
| 11 | Not intro ☓ | 否定の定義 |
| 12 | Not elim | Imp elimの特殊ケース |
- 基本証明 8個
- 基本リーズニング 1個
- 組み合わせリーズニング 1個
- 定義 1個
- 特殊ケース 1個
実際：
- And_intro
- And_left
- And_right
- Or_inl
- Or_inr
- fun_OR_MAKE
- trivial
- EFQ
