lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

index.md (1184B)

      1 +++
      2 title = 'Standard translation: mapping basic modal logic to first-order predicate logic'
      3 +++
      4 # Standard translation: mapping basic modal logic to first-order predicate logic
      5 Aim to map formulas of basic modal logic to first-order predicate logic such that:
      6 - φ in BML is *valid* iff its translation in first-order predicate logic is *valid*
      7 - φ in BML is *satisfiable* iff its translation in first-order predicate logic is *satisfiable*
      8 
      9 Translation:
     10 - translate "p is true in world x" as "predicate P holds for x"
     11 - translate "accessibility relation R" as "binary predicate R"
     12 - translation is relative to some state
     13 - notation: Px instead of P(x), Rxy instead of R(x,y)
     14 
     15 Rules for standard translation:
     16 
     17 ![Standard translation rules](standard-translation-rules.png)
     18 
     19 Examples of translation:
     20 
     21 ![Standard translation examples](standard-translation-examples.png)
     22 
     23 first-order predicate logic is decidable _if it uses at most 2 variables_.
     24 therefore, adapt standard translation to only use 2 variables.
     25 
     26 In a formula, check the situation with bound variables, and rename where possible.
     27 When you are in state _a_ and start a quantification, use the variable _b_, and vice versa.