(n +2)度目：カリー／ハワード対応

論理 本編ネタ
And_intro And intro
And_left And elim left
And_right And elim right
Or_inl Or intro left
Or_inr Or intro right
fun_OR_MAKE なぜか無い
後で定義 Or elim
特殊 Imp intro
MP（不要だが） Imp elim
trivial True intro
EFQ False elim
不要 Not intro
後で定義 Not elim
  • MP = modus ponens
  • EFQ = ex falso quodlibet エクス・ファルソ・クァドリベット

メタ関数の関数化：

  • fun_IMP_INTRO = id
  • fun_NOT_INTRO
  • fun_AND_INTRO
関数 定理・証明
関数のデータ化 定理・証明の命題化
メタ関数 メタ定理・証明＝リーズニング
メタ関数の関数化 リーズニングの定理化

実際に必要なもの：

  1. And
    1. And_intro
    2. And_left
    3. And_right
  2. Or
    1. Or_inl
    2. Or_inr
    3. fun_OR_MAKE
  3. True
    1. trivial
  4. False
    1. EFQ