[SOLVED] Kripke semantics: learning software available?

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

Solution