All geek questions in one place

Kripke semantics: educational software available?

I am stuck in the Kripke semantics and wonder if there is educational software through which I can check the equivalence of statements, etc., since Im start to think that it is easier to learn by example (even if using abstract variables).

I will use

  • ☐A must write A
  • ♢ A, possibly A

do ☐true, ☐false, ♢ true, ♢ false evaluate values, if so, what values ​​or types of values ​​from what is set ({true, false} or, perhaps, {necessary, possible))? [one]

I think I read all Kripke models using duality axiom :

(☐A) → (& not; ♢ & not; A)

i.e. if necessary for paytax , then it is not allowed not paytax
(no matter which one you need to pay tax ...)

ie2. if necessary for earnmoney , he is not allowed to not earnmoney
(again, no matter how you really need to make money, the logic still holds)

since A-> B is equivalent to & not; A <- & not; B allows you to test

& not; ☐A <- & ♢ no; A

there is no need for upvote if it is not allowed upvote

this axiom works twice:

♢ A → & not; & ☐ no; A

If it is allowed to earnmoney , then it does not need to not earnmoney

Not all modalities behave the same, and different Kripke models are more suitable for modeling one modalite than another: not all Kripke models use the same axioms . (Are classical quantifiers also modalities? If so, do Kripke models allow them to be simulated?)

I will go over to the list of general axioms and try to find examples that make it shown contradictory or unnecessary to postulate ...

  • ☐ (A-> B) → (☐A-> ☐B):

if (it is necessary that (earningmoney implies paytaxes)) then ((the need to generate income) implies (the need to pay taxes))

note that making money does not mean paying taxes, the falsity of the implication A-> B does not affect the value of the truth of the axiom ...

urgh its too long to talk about my problems trying to figure it all out ... feel free to edit

+4
source share
2 answers

I am not sure if there is educational software for teaching relational semantics for modal logic. However, I can try to answer some of the questions you asked.

First, modal operators act on judgments rather than true values ​​for necessity and opportunity. Therefore, if φ is a sentence, then both ☐φ and ♢ φ are sentences. Since neither true nor false are sentences, none of the “true,” “true,” “false,” and “false” are meaningful sequences of characters.

Secondly, what you call the "duality axiom" is usually an expression of the interdependence of modal operators. It can be introduced as an axiom in the axiomatic development of modal logic or obtained as a consequence of the semantics of modal operators.

Third, classical quantifiers are not modal operators and do not express modal concepts. In fact, modal logics are usually defined by introducing modal operators into propositional or predicate logic. I think your confusion arises from the fact that the semantics of modal operators are similar to the semantics of quantifiers. For example, the semantics of a necessity operator is similar to the semantics of a universal quantifier:

  • ⊧ ∀x.φ (x) ≡ φ (α) is true for all α in the quantization region
  • ⊧ w ☐φ ≡ φ is true in all possible worlds accessible from w

A similarity is observed when comparing the opportunity operator with the existence quantifier. In fact, modal operators can be defined as quantifiers over possible worlds. As far as I know, the opposite is not true.

+1
source

Source: https://habr.com/ru/post/1392405/

More articles:


All Articles