Kripke语义：学习软件可用吗？
我陷入了Kripke 语义，想知道是否有教育软件通过它我可以测试语句的等价性等，因为我开始认为通过示例学习更容易（即使在抽象变量上）。
我将使用
- ☐A 来写必然 A
- ♢A ，可能 A
做 burytrue, □false, ♢true, ♢false 评估值，如果是的话，来自哪个集合的值或类型值（{true, false} 或可能 {有必要，可能}）？ [1]
我想我读过所有Kripke模型都使用对偶公理：
(ăA)->(Ø♢ØA)，
即如果有必要的话paytax 那么就不允许不paytax
（不管是否需要缴税...）
ie2。如果有必要赚钱，则不允许不赚钱
（同样，无论赚钱是否真的有必要，到目前为止，逻辑仍然成立）
因为 A->B 相当于 ØA<-ØB 让我们测试
ØTreeA<-♢ØA
它没有必要 赞成如果允许不赞成赞成
这个公理具有双重作用：
♢A->НЛA
如果允许earnmoney 那么没有必要不 earnmoney
并非所有模态的行为都相同，不同的 Kripke 模型 比另一种模态更适合建模一种模态：并非所有Kripke 模型都使用相同的公理。 （经典量词也是模态吗？如果是的话，Kripke 模型允许对它们进行建模吗？）
我将浏览常见公理列表，并尝试找到一些例子，使其看起来违反直觉或没有必要假设......
- （A->B）->（A->B）：
如果（有必要（赚钱意味着纳税）） 那么 ((挣钱的必要性) 意味着 (缴税的必要性))
请注意，挣钱并不意味着缴税，蕴涵 A->B 的虚假性并不影响该公理的真值……
呃，它也采用了很长一段时间来表达我在试图理解这一切时遇到的问题......请随意编辑
I am stuck on Kripke semantics, and wonder if there is educational software through which I can test equivalence of statements etc, since Im starting to think its easier to learn by example (even if on abstract variables).
I will use
- ☐A to write necessarily A
- ♢A for possibly A
do ☐true, ☐false, ♢true, ♢false evaluate to values, if so what values or kinds of values from what set ({true, false} or perhaps {necessary,possibly})? [1]
I think I read all Kripke models use the duality axiom:
(☐A)->(¬♢¬A)
i.e. if its necessary to paytax then its not allowed to not paytax
(irrespective of wheither its necessary to pay tax...)
i.e.2. if its necessary to earnmoney its not allowed to not earnmoney
(again irrespective of wheither earning money is really necessary, the logic holds, so far)
since A->B is equivalent to ¬A<-¬B lets test
¬☐A<-♢¬A
its not necessary to upvote if its allowed to not upvote
this axiom works dually:
♢A->¬☐¬A
If its allowed to earnmoney then its not necessary to not earnmoney
Not all modalities behave the same, and different Kripke model are more suitable to model one modalit than another: not all Kripke models use the same axioms. (Are classical quantifiers also modalities? if so do Kripke models allow modeling them?)
I will go through the list of common axioms and try to find examples that make it seem counterintuitive or unnecessary to postulate...
- ☐(A->B)->(☐A->☐B):
if (its necessary that (earningmoney implies payingtaxes))
then ((necessity of earningmoney) implies (necessity of payingtaxes))
note that earning money does not imply paying taxes, the falsehood of the implication A->B does not affect the truth value of the axiom...
urgh its taking too long to phrase my problems in trying to understand it all... feel free to edit
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
模态逻辑证明器和推理器：
Java 中的引擎画面：
模态逻辑计算器：
实际游戏讲座认知逻辑的实现：
非常好的博士论文：
关于模态逻辑的讲座（行动、冲突、游戏）：
有关模态逻辑和一般逻辑的视频讲座：
Modal logic provers and reasoners:
Engine tableau in Java:
Modal logic calculators:
Lectures for practical game implementations of epistemic logic:
Very good phd thesis:
Lectures about modal logic (in action, conflict, games):
Video lectures about modal logic and logic in general:
我不确定是否存在用于教授模态逻辑关系语义的教育软件。不过，我可以尝试回答您提出的一些问题。
首先，必然性和可能性的模态运算符根据命题而不是真值进行操作。因此，如果 φ 是一个命题，那么 ψ 和 ♢φ 都是命题。因为 true 和 false 都不是命题，所以 burytrue, ♢true, buryfalse< /em> 和 ♢false 是有意义的符号序列。
其次，你所说的“对偶公理”通常是模态运算符的可相互定义性的表达。它可以作为模态逻辑的公理化发展中的公理引入，或者作为模态运算符的语义的结果而导出。
第三，经典量词不是模态运算符，不表达模态概念。事实上，模态逻辑通常是通过将模态运算符引入命题或谓词逻辑来定义的。我认为您会感到困惑，因为模态运算符的语义看起来与量词的语义相似。例如，必然性算子的语义与全称量词的语义相似：
将可能性算子与存在量词进行比较时，可以看到相似之处。事实上，模态运算符可以定义为可能世界的量词。据我所知，事实并非如此。
I'm not sure whether educational software for teaching relational semantics for modal logics exists. However, I can attempt to answer some of the questions you have asked.
First, the modal operators for necessity and possibility operate on propositions, not truth values. Hence, if φ is a proposition then both ☐φ and ♢φ are propositions. Because neither true nor false are propositions, none of ☐true, ♢true, ☐false, and ♢false are meaningful sequences of symbols.
Second, what you refer to as the "duality axiom" is usually the expression of the interdefinability of the modal operators. It can be introduced as an axiom in an axiomatic development of modal logic or derived as a consequence of the semantics of the modal operators.
Third, the classical quantifiers are not modal operators and don't express modal concepts. In fact, modal logics are generally defined by introducing the modal operators into either propositional or predicate logics. I think your confusion arises because the semantics of modal operators appears similar to the semantics of quantifiers. For instance, the semantics of the necessity operator appears similar to the semantics of the universal quantifier:
A similarity is seen when comparing the possibility operator with the existential quantifier. In fact, the modal operators can be defined as quantifiers over possible worlds. As far as I know, the converse isn't true.