Mizar - Isar 比較

• Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。
• Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。
• Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。
• Isarの前置withは前置fromと似ている。要チェック。
• Isarの前置withはMizarのthen ... by相当らしいが。
• Isarのper casesブロックがなく、proof qedで代用。どうしているのか？
• Mizarのsupposeを要チェック。Isarのnext assumeと似ているらしい。Isarのnextも要チェック。
• Mizarのthenがどのタイミングで使うかが分からない。
• Isarのusingを要チェック。

推論カルテット

1. 連言 ∧

  A  B     A∧B
 ------   ------
  A∧B       A

 - A∧B                -A
 -------(分割統治)   --------(過剰責務)
 -A   -B             - A∧(B)

2. 選言 ∨

  A          A∨B [A |- C, B |- C]
 -------   -------------------------
  A∨(B)      C


 - A∨B            -C
 -------(投機)   -----------------------------
   -A             - (A)∨(B) -[C -| A, C -| B]

3. 否定 ¬

  [A |- False]    A  ¬A
  -------------   -------(矛盾の指摘)
  ¬A              False

  - ¬A              -False
 --------------   -------------(アラ探し)
  -[False -| A]    - ¬(A)  -(A)

4. 含意 ⇒

 [A |- B]    A A⇒B
 ---------  -------
  A⇒B        B

  - A⇒B        -B
 ----------   ---------------(因果を探る)
  [B -| A]     -(A) - (A)⇒B

5. 真 True

   A      True  [True |- A]
 ------  -------------------
  True        A


 -True       -A
 -------  --------------------(何も言ってない)
 -(A)      -True -[A -| Truw ]

6. 偽 False

  A  ¬A      False
 ---------  -------
   False       (A)

  -False          -A
 ------------   -------(理不尽の正当化)
 -(A) - ¬(A)    -False

7. 全称 ∀

  P  [a]     ∀x.P
 --------    -------
  ∀x.P        P(t)

 -∀x.P       -P(t)
 --------    --------(順方向だとアブダクション)
  -P  [a]     -∀x.P

8. 存在 ∃

  P(t)    ∃x.P [P(a) |- C]
 -----    -----------------
 ∃x.P        C

 -∃x.P            -C
 -------(探索)  ----------------------
  -P(t)          -∃x.P  -[C -| P(a)]

正しい逆推論とアブダクション

推論（正確にはリーズニング）に関して次の4分類をする。

	正しい	間違っている
受け入れやすい	問題なし	誤用（アブダクション）
受け入れにくい	難解	問題なし

推論を順推論（通常の推論）と逆推論（バックワードリーズニングの原子ステップ）に分ける。問題となるのは：

1. 難解な順推論
2. 誤用な順推論
3. 難解な逆推論
4. 誤用な逆推論

難解な順推論

 [A |- False]
 -------------[背理法]
   ¬A

    A⇒B
 ------------[含意の書き換え]
   ¬A∨B

誤用な順推論

    B  A⇒B
  ----------[ニセ・モダスポネンス]
      A

    A ⇒ B
   --------[逆は真なり]
    B ⇒  A

    A ⇒ B
   -----------[否定（裏）は真なり]
   ¬A ⇒ ¬B

     P(t)
    ----------[事例を一般化]
    ∀x.P(x)

難解な逆推論

そもそも逆推論は難解だし、受容しにくい逆推論は順推論で代替されるので、実は問題にならないかも。

難解かどうかはともかく、有用な逆推論：

   - A∧B
  ---------[分割統治]
  -A    -B

   - A∨B
  ----------[投機的選択]
     -A

    -False
  ------------[アラ探し]
  - A   - ¬A

      - B
  -------------[法則の措定]
   -A   - A⇒B

     - ∃x.P(x)
  ---------------[事例の探索]
     - P(t)

        -A
   ------------[理不尽の正当化]
       -False

「アラ探し」と「理不尽の正当化」はアブダクションではなくて正しい逆推論。

• False（矛盾）をobligationとする。矛盾を示すためには、A と ¬A を同時に示さなくてはならない。もし、Aと¬Aが示せれば（見つかれば）矛盾が示せる。したがって、背景理論の矛盾が示せる。背景理論の矛盾から、背景理論の公理系の矛盾が言える。公理系の少なくともひとつは間違っていると言える。
• Aをobligationとして、矛盾をresolved obligationとする。resolved obligationである矛盾が示せればAが言える。もし、Aが明らかに変ならば、Aを肯定する（主張する、証明できる）背景理論はおかしいことになる。つまり、「理論を正当化」できるような背景（社会、世界）がおかしいことになる。

誤用な逆推論

誤用≒アブダクションの特徴は、含意や推論の方向を意識しないことなので、誤用な推論と誤用な逆推論の区別はしにくい、つうか事実上区別はないと思ってよい。

A, B, A⇒B に対して、2-in 1-outとなる推論は：

• A, B |- A⇒B アブダクション：共起から含意
• A, A⇒B |- B モダスポネンス
• B, A⇒B |- A アブダクション：ニセ・モダスポネンス

1-in 2-outとなる推論は：

• A |- B, A⇒B 誤用：逆推論：法則と結果の措定・予測
• B |- A, A⇒B 誤用：逆推論：法則と原因の措定・予測
• A⇒B |- A, B アブダクション：含意から共起、原因の絶対化・必然化

科学的逆推論を順推論として誤用している。なお、アブダクションである事例の一般化も科学的逆推論としてなら正しい。

向きの意識がない、というときの「向き」は

1. 含意（条件命題）の向き
2. 推論の向き

演繹定理から、これらの向きは同じものとみなせる。

「裏は真なり」は、逆、裏、対偶の区別がついてない、ということだろう。

科学で有用な推論

'+'が確認済みの事実・法則を表すマーカー、'-'が確認責務を示すマーカー、'?'が仮説を示すマーカーとする。

• +A -| -B, ?(A⇒B) 逆推論：法則と結果の措定・予測
• +B -| -A, ?(A⇒B) 逆推論：法則と原因の措定・予測

科学的帰納原理は、

   P(t1)  P(t2)  ... P(tn)
   ------------------------[科学的帰納]
          ∀x.P(x)

極端な例は：

      P(t)
   ---------[単一事例からの全称化]
    ∀x.P(x)

共起、因果、含意

これはホントに難しい。いずれ議論したい。