Kripke semantics: learning software available?

问题:

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

回答1:

Modal logic provers and reasoners:

1. http://www.cs.man.ac.uk/~schmidt/tools/
2. http://www.cs.man.ac.uk/~sattler/reasoners.html

Engine tableau in Java:

1. http://www.irisa.fr/prive/fschwarz/lotrecscheme/
2. https://github.com/gertvv/oops/wiki
3. http://molle.sourceforge.net/

Modal logic calculators:

1. http://staff.science.uva.nl/~jaspars/lvi98/Week3/modal.html
2. http://www.ffst.hr/~logika/implog/doku.php?id=program:possible_worlds
3. http://www.personeel.unimaas.nl/roos/EpLogic/start.htm

Lectures for practical game implementations of epistemic logic:

1. http://www.ai.rug.nl/mas/

Very good phd thesis:

1. http://www.cs.man.ac.uk/~schmidt/mltp/
2. http://www.harrenstein.nl/Publications.dir/Harrenstein.pdf.gz

Lectures about modal logic (in action, conflict, games):

1. http://www.logicinaction.org/
2. http://www.masfoundations.org/download.html
3. Modal Logic for Open Minds, http://logicandgames.pbworks.com/f/mlbook-almostfinal.pdf (the final version is not free)

Video lectures about modal logic and logic in general:

1. http://videolectures.net/ssll09_gore_iml/
2. http://videolectures.net/esslli2011_benthem_logic/
3. http://videolectures.net/esslli2011_jaspars_logic/
4. http://www.youtube.com/view_play_list?p=C88812FFE0F526B0

回答2:

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:

• ⊧ ∀x.φ(x) ≡ φ(α) is true for all α in the domain of quantification
• ⊧_w ☐φ ≡ φ is true in every possible world accessible from w

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.