Isabelle中基于A⇒B证明¬A⇒¬B及双向等价性的通用方法咨询

场景1：从A⇒B推导¬A⇒¬B的注意事项与可行方案 #

首先明确：纯命题逻辑中，A⇒B无法直接推导出¬A⇒¬B，这是典型的否定前件谬误——比如A为“x是猫”、B为“x是动物”时，A⇒B成立，但¬A⇒¬B显然不成立。只有在补充额外前提（如B⇒A，即A、B等价）时，该推导才成立。

如果你实际想推导的是A⇒B的逆否命题¬B⇒¬A（这是逻辑等价式，必然成立），以下是Isabelle中用基础证明方法的实现：

用apply战术的简洁证明 #

lemma "A ⟶ B ⟹ ¬B ⟶ ¬A"
  apply (rule impI)       (* 引入蕴含前提：假设¬B *)
  apply (rule notI)       (* 引入否定结论：假设A，目标导出矛盾 *)
  apply (drule mp)        (* 用A⇒B和假设A推导出B *)
  apply (rule notE)       (* 用¬B和B导出矛盾 *)
  apply assumption
  done

结构化Isar证明（更易读） #

lemma "A ⟶ B ⟹ ¬B ⟶ ¬A"
proof
  assume nb: ¬B
  show ¬A
  proof
    assume a: A
    from a and `A ⟶ B` have b: B by (rule mp)
    from nb and b show False by (rule notE)
  qed
qed

若你确实需要推导¬A⇒¬B，必须补充B⇒A作为前提，示例：

lemma "A ⟶ B ⟹ B ⟶ A ⟹ ¬A ⟶ ¬B"
  apply (rule impI)
  apply (rule notI)
  apply (drule mp)
  apply (drule mp)
  apply assumption+
  done

场景2：证明A与B等价时，完成B⇒A的反向推导 #

A与B等价的定义是(A⇒B) ∧ (B⇒A)，你已证得A⇒B，反向推导B⇒A的通用思路如下：

1. 从等价定义或结构入手
   如果A、B的等价是基于定义（如A是¬¬P、B是P），直接展开定义，用重写规则替换。比如利用Isabelle内置的not_not_eq规则完成双重否定的推导。

2. 反证法与逆否命题结合
   经典逻辑中，反证法是推导反向蕴含的常用技巧：假设¬A，结合已证的A⇒B导出¬B，再与假设B矛盾，从而证明A。示例Isar证明：

   (* 假设你已证得A⇒B *)
   lemma AB: "A ⟶ B" by ... (* 你的证明步骤 *)
   
   lemma BA: "B ⟶ A"
   proof
     assume b: B
     show A
     proof (rule classical)  (* 启用经典逻辑反证 *)
       assume na: ¬A
       from na and AB have nb: ¬B by (rule contrapos_pp)  (* 调用逆否引理 *)
       from b and nb show False by (rule notE)
     qed
   qed
   
   (* 最终等价性证明 *)
   lemma A_iff_B: "A ⇔ B"
     by (rule iffI) (rule AB, rule BA)
   

3. 基础战术的分步调试

   • 先用apply auto快速验证是否存在自动可证路径，若可行再拆解为基础步骤；
   • 用apply (rule impI)引入B作为假设，将目标简化为证明A；
   • 根据A的结构选择对应规则：A是合取式用conjI，析取式用disjI1/disjI2，否定式用notI；
   • 用drule mp调用已证的A⇒B引理，结合当前假设推导中间结论。

4. 检查前提与形式化正确性
   如果始终推不出，需核对：是否遗漏了题目隐含的前提？A、B的形式化是否与题目描述一致？比如是否误将蕴含写成了合取，或颠倒了命题的结构。

内容的提问来源于stack exchange，提问作者user22346194