Advanced Logic

Table of Contents

Exercise 5

2b

Show validity of: [a*] ↔ φ ∧ [α][α*]φ

4

a

δ=while ¬p do bacR^¬p={(2,2),(3,3),(4,4)}R^ac=Ra;Rc={(1,2),(2,3),(4,3)};{(3,1)}={(2,1),(4,1)}Rbac=RbRac={(3,4),(3,2),(2,1)}{(2,1),(4,1)}={(3,4),(3,2),(2,1),(4,1)}R¬p;bac={(2,2),(3,3),(4,4)};{(3,4),(3,2),(2,1),(4,1)}={(2,1),(3,4),(3,2),(4,1)}R(¬p;bac):R¬p;bac0={(1,1),(2,2),(3,3),(4,4)}R¬p;bac1={(2,1),(3,4),(3,2),(4,1)}R¬p;bac2=R¬p;bac1{(3,1)}Rp={(1,1)}Rδ={(1,1),(2,1),(4,1),(3,1)}\begin{aligned} \delta &= \text{while $\lnot p$ do $b \cup ac$} \\ \hat{R}_{\lnot p} &= \{(2,2), (3,3), (4,4)\} \\ \hat{R}_{ac} &= R_{a}; R_{c} = \{(1,2), (2,3), (4,3)\}; \{(3,1)\} \\ &= \{(2,1), (4,1) \} \\ R_{b \cup ac} &= R_{b} \cup R_{ac} = \{(3,4), (3,2), (2,1) \} \cup \{(2,1), (4,1)\} \\ &= \{(3,4), (3,2), (2,1), (4,1)\} \\ R_{\lnot p; b \cup ac} &= \{ (2,2), (3,3), (4,4) \}; \{(3,4), (3,2), (2,1), (4,1) \} \\ &= \{(2,1), (3,4), (3,2), (4,1) \} \\ R_{(\lnot p; b \cup ac)*}: R_{\lnot p; b \cup ac}^{0} &= \{(1,1), (2,2), (3,3), (4,4) \} \\ R_{\lnot p; b \cup ac}^{1} &= \{(2,1), (3,4), (3,2), (4,1)\} \\ R_{\lnot p; b \cup ac}^{2} &= R_{\lnot p; b \cup ac}^{1} \cup \{(3,1)\} \\ R_{p} &= \{(1,1)\} \\ R_{\delta} &= \{(1,1), (2,1), (4,1), (3,1) \} \end{aligned}

b

M ?⊨ [δ]p → p