This post is regarding the proof of Theorem 3.1.5 in Reasoning about Knowledge, by Fagin, Halpern, Moses, & Vardi.
In particular, it was mentioned without proof (for part (c) of the theorem, in case you wish to refer), that the Axiom $\mathbf 5$ or $A5$ corresponds to a Euclidean possibility relation. Axiom $\mathbf 5$ is given by: $$\lnot K_i\varphi \to K_i\lnot K_i\varphi$$
So, I'm trying to prove that A5 is valid in all Euclidean structures, i.e. structures $M = (S,\pi, R_1,\ldots,R_k)$ where the relations $R_i$ are Euclidean.
Let $M$ be a Euclidean structure (for $n$ agents, labeled $1$ to $n$). We want to show $M\vDash\lnot K_i\varphi \to K_i\lnot K_i\varphi$. This is the same as showing $M\vDash \lnot K_i\lnot K_i\varphi \to K_i\varphi$. Suppose for some $s\in S$, $(M,s)\vDash \lnot K_i\lnot K_i\varphi$. Then there exists some state $t$ such that $(s,t)\in R_i$ and $(M,t)\vDash \lnot\lnot K_i\varphi$, which is just $(M,t)\vDash K_i\varphi$. Then for all states $u$ such that $(t,u)\in R_i$, we have $(M,u)\vDash \varphi$.
So far I haven't used the fact that the $R_i$'s are Euclidean, i.e. if $(x,y)\in R_i$ and $(x,z)\in R_i$ then $(y,z)\in R_i$. Unfortunately, I don't know where to use it.
Could someone please help me show $(M,s)\vDash K_i\varphi$ in order to complete the proof? Please let me know if you've any other way to approach this too.
If any notation needs clarification, please ask in the comments and I shall clarify here.
You have a state $t$ such that $(s,t)\in R_i$ and for all $u$ such that $(t,u)\in R_i$, $(M,u)\models\varphi$. You want to show that $(M,s)\models K_i\varphi$. That is, you want to show that for any $u$ such that $(s,u)\in R_i$, $(M,u)\models\varphi$. But now since $R_i$ is Euclidean, if $(s,u)\in R_i$ then $(t,u)\in R_i$ since $(s,t)\in R_i$. So, you do have $(M,u)\models\varphi$, as desired.
I think the argument is a bit more intuitive if you formulate it directly. Suppose I (the agent) don't know $\varphi$. That means I can imagine some world $u$ in which $\varphi$ is false (where "imagine" refers to my relation $R_i$). Now since my imagination is Euclidean, for any other world $t$ that I can imagine, I could imagine $u$ from $t$. So, in the world $t$, I would still not know $\varphi$. Thus from every world $t$ that I can imagine, I don't know $\varphi$. That is, I know that I don't know $\varphi$.