在 Isabelle 中求解 ~(P /\ Q) |- Q -> ~P

Solve ~(P /\ Q) |- Q -> ~P in Isabelle

~(P /\ Q) |- Q -> ~P

我不知道从哪里开始。 否定让我困惑。

我必须在 Isabelle(一个程序)中解决这个问题,但如果有人解释如何使用自然演绎来解决,那将是足够的帮助。

假设你在谈论Isabelle/HOL,你可以使用像ruleeruleassumption这样的“单步战术”和基本的自然推演规则。您的命题可能需要的是:

  • 介绍规则notI,conjI,disjEimpI
  • 消除规则如notEconjEdisjEimpE
  • 销毁规则,例如 mp(先决条件)、conjunct1conjunct2

如果您想了解特定规则的含义,只需写下例如thm notI 伊莎贝尔将展示定理的陈述。

您可以设定一个目标,例如

lemma "¬(P ∧ Q) ⟹ Q ⟶ ¬P"

然后写例如

apply (rule impI)

应用蕴含的引入规则,使您拥有更新后的目标状态

goal (1 subgoal):
 1. ¬ (P ∧ Q) ⟹ Q ⟹ ¬ P

现在您找到下一个合适的规则并应用该规则,直到解决所有子目标。然后你可以写done,你的证明就完成了。

至于assumptionerule:如果你最终的目标有一些P需要证明并且P已经在假设中,你可以使用 apply assumption 来解决它。 (erule 类似于 ruleassumption 直接链接在它后面,通常便于应用消除规则)

但是,这种证明做起来很繁琐。更好的方法是使用 Isabelle 的结构化证明语言 Isar 进行整个证明。 Isar的介绍可以看Concrete Semantics.

的第5章

这是一个例子,SO 问题的质量很多时候是由答案决定的,而不是问题本身。我给出这个答案是为了感谢 M.Eberl 另一个有用的答案,因为我无法发表评论。

至于上面的评论,你可能在问作业问题,评论是有效的,但如果你被否定搞糊涂了,那么你基本上注定要失败,直到你取得进步,所以即使是一个完整的答案对您没有帮助,这里没有正确答案。

这个公式非常基础,除了通过应用循序渐进的规则,任何人都很难证明他们理解他们所证明的东西,而不是通过大量繁琐的步骤来做到这一点。

例如:

lemma "~(P ∧ Q) ==> Q --> ~P"
  by auto

如果要求您表现出理解,那肯定不会给您带来任何好处。

我在很大程度上取得了进步 "by the method of absorption over time",在他的回答中,M.Eberl 对自然演绎的基础知识进行了重要概述。我对它的兴趣是随便乱逛,看看能不能多吸收一点。

至于ruleerule,有作弊sheet:

http://www.phil.cmu.edu/~avigad/formal/FormalCheatSheet.pdf

至于 Isabelle 的逻辑证明,Isabelle/HOL 如此庞大和复杂,一点帮助,一次,对你没有多大帮助,但总的来说,这很重要。

基本的逻辑等价

我很久以前就学过一个蕴涵的等价语句。它甚至在 HOL.thy, line 998:

lemma disj_not2: "(P | ~Q) = (Q --> P)"

从那里,很容易看出,连同 DeMorgon 定律(HOL.thy 的第 993 行),您在问题中陈述了等价性。

嗯,当然,不完全是,这就是所有麻烦的来源。根据琐碎的等价性重新排列事物,最终证明等价性。 (同时也知道符号的含义,例如您的 |- 将是 ==>。我使用 ASCII,因为我不信任浏览器中的图形。)

M.Eberl 提到了结构化证明。考虑这个:

lemma "~(P ∧ Q) ==> Q --> ~P"
proof-
  fix P Q :: bool
  assume "~(P ∧ Q)"
  hence "~P ∨ ~Q" by simp
  hence "~Q ∨ ~P" by metis
  thus "Q --> ~P" by metis
qed

家庭作业我应该得到多少分?没什么。这实际上是 metis 知道如何使用基本的一阶逻辑的证明。否则,它怎么知道从 ~Q ∨ ~P 跳到 Q --> ~P

既然你明确提到了自然演绎。在自然演绎的特定风格中——行被编号并且假设的范围用方框明确标记(在下面用花括号表示)——证明你的陈述的一种方法如下:

1. ~(P & Q) premise
2. { Q       assumption
3.   { P     assumption
4.     P & Q and-introduction 3, 2
5.     _|_   negation-elimination 1, 4 }
6.   ~P      negation-introduction 3-5 }
7. Q -> ~P   implication-introduction 2-6

其实,既然你的目标是证明一个蕴涵,那么一开始你只有一个选择,即蕴涵引入。

将上述证明尽可能忠实地翻译成结构化 Isar 证明将是一个很好的练习(例如,使用所谓的 "raw proof blocks" 并且在 Isabelle 中顺便也用大括号表示)。

类似于 JIT 编译器,这是一个 LJEFAATGAA 答案(从另一个答案中学到足够的知识来给出答案)。

这是我学到的,而不是其他人可能学到的,这可能有助于其他人学习;伊莎贝尔的学习曲线相当残酷。我认为 OP 需要帮助的时间已经过去了。

  • 除了 M.Eberl 对 的回答,对于特定的 thm 为什么 rule thm 产生特定的目标状态对我来说仍然是个谜,以及为什么 rule thm 会生成消息 Failed to apply initial proof method.
  • 除非克里斯给出了精确的轮廓,加上规则和括号,否则我无法填写精确的细节。一个例子,如果一个人有时间学习,给他们一个部分的答案,让他们做一点工作,而不是给他们完整的答案。

两个主要驱动点

经过一些评论,我展示了大纲中的证明。它让我从必须解决细节中得到以下理解,在那里我说话好像我知道我是对的:

  1. apply(rule thm) 的使用应用于链式事实和目标陈述的组合,其中 this 在输出中显示一个或多个链式事实。
  2. 大括号开始和结束局部 context/scope。 context/scope 内部和外部的变量按照我们期望的方式工作,也就是说,范围在编程语言中正常工作。因此,如果我在证明的开头声明 fix P Q :: bool,然后在子上下文中声明 fix Q :: bool,子上下文中的 Q 指的是与父上下文不同的变量Q.

正确地注明了 Chris,我在此处插入他的大纲,以便可以轻松地将其与 Isar 来源进行比较:

1. ~(P & Q) premise
2. { Q       assumption
3.   { P     assumption
4.     P & Q and-introduction 3, 2
5.     _|_   negation-elimination 1, 4 }
6.   ~P      negation-introduction 3-5 }
7. Q -> ~P   implication-introduction 2-6

来源:

lemma "~(P & Q) ==> Q --> ~P"
proof-
  fix P Q :: bool
  assume a1: "~(P & Q)"
  { 
    assume a2: "Q"
    { 
      assume a3: "P"
      have a4: "P & Q" 
        apply(rule conjI) apply(rule a3) by(rule a2)
      (* NOTE: have to set 'notE' up right. Next 'hence False' doesn't do it. *)
      (* hence False apply(rule) by(metis a1) *)
      (* 'rule' applies the default of 'conjI', because there is the fact
         'this: P & Q', which comes from 'hence'; 'rule notE' gives an error.*)
      from a1 a4
      have False (* From 'this' and 'goal': ~(P & Q) ⟹ P & Q ==> False *)
        by(rule notE) (* notE: ~P ==> P ==> R *)
    }
    hence "~P" 
      apply(rule notI) by(assumption)
  }
  thus "Q --> ~P" 
    apply(rule impI) by(assumption)
qed

更好地理解作用域

我的陈述需要思考 have False。我没有为 notE 做好准备。只是为了看看我是否在正确的轨道上,我会执行 sledgehammer,但它无法在该上下文中证明 False

这是因为我处于自动驾驶状态,并且在两个本地上下文中使用 fix Q :: boolfix P :: bool。我把它们拿出来 sledgehammer 很容易找到证据。

这是一个人知道一些逻辑,但不知道如何用 Isabelle/HOL 和 Isabelle/Isar 语言正确实现逻辑的例子。

接下来,我必须学习如何正确设置 apply(rule notE)

强调一点

我对上述来源的部分理解来自于在 isar-ref.pdf 中看到短语 chained facts。对自然演绎规则的少量接触以及 M.Eberl 关于统一化、实例化和解析的解释最终有助于理解输出面板中发生的事情。

上面我把hence False注释掉了,然后用have False。幸运的是,在 Isabelle 中,有多种方法可以做事,但目标是应用 notE。尽管如此,仍有不同的 Isar 关键字可用于设置。

无论如何,看到链式事实如何与 rule 一起使用是一个灵光一现的时刻。我想这实际上是声明 have False 所涉及的内容,因为它与 notE:

相关
term "~P ==> P ==> R" (* notE: line 376 of HOL.thy *)

lemma "~(P & Q) ⟹ P & Q ==> False"
  by(rule notE)

如果我有一个帐户,我会投票解决这个问题以摆脱 -1。

感谢 Chris 给出了准确的轮廓。