Breaking Gentzen's bad habit

区別しない習慣が悪い癖。

連言リストと選言リストの区別

連言リストと選言リストは明確に分かるようにする。

• 連言リスト ∧(A, B, C)
• 選言リスト ∨(A, B, C)

または、

• 連言リスト (A, B, C)
• 選言リスト (A | B | C)

単元リストと空リストのとき区別できない。単元リストはいいのだが、

• 連言リスト ∧() (true) = (T)
• 選言リスト ∨() (false) = (⊥)

別な表記として、

• Π(A, B, C)
• Σ(A, B, C)

連言リストと選言リストをインデックス記法で書く。

• ∧_i(A_i)
• ∨_i(A_i)

あるいは、

• Π_i(A_i)
• Σ_i(A_i)

あるいは、

• ∀_i(A_i)
• ∃_i(A_i)

論域＝{インデックス | インデキシング}セット を明示すると：

• ∧i∈I.A_i、 Πi∈I.A_i、 ∀i∈I.A_i
• ∨i∈I.A_i、 Σi∈I.A_i、 ∃i∈I.A_i

引数を丸括弧にして、

• ∧i∈I.A(i)、 Πi∈I.A(i)、 ∀i∈I.A(i)
• ∨i∈I.A(i)、 Σi∈I.A(i)、 ∃i∈I.A(i)

アサーションとリクエストの区別

• アサーションシーケント： Γ →! B または Γ ⇒! B または Γ |-! B
• リクエストシーケント： Γ →? B または Γ ⇒? B または Γ |-? B

もっとちゃんと書けば：

• アサーションシーケント： f:: Γ |-! E:B
  • fはアサーション名=定理名
  • Γはコンテキスト＝前提〈仮定〉
  • Eは証拠式＝証明
  • Bは帰結〈結論〉
• リクエストシーケント： f:: Γ |-? _:B
  • fはリクエスト名=予想名＝問題名＝ゴール名
  • Γはコンテキスト＝前提〈仮定〉
  • _ はプレースホルダ
  • Bはターゲット

証明とリーズニングの区別

これは後日書く。