我们确定不可能以天真的方式将序列嵌入到分离逻辑中吗？
在 PLCC 的第 100 页上，它指出 ifP [|-] Q意味着“适用于所有世界w，如果w |= P那么w |= Q，那是行不通的，因为它无法证明(P [|-] Q) |-- |> (P [|-] Q)。
我不明白为什么嵌入它!!(P |-- Q)不起作用，特别是因为证明这一点很简单，而且证明起来也
!!(P |-- Q) |-- |> !!(P |-- Q)没有那么难
!!(P |-- Q) |-- !!(|> P |-- |> Q)。