I'm looking for some guidance in defining a new epistemic, temporal logic.
I am looking to extend a logic called Sequential Epistemic Logic (SPAL): https://pdfs.semanticscholar.org/dae6/739b8b05bf2845f2de41611c3cd0c9ae03d5.pdf (p14)
In SPAL we define sequential models using time index $t$. A model $M$ includes set of worlds $W$, an valuation function $V$ on a set of propositions $PROP$ and a relation sequence $\sigma = \langle R_0, R_1,. . . R_t \rangle$ where $R_i$ is the 'epistemic relation' on $W$ at time $i$. For now we just note that there is a way to get from $R_{i}$ to $R_{i+1}$, and in general to move from one relation another.
This relation is important because we need to define Knowledge (K) in world $w$ at a certain time as $M, w, t, \sigma \models K \varphi$ iff $\forall v$ such that $w R_t v, M,v,t, \sigma \models \varphi$.
Importantly in SPAL is the ability to refer to different times using operators such as X (next epistemic time) or Y (previous epistemic time):
1) $M,w,t,\sigma \models X \varphi$ iff $M,w,t+1, \sigma \models \varphi$
2) $M,w,t, \sigma \models Y \varphi$ iff t= 0 or $M,w,t-1 \sigma \models \varphi$
The main concern I have is that intuitively, certain prositional atoms in PROP have yet to be 'settled'. For example an atom that occurs in 2100. There are futures where it is either true or false. Similarly, our $\sigma$ function is meant to represent the epistemic history of what occurs. However we should also be able to consider 'futures', beyond where the sequence $\sigma$ has reached. For example if the sequence stopped at $t$ and I wanted to consider whether or not $M,w,t, \sigma \models XX \varphi$, it would require me to consider a hypothetical future. The truth of these propositions have yet to be determined.
To solve this problem I am trying to define a new logic, and am looking for help in defining the concept of 'settled'.
What I have done so far is define a supervaluation $V$ and then define a set $S_T$ as the settled atoms at time $T$.
I then consider the set $V_T = \{U: U \mapsto 2^W | \forall p \in S_T, U(p) = V(p)\}$
I.e. we get the set of possible valuations that agree on the settled atoms.
I then define that $M,U,w \models p$ iff $w \in U(p)$
and say that a proposition $\varphi$ is physically settled at $T$ iff $\forall U \in V_T, M,U,w \models \varphi$. I assume here that $\varphi$ does not contain epistemic operators such as $X,Y,K$.
So now I've got the 'physically settled propositions' at a given time. I now want to do the same thing, but with epistemic propositions. So I want to make sure that in general, propositions of the form $X \varphi$ are not settled.
I try to do the same thing as I did with the relations.
So essentially, I fix the 'physical time' $T$, and consider the sequence $\sigma_T = \langle R_T^1, R_T^2 . . R_T^t \rangle$.
I then define a set of `relation sequences':
$Q^t_T = \{ \Lambda : \Lambda = \langle \lambda_1, \lambda_2 . . \rangle, \forall j \in t, \lambda_j = R_T^j\}$
So these $\Lambda$ sequences are infinitely long but they agree with the $\sigma_T$ sequence up until time $t$.
I now consider a proposition that uses $\varphi$ as a base, call it $B[\varphi]$. I.e. it uses $\varphi$ but allows the inclusion of epistemic operators such as $K, X, Y$.
I then say that $B[\varphi]$ is settled iff $\varphi$ is physically settled and
$\forall \Lambda \in Q^t_T, M, U, \Lambda, w, t, T, \models B[\varphi]$.
I.e., it is true in all epistemic futures (given by the different possible sequences).
So the settled propositions have their truth value already determined. In general, they do not use futuristic operators such as $X$, and any atoms they use represent propositions that are already 'temporally decided'.
Thanks for any help. I'm finding this all quite challenging. Does this make sense, have I made any errors and what should I change?
