命题逻辑的格区分答案

【问题标题】：Case distinction for propositional logic命题逻辑的格区分
【发布时间】：2015-07-28 13:35:30
【问题描述】：

我想证明

P ==> P

按大小写，理解后者。

lemma "P ⟹ P"
proof (cases P)

goal (2 subgoals):
1. P ⟹ P ⟹ P
2. P ⟹ ¬ P ⟹ P

我不太确定我是否想要这些。我想假设 P 是真的，然后通过假设证明 P 是真的，然后假设不是 P 并通过假设证明不是 P。就像在真值表中一样。

第二个子目标中的非 P 看起来很奇怪，这是否可以证明？

 assume P then show P by assumption

 Successful attempt to solve goal by exported rule:
 (P) ⟹ P 

next

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

 assume P assume "¬P" then show "¬P" by (rule HOL.FalseE)

这很糟糕。

如何以 P 而不是 P 为案例？

【问题讨论】：

P ==> ~P ==> Q 总是正确的，因为假设是矛盾的。

标签： logic isabelle

【解决方案1】：

P 而不是 P 已经是你的情况。如果你写“案例 P”，Isabelle 复制当前目标并将 P 添加到第一个新子目标的假设中，并将 - P 添加到第二个新子目标的假设中。如果以这种方式使用，则目标的右侧不受 case 方法的影响。

在您的案例中，您不必证明第二个子目标中的 ¬ P，但您可以将其用作案例目标引入的附加假设。

显然，您无法在第二个子目标中从 ¬ P 证明 P。幸运的是，全局假设 P 仍然存在，因此两种情况仍然可以从 P 中证明 P，这在没有案例的情况下已经很简单了；）。

如果您想通过让 Isabelle 直接插入变量的可能值来证明某事，您可以尝试：

  lemma "P ⟹ P"
  proof (induct P) 

  goal (2 subgoals):
  1. True ⟹ True
  2. False ⟹ False

【讨论】：