Modal logic: Why is K5 determined by the class of all Euclidean frames?

Question

I am interested in proving that K, the smallest normal modal logic, in combination with the formula 5 (Possibly A then Necessarily Possibly A) is determined by the class of all Euclidean frames.

For the three maximally consistent sets G, B, and P, and the accessibility relation R, we can assume GRB and GRP and are interested in proving BRP. We can let Necessarily A be a member of B, in which case we're interested in showing that A is a member of P. Supposing this not to be the case, we have that Not A is a member of P. But then, by the accessibility relation R we should also have that Necessarily Not A is a member of G; in other words that Not Possibly A is a member of G. This, however, does not align with the proof I am trying to follow, which holds that we arrive at Possibly Not A as a member of G.

I'm not sure where I'm missing the mark and would appreciate any insight.

Answer 1

Let us unpack that wall of text.

You have 5: ◊p→□◊p as a theorem, and assume the frame {{G, B, P}, R} has R such that GRB and GRP. Further you are assuming B ╟ □A aiming to prove that entails P ╟ A , and so BRP must be. It looks like you are using an indirect proof (reduction to absurdity).

Ah, yes...

• Use the Frame of {{G, B, P}, R}
  • Assume GRB & GRP
    • Assume B ╟ □A
      • Assume P ╟ ~A
      • G ╟ ◊~A (via GRP)
      • G ╟ □◊~A (via theorem 5: ├ ◊A→□◊A )
      • B ╟ ◊~A (via GRB)
      • B ╟ ~□A (via duality)
      • Contradiction!
    • Therefore P ╟ A
  • Therefore BRP
• Therefore GRB & GRP → BRP