如何阅读经典逻辑中的 P 蕴含 Q？

例子 ：

这是使用经典逻辑规则的模态逻辑。
KaX : a 知道 X 是真的。

我很好奇如何阅读英语的含义？如果然后呢？

编辑：在模态逻辑中，Ka 变成 Box，它是盒形符号，象征着必要性规则，规则 N，这意味着，盒子 P，如果你在世界 Delta 中有 P，那么所有可访问的世界也应该有 P。

还有钻石 P，意思是可能性，存在一个世界，它有从钻石 P 所拥有的世界可以访问的 P。

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

我会用

• ☐A 必须写 A
• ♢A 代表可能的 A

☐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允许对它们进行建模？）

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

• ☐(A->B)->(☐A->☐B)：

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

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

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

模态认知逻辑（又名知识逻辑）是否有任何（类似 SMT 的）求解器？

我需要一阶（不仅仅是命题）案例。

我在 Haskell 中编写了一些代码来建模命题逻辑

但是，由于数据类型是封闭的，因此没有自然的方法可以将其扩展到模态逻辑。因此，我认为我应该改用类。这样，我以后可以很容易地在不同的模块中添加新的语言特性。问题是我不完全知道如何写它。我想要类似下面的东西

错误当然在于连词的定义。但是，我不清楚如何重写它以使其工作。

我正在使用模态SAT求解器。不幸的是，这个求解器使用的是 Flex 和 Bison，这两种语言我都没有掌握......

我想将一种语法更改为另一种语法，但我遇到了一些问题，即使在关于 Flex-Lexer 和 Bison 的教程之后也是如此。

所以这里是问题：

我希望能够解析这样的模态逻辑公式：

在以前的符号中，这样的公式是这样写的：

(NOT (IMP (AND (ALL R0 (IMP C0 C1)) (ALL R0 C0)) (ALL R0 C1)))

这里是用于解析它们的 Flex/Bisons 文件：

alc.y

alc.lex

现在，让我们编写我们的示例，但使用我想使用的新语法：

阻碍我正确解析这种新语法的主要问题是：

• IMP (A B)现在写成~B | A（如在布尔逻辑中(A => B) <=> (~B v A)）。
• ALL RO现在写[r0]。
• SOME RO现在写<r0>。
• IFF (A B)现在写(~B | A) & (~A | B)。（IFF代表for if and only if）

这是新符号的小列表，即使我不知道如何解析它们：

我假设只有这两个文件会改变，因为它应该仍然能够通过使用其他 .y 和 .lex 编译源代码来读取以前的语法

但我要求您帮助确切地知道如何写下来：/

提前致谢 ！

所以这个问题与存储不同命题模态公式的列表有关。我能够删除重复项，但我不知道如何找到不一致的地方。例如：

初始列表列表：

上面的列表示例列表有一些问题我想简单地找到它们并打印出一条消息。例如，第一个列表有框 p 和否定框 p我希望它被检测到。它也没有 q 和 q。

同样，第二个列表没有(p or q) 和 (p or q)。任何人都可以提出解决此问题的方法，这可能很容易，但我似乎无法想到。

理想情况下，是否可以将子列表标记为已关闭？也许分配状态已关闭？

为简单起见，我们只考虑具有单个代理的 Kripke 结构，其知识由模态算子 K 描述。我们知道，在所有相应的 Kripke 结构中，K 由等价解释，任何公式 A 都成立

a) 公式 KA -> A（知识公理）有效，
b) 但公式 A -> KA 和 ¬KA 无效。

利用这些事实表明模态运算符 K 的这种行为不能由任何布尔函数编码（即，由表定义的真值）。

提示：假设可以使用 K 的真值表从 A 的真值计算 KA 的真值（与从 A 计算 ¬A 的方式相同）。考虑 K 的所有可能的真值表，并证明它们都不具有上述 a) 和 b) 的性质。

我不明白那个提示......制作K的真值表就像构建否定符号¬的真值表，在我看来这没有意义我认为只有对某事进行否定而不只是否定才有意义

据我了解，模态量词可能会放宽逻辑合取的行为：

我的问题是：它对其他操作（如独占析取、蕴涵和等价）有什么具体影响吗？这些例子怎么样（我自己想不通）：