参考：選言と否定

2009-03-19セミナーでは扱わないけど（いや、触れるか？）。

        A    B

       ---  ---

        .   .

        .   .

 A∨B   C   C
      ‖

      ↓
           #1  #2

          ---  ---

           A    B

          ---  ---

          .   .

          .   .

   A∨B   C   C

  -----------------[∨消去 #1, #2]

         C

∨消去は⊃の導入と似た感じになる。∨の導入は簡単で、∧の消去と双対。

否定に関しては論理定数⊥が必要で：

    A

   ---

    .

    .

   ⊥

 

   ‖

   ↓
   #1

  ----

    A

   ---

    .

    .

   ⊥

  ----[¬導入 #1]

  ¬A

¬の消去は排中律。