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 (2313B)

      1 +++
      2 title = 'Formula validity using sequents and tableaux'
      3 +++
      4 # Formula validity using sequents and tableaux
      5 Sequents and tableaux are two ways to determine validity of formulas.
      6 Tableaux also conveniently provide a countermodel if a formula is not valid.
      7 
      8 Some examples in [exercise class 3](../exercise-3/#sequents-and-tableaux-exercise-5).
      9 
     10 ## Sequents
     11 φ₁...φn ⇒ ψ₁...ψm valid if in every model, in every world in that model, the conjunction of the φᵢ implies the disjunction of the ψᵢ.
     12 
     13 Empty conjunction is true, empty disjunction is false.
     14 
     15 Reducing modal sequents:
     16 
     17 ![Reducing modal sequents rules](reducing-modal-sequents.png)
     18 
     19 φ valid iff the sequent (⇒ φ) valid.
     20 
     21 For modal logic:
     22 - If we get a sequent of the form p₁...n, ◇φ₁..◇φm ⇒ q₁..qk, ◇ψ₁...◇ψl
     23 - Such a sequent only valid iff either pᵢ = qj for some i and j, or φᵢ ⇒ ψ₁...ψl is valid for some i ∈ {1...m}
     24 
     25 A sequent _closes_ if the conjunction of the left side implies a disjunction of the right side.
     26 That is, φ₁ ∧ ... ∧ φᵤ ⇒ ψ₁ ∨ ... ∨ ψᵥ.
     27 So if _any_ of the formulas on the left appear on the right.
     28 
     29 Start with intended conclusion, try to build a proof while moving upwards.
     30 Formula is valid iff it is derivable in sequent calculus.
     31 Validity using sequents:
     32 1. Rewrite formula
     33     - (a → b) to (¬ a ∨ b)
     34     - (¬ □ a) to (◇ ¬ a)
     35     - (□ a) to (¬ ◇ ¬ a)
     36 
     37 2. Rewrite sequent, based on rules above
     38 3. Maybe rewrite formula again
     39 4. Decide on validity of sequent
     40 5. Conclude on validity of formula
     41 
     42 ## Tableaux
     43 Tableau is finite tree of sequents.
     44 If all solid branches close, yields validity of initial sequent.
     45 If at least one branch does not close, yields a counterexample.
     46 
     47 The dot separates assumptions on the left from what's true on the right.
     48 "Closing" is the same as for sequents.
     49 
     50 ![Tableau rules](tableau-rules.png)
     51 
     52 In modal logic:
     53 
     54 ![Tableau modal logic](tableau-modal-logic.png)
     55 
     56 ### Example
     57 
     58 ![Example](example-tableau.png)
     59 
     60 It's not valid because in the two red states, the letters on the left of the dot are not on the right.
     61 The countermodel comes from taking the numbers next to each step (the numbers are states), connecting them, and creating a valuation where the letters on the left side of the dot (the assumptions) are true.