Z3验证Lewis Carroll谓词逻辑推理失败问题咨询

问题描述 #

用户尝试通过断言前提合取蕴含结论的否定来验证重言式，即验证前提集合与结论否定是否矛盾，预期返回unsat，但实际返回sat。相关逻辑与代码如下：

逻辑命题 #

• 所有不贪婪的兔子都是黑色的
• 没有老兔子不贪婪（即所有老兔子都贪婪）
• 结论：有些黑兔子不是老的

验证代码 #

; All rabbits, that are not greedy, are black
; No old rabbits are free from greediness
; Therefore: Some black rabbits are not old
(declare-sort U) 
(declare-fun g (U) Bool)
(declare-fun b (U) Bool)
(declare-fun o (U) Bool) 
(assert (forall ((x U)) (=> (not (g x)) (b x) ))) 
(assert (forall ((x U)) (=> (o x) (g x) ))) 
(assert (not (exists ((x U)) (and (b x) (not (o x))))))
(check-sat)
; returns sat

原因解释 #

核心问题在于论域U可能为空集合：

• 全称量词命题（如前提中的两个forall）在空论域下是空洞真（vacuously true）——因为没有元素违反命题，所以前提全部成立。
• 结论的否定not (exists x (b x ∧ ¬o x))等价于forall x (¬b x ∨ o x)，这个全称命题在空论域下同样是空洞真。
• 当U为空时，前提和结论否定同时成立，整个断言集合可满足，因此求解器返回sat。

若要得到预期的unsat结果，需添加论域非空的前提，比如断言存在至少一个元素：

(assert (exists ((x U)) true))

添加后执行(check-sat)，将返回unsat，符合逻辑矛盾的预期。

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