求解伊莎贝尔中的 ~(P /\ Q) |- Q -> ~P

Question

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

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

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

Answer 1

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

\n\n

至于上面的评论，你可能会问一个家庭作业问题，该评论是有效的，但如果你被否定所困惑，那么你基本上注定要失败，直到你取得进展，所以即使是一个完整的答案也不会帮不了你，而且这里没有正确的答案。

\n\n

这个公式是如此基本，除非通过应用分步规则，否则任何人都很难证明他们理解他们所证明的内容，而不经历大量繁琐的步骤。

\n\n

例如：

\n\n

lemma "~(P \xe2\x88\xa7 Q) ==> Q --> ~P"\n  by auto\n

\n\n

如果要求你表现出理解力，那么这肯定不会给你带来任何好处。

\n\n

我“通过随着时间的推移吸收的方法”取得了很大的进步，在他的回答中，M.Eberl 给出了自然演绎基础知识的重要概述。我对它的兴趣是闲逛，看看我是否能吸收更多一点。

\n\n

至于rule和erule，有备忘单：

\n\n

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

\n\n

至于通过伊莎贝尔（Isabelle）进行的逻辑证明，伊莎贝尔/HOL是如此庞大和复杂，以至于一次小小的帮助不会给你带来多大帮助，尽管总的来说，这一切都很重要。

\n\n

基本的逻辑等价

\n\n

我很久以前就学会了蕴涵的等价陈述。甚至在HOL.thy，第 998 行：

\n\n

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

\n\n

由此，很容易看出，连同 DeMorgon 定律（HOL.thy 的第 993 行），您在问题中陈述了等价性。

\n\n

嗯，当然，不完全是，这就是所有麻烦出现的地方。根据琐碎的等价重新排列事物，最终证明等价。（同时也知道符号的含义，例如您的|-意愿==>。我使用 ASCII 因为我不信任浏览器中的图形。）

\n\n

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

\n\n

lemma "~(P \xe2\x88\xa7 Q) ==> Q --> ~P"\nproof-\n  fix P Q :: bool\n  assume "~(P \xe2\x88\xa7 Q)"\n  hence "~P \xe2\x88\xa8 ~Q" by simp\n  hence "~Q \xe2\x88\xa8 ~P" by metis\n  thus "Q --> ~P" by metis\nqed\n

\n\n

我的家庭作业应该得到多少分？没什么。这实际上是metis知道如何使用基本一阶逻辑的见证。否则，它怎么知道要从 跳转~Q \xe2\x88\xa8 ~P到Q --> ~P？

\n