I am studying modal logic with the textbook 'Reasoning about Knowledge' Fagin et al. 1995
The positive introspection axiom is taken as something that can be proved with the possible worlds model of knowledge and the assumption that the possibility relation of agents are equivalence relations. Below I have attached the proof of positive introspection presented in the textbook:
Here is the theorem statement presented in the textbook:
Here is the textbooks proof of the theorem statement (with the assumption that $\mathcal{K_i}$ is an equivalence relation)
The aim is to prove that $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$
The book seems to instead prove that $ (M,s) \vDash K_i\phi \Rightarrow (M,s) \vDash K_iK_i\phi$ by assuming the possibility relation $\mathcal{K_i}$ is an equivalence relation.
I believe both $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$ and $ (M,s) \vDash K_i\phi \Rightarrow (M,s) \vDash K_iK_i\phi$ are subtly different theorems, although I agree that what the book proved (with the additional assumption that $\mathcal{K_i}$ is an equivalence relation) implies $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$ anyway, but not the other way around, and is thus stronger than $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$, I think that $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$ can be proved directly without the need to assume that $\mathcal{K_i}$ is an equivalence relation, and I think in this sense, the book has done something unnecessary.
Here is my proof of $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$ without the assumption that $\mathcal{K_i}$ is an equivalence relation.
Proof:
Since $M \vDash K_i\phi$, we know that $(M,s) \vDash K_i\phi, \forall s \in S$ where $S$ is a set of possible worlds or states in the Kripke structure $M$.
Thus, we have, for any state $s \in S$, $(M,u) \vDash K_i\phi$ for all $u \in S$ such that $(s,u) \in \mathcal{K_i}$, and therefore, by definition, $(M,s) \vDash K_iK_i\phi$.
Since this is true of arbitrary $s \in S$, we know that $(M,s) \vDash K_iK_i\phi$ for all $s \in S$, and so $M \vDash K_iK_i\phi$
I would like to know if what I have said here is accurate, and would also appreciate it if someone could help me understand better what $K_iK_i\phi$ on its own is supposed to mean, as in the theorem statement of the positive introspection axiom presented in the book, it is written: $M \vDash K_i\phi \Rightarrow K_iK_i\phi$ which I took to mean $M \vDash K_i\phi \Rightarrow M \vDash K_iK_i\phi$, however it seems the book has taken this to mean $(M,s) \vDash K_i\phi \Rightarrow (M,s) \vDash K_iK_i\phi$, which is stronger than my interpretation of the statement and required $\mathcal{K_i}$ to be an equivalence relation to prove.
I would appreciate it if someone could help clear up this issue, thank you.
EDIT: I kept saying the books interpretation requires $\mathcal{K_i}$ to be an equivalence relation, more accurately, I should have said the book requires $\mathcal{K_i}$ to be transitive.
Probably, they should have added at the end of the proof something like 'since $s, t, u$ were arbitrary, the result holds generally for any states.' In other words, they showed that positive introspection is valid on a class of transitive (and hence equivalence) frames. Positive introspection (axiom 4 in usual setting) means that if an agent knows something, then she is aware of her knowledge. This leads (with especially negative introspection) to quite an idealized notion of an agent that is logically omniscient (there is a chapter on the problem in Fagin et al.). In the book, positive introspection is valid on any transitive frame, i.e. true in all states of all models built on transitive frames. You are right in assuming that equivalence is not necessary for the aforementioned proof, but the authors intend to present a model for knowledge, which is usually assumed to be $S\mathbf{5}$. Sorry for a woolly answer.