使用 SML 和 HOL 推理规则从第一原理证明定理

我正在尝试证明这个定理[] |- p /\ q <=> q /\ p :thm将 SML 与 HOL 推理规则结合使用。这是 SML 代码：

val thm1 = ASSUME ``p:bool /\ q:bool``;
val thm2 = ASSUME ``p:bool``;
val thm3 = ASSUME ``q:bool``;
val thm4 = CONJ thm2 thm3;
val thm5 = CONJ thm3 thm2;
val thm6 = DISCH ``(q:bool/\p:bool)`` thm4;
val thm7 = DISCH ``(p:bool/\q:bool)`` thm5;
val thm8 = IMP_ANTISYM_RULE thm6 thm7;

上述代码的结果是：

val thm8 =  [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) <=> p /\ q: thm

我究竟做错了什么？

你的最终定理的问题是你仍然有p and q作为假设，通过引入thm2 and thm3，而你可以而且应该从thm1.

你需要的第一个定理是这样的p /\ q ==> p。我通过浏览找到了合适的规则描述 http://sourceforge.net/projects/hol/files/hol/kananaskis-11/kananaskis-11-description.pdf/download（第 2.3.24 节）。它被称为CONJUNCT1.

使用它，我们可以得到p作为定理thm1:

val thmp = CONJUNCT1 thm1;

同样的想法可以得到q作为定理thm1:

val thmq = CONJUNCT2 thm1;

然后你可以将你的想法应用到thm5:

val thm5 = CONJ thmq thmp;

The 重要的事情这是我们不使用的p源自p (thm2) and q源自q (thm3） 反而p源自p /\ q and q源自p /\ q（环境show_assumes := true;可能有助于更清楚地看到这一点）。

最后，我们将您的想法应用到thm7:

val thm7 = DISCH ``p /\ q`` thm5;

获得所需结果的前半部分，但没有任何无关的假设。

后半部分以类似的方式获得：

val thm9 = ASSUME (``q /\ p``);
val thmp2 = CONJUNCT2 thm9;
val thmq2 = CONJUNCT1 thm9;
val thm6 =  DISCH ``q /\ p`` (CONJ thmp2 thmq2);

然后你的想法thm8完美运行：

val thm8 = IMP_ANTISYM_RULE thm7 thm6;