証明図の書式を決めている動機

一言でいうと節約原理。

1. ページ節約： 紙面とインクを使わない。リソース・コストの節約。
2. 絵図排除： 絵図（イラスト・ピクチャー）を避けて活字組版で処理したい。人件費と時間の節約。
3. コピー排除： 手書きのとき、コピー（転記）を避けたい。手間の節約。
4. ムーブ排除： 手書きのとき、ムーブ（転記後に消去）を避けたい。手間の節約。
5. 記憶支援： 覚えやすいマーカー（コジツケでもいい）や一覧表。記憶負担の節約。

いずれの動機も、理論的な根拠と合理性はない。「致し方なくそうした」結果が今の書式だが、一度決まってしまうと、理論的な根拠・合理性があると勘違いする人が出てくる。コジツケを整合性があると思い込んだりする。困ったもんだ。

例 選言除去

   X      A    B
  f↓    g↓  h↓
   A∨B   C    C
  =================[右2列にCoPair]
           A∨B
          ------
   X      A    B
  f↓    g↓  h↓
   A∨B   C    C
          ------
             C
  =================[簡略化]
    X       A∨B
   f↓  [g,h]↓
   A∨B      C
  =================[SeqComp]
        X
       f↓
      A∨B
  [g,h]↓
        C
   ==============[簡略化]
         X
  f;[g,h]↓
         C

上記のリーズニング過程をできるだけ節約して書きたいので、

   X      A    B
  f↓    g↓  h↓
   A∨B   C    C
  =================[DisjElim]
        +---------
   X    |  A    B
  f↓   | g↓  h↓
   A∨B |  C    C
   -----+-----------[∨E]
    C

例 連言導入

    X     X
  f↓    g↓
    A     B
  ===========[Pair]
      X
     ----dup
    X     X
  f↓    g↓
    A     B
   ---------
      A∧B

これは十分簡略だと思うが

    X     X
  f↓    g↓
    A     B
  ===========[Pair]
    X     X
  f↓    g↓
    A     B
   ---------[∧I]
      A∧B

dupを省略してわずかに節約。

さらに、上段に対して追加した分だけを取り出して、「推論規則」とほざいたりしている。

    A     B
   ---------[∧I]
      A∧B

節約原理だけを動機にしていると思えば、サモアリナン。

表層的なキタナーイ書き方の奥に、美しく整合的な構造が確かにある。が、汚さで見えないか、汚さを美しいと勘違いするような転倒した歪んだ美意識が形成されるのでは？