logic - Kripke 语义：学习软件可用吗？

Question

我被困在Kripke 语义上，想知道是否可以educational software通过它测试语句的等价性等，因为我开始认为它更容易通过示例来学习（即使是在抽象变量上）。

我会用

☐true, ☐false, ♢true, ♢false 是否评估为值，如果是，则来自什么集合（{true, false} 或 {necessary,possibly}）的哪些值或类型的值？[1]

我想我读过所有Kripke models使用的duality axiom：

(☐A)->(¬♢¬A)

即如果有必要，paytax那么它不允许不paytax
（不管它是否有必要纳税......）

即2。如果有必要，则earnmoney不允许earnmoney
（同样，不管赚钱是否真的有必要，到目前为止，逻辑仍然成立）

因为 A->B 等价于 ¬A<-¬B 让我们测试

¬☐A<-♢¬A

upvote如果允许，则没有必要upvote

这个公理具有双重作用：

♢A->¬☐¬A

如果它允许，earnmoney那么它没有必要不earnmoney

并非所有模态的行为都相同，并且不同Kripke model的模态比另一种更适合模拟一种模态：并非所有模态都Kripke models使用相同的axioms. （经典量词也是模态吗？如果是的话，是否Kripke models允许对它们进行建模？）

我将浏览常见公理列表，并尝试找到使假设看起来违反直觉或不必要的示例……

if (它有必要 (earningmoney 意味着要交税)) 那么 ((necessity of Earningmoney) 意味着 (necessity of paidtax))

请注意，赚钱并不意味着纳税，暗示 A->B 的错误并不影响公理的真值...

呃，它花了太长时间来表达我试图理解这一切的问题......随时编辑

score 5 · Accepted Answer

模态逻辑证明者和推理者：

Java中的引擎画面：

模态逻辑计算器：

认知逻辑的实际游戏实现讲座：

非常好的博士论文：

关于模态逻辑的讲座（在行动、冲突、游戏中）：

关于模态逻辑和一般逻辑的视频讲座：

score 1 · Accepted Answer

我不确定是否存在用于教授模态逻辑的关系语义的教育软件。但是，我可以尝试回答您提出的一些问题。

首先，必要性和可能性的模态运算符对命题而不是真值进行操作。因此，如果 φ 是一个命题，那么 ☐φ 和 ♢φ 都是命题。因为真假都不是命题，所以 ☐ true、♢true、☐false 和 ♢false 都不是有意义的符号序列。

其次，您所说的“对偶公理”通常是模态运算符的可互定义性的表达。它可以在模态逻辑的公理化发展中作为公理引入，也可以作为模态运算符语义的结果而导出。

第三，经典量词不是模态运算符，也不表达模态概念。事实上，模态逻辑通常是通过将模态运算符引入命题或谓词逻辑来定义的。我认为你的困惑是因为模态运算符的语义看起来类似于量词的语义。例如，必要性运算符的语义看起来类似于全称量词的语义：

将可能性算子与存在量词进行比较时，可以看到相似之处。事实上，模态运算符可以定义为可能世界上的量词。据我所知，反之亦然。

2 回答 2