自然演繹のボックス構造による定式化

論理記号	導入規則	除去規則
∧	∧導入 BOX	∧除去1, ∧除去2 BAR
⊃	⊃導入 BOX	⊃除去（モダスポネンス）BAR
∨	∨導入1, ∨導入2 BAR	∨除去 BOX
¬	¬導入（背理法）BOX	¬除去（矛盾）BAR

BOXまたはBARのラベル

論理記号	導入規則	除去規則
∧	pair BOX	proj1, proj2 BAR
⊃	curry BOX	eval BAR
∨	inj1, inj2 BAR	copair BOX
¬	contra BOX	conflict BAR

 Γ→ A   Γ → B

 =================[∧導入]

 Γ → A∧B
      Γ

 +------------+[pair]

 |  ↓    ↓  |

 |  --    --  |

 |  A      B  |

 +------------+[/pair]

     A∧B


 Γ → A∧B

 ===========[∧除去1]

 Γ→ A
  A∧B

 ------[proj1 A, B]

   A


 Γ → A∧B

 ===========[∧除去2]

 Γ→ A
  A∧B

 ------[proj2 A, B]

   B


 Γ → A

 ===========[∨導入1]

 Γ→ A∨B
   A

  -----[inj1 A, B]

  A∨B


 Γ → B

 ===========[∨導入2]

 Γ→ A∨B
   B

  -----[inj2 A, B]

  A∨B


 Γ → A∨B   A → Y   B → Y

 =============================[∨除去]

    Γ → Y
    A∨B

 +----------+[copair]

 |   A    B |

 | ---  --- |

 |  ↓   ↓ |

 | ---  --- |

 |   C    C |

 +----------+[/copair]

      C


 Γ, A → B

 ===========[⊃導入]

 Γ → A⊃B
    Γ

 +-------+[curry]

 | # A   |

 | ----  |

 |  ↓   |

 | ---   |

 |  B    |

 +-------+[/curry]

   A⊃B


 Γ → A⊃B  Δ → A

 ====================[⊃除去]

    Γ,Δ → B
 A∧(A⊃B)

 ----------[eval A, B]

    B


 Γ, A |→ ⊥

 ==============[¬導入]

  Γ |→ ¬A
    Γ

 +------+[contra]

 |  A   |

 | ---  |

 | ↓   |

 | ---  |

 | ⊥   |

 +------+[/contra]

   ¬A


 Γ → A   Γ → ¬A

 =====================[¬除去]

   Γ |→ ⊥
   A∧¬A

  --------[conflict]

    ⊥