模态运算符可以定义为布尔函数吗？

Question

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

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

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

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

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

Answer 1

考虑所有可能的 K 真值表：

| A | K₁A | K₂A  | K₃A | K₄A |
—————————————————————————————
| 1 |  1  |  1  |  0  |  0  |
—————————————————————————————
| 0 |  1  |  0  |  1  |  0  |

表明它们都不授予上述 a) 和 b) 属性。

案例 1

| A | KA  | KA->A | A->KA | ¬KA |
—————————————————————————————————
| 1 |  1  |   1   |   1   |  0  |
—————————————————————————————————
| 0 |  1  |   0   |   1   |  0  |

在这种情况下，KA->A 不是重言式。

案例 2

| A | KA  | KA->A | A->KA | ¬KA |
—————————————————————————————————
| 1 |  1  |   1   |   1   |  0  |
—————————————————————————————————
| 0 |  0  |   1   |   1   |  1  |

在这种情况下，A->KA 是一个重言式。

案例 3

| A | KA  | KA->A | A->KA | ¬KA |
—————————————————————————————————
| 1 |  0  |   1   |   0   |  1  |
—————————————————————————————————
| 0 |  1  |   0   |   1   |  0  |

在这种情况下，KA->A 不是重言式。

案例 4

| A | KA  | KA->A | A->KA | ¬KA |
—————————————————————————————————
| 1 |  0  |   1   |   0   |  1  |
—————————————————————————————————
| 0 |  0  |   1   |   1   |  1  |

在这种情况下，¬KA 是一个重言式。

---

K 的期望行为可以用多值矩阵编码吗？

对于运动模态系统，答案如下：

• 3个值不足，
• 4 个值足以满足所谓的基本模态逻辑，
• 任何有限数量的值都不足以用于句法“完整”和演绎“自然”的模态系统。

见，例如。 g.，Jean-Yves Beseau 的 the article 中的介绍性部分。
我希望这些结果与认知模态系统相关。