VRS - Transition Systems: Definition of universal predecessors/successors with sets in contrast to formulas equivalent?

Question

Hello,

the definition of universal predecessors in set theory is pre∀(Q) := {s1 ∈ S | suc(s1) ⊆ Q}, i.e. all states of S that have all their successors (if any) in Q. If a state has no successors it is also contained in pre∀(Q).
The definition of pre∀(Q) in propositional logic is the following, with φ being the formula that symbolically represents Q and R being the formula of the symbolic transition relation:
pre∀(φ) :⇔ ∀x1′ . . . xn′. R → old2new(φ)
(old2new(): substitutes state variables xi with next state variables xi').

In the set representation, also all states that have no successors are contained. But since those states have no outgoing transitions, they are not contained in R → old2new(φ) and therefore also not represented by pre∀(φ). Is that correct or have I done a mistake?

Best regards,
choehne

Comments

Thank you for your interesting question! One humble wish for the future: Could you possible use the tag “VRS”?

---

Thanks for letting me know! I fixed it in my past questions.

Answer 1

You have made a mistake: Look if a state x does not have outgoing transitions, then the transition relation R(x,x') is not satisfied for any assignment to x' if x is assigned with the values of the state in question. Hence, the implication R(x,x') →φ(x')  you mention is trivially true for that x and any x', and hence, that state x is in pre∀(φ).

So, both definitions are indeed equivalent to each other.

Comments

Thank you very much! I ran into the pitfall of implications, as I have done more than once before :-)

---

Yes, this "vacuous" satisfaction of implication is making us often trouble, but it is the only option to be consistent with most definitions. Bytheway, that is also a big trouble for specifications: It is easy to verify Phi->Psi for any system in case Phi is unsatisfiable, but it is meaningless.

---

In set theory, we can express ∀x∈X. … and  ∃x∈X. …. In quantified logic, there is a slight difference. There, we'd write ∃x. X(x) ∧ … and ∀x. X(x) → ….

---

Thanks to both of you for your advices!