universal predecessor symbolically Exam Feb 2022 Q3d

Question

I have solved this question but my procedure is a little different is it correct?

Finally the answer is same sets {p} and {p,q}.

And how is universal predecessor changed to existential predecessor in the sample solution? Is it possible?

Answer 1

I don't understand you computation. I understand that you can replace the universal quantification on p' with only one of the cofactors, since the other one is trivial, but the same is not true for the second quantification on q'. If you don't like the example solution, then you probably want the following one:

    ∀p'. ∀q'. ( ((p↔q) ∨ (p'⊕q')) ∧ ((p↔q')∨(p'⊕q)) ) -> p'
    = ∀q'. ( ((p↔q) ∨ (0⊕q')) ∧ ((p↔q')∨(0⊕q)) ) -> 0
    = ∀q'. !( ((p↔q) ∨ q') ∧ ((p↔q')∨q) ) 
    = !( ((p↔q) ∨ 0) ∧ ((p↔0)∨q) ) 
    & !( ((p↔q) ∨ 1) ∧ ((p↔1)∨q) )
    = !( (p↔q) ∧ (!p∨q) ) 
    & !( 1 ∧ (p∨q) )
    = !((p↔q) ∧ (!p∨q)) & !(p∨q)
    = !((p↔q) ∧ (!p∨q)) & !p∧!q
    = !((0↔0) ∧ (!0∨0)) & !p∧!q
    = !(1 ∧ 1) & !p∧!q
    = !1 & !p∧!q
    = 0 & !p∧!q
    = 0

This time, the result is as given in the example solution, namely false. 

The change from universal to existential quantifiers is due to shifting the negation inside. Note that we have ¬ ∀x.phi = ∃x. ¬phi

Comments

how do you put p=0 and q=0 ??

---

That is due to page 69 of the Kripke structure chapter
φ ∧ x ⇔ [φ][x<-1] ∧ x and φ ∧ ¬ x ⇔ [φ][x<-0]