0

Modus Ponens のそのようなバリアントがあると仮定しましょう

lemma invDed: ‹(A-->B)==>(A==>B)›
  apply(rule mp)
  apply assumption
  apply assumption
  done

定理の証明に適用できますか? (つまり、A:=A、B:=A、および A-->A を以前に証明されたかのように使用します)

lemma myid2: "A==>A"

そうでない場合、なぜですか？この定理を証明する他の方法をいくつか知っています (「仮定を適用する」またはフレーゲの命題計算公理からの 5 段階証明) が、証明力学のこのニュアンスに興味がありました。

1 つのルールがありますが、別の [許容される] ルールを取得したいのですが、何が問題ですか?

4

1 に答える 1

0

での適用ruleは、右端のメタ含意 ( ==>) の後の式にのみ適用されます。したがって、次のような結果が得られますが、これはあまり役に立ちません。

lemma myid2: "A==>A"
proof (rule invDed[where A=A and B=A])
  show "A ⟹ A ⟶ A"
    by (rule imp_refl)
  show "A ⟹ A"
    by assumption
qed

施設を回転させて (以下で[rotated]修飾子を使用して) を持っているA==>(A-->B)==>(B)場合は、次のように適用できますerule。

lemma myid2: "A==>A"
  apply (erule invDed[rotated])
  apply (rule imp_refl)
  done
于 2019-11-20T16:15:40.610 に答える