Modal logics and logics with integer or even rational numbers - is that possible? I am trying to find some research trends (publications, keywords for futher search, etc.) on logics and modal logics whose predicates can containt integer or even rational numbers (like x>2, x^2>3, complexFunction(x)>4 and so on). I understand that in each case such predicates can be expressed as a Boolean variablea/predicatea (there can be Boolean variable for each natural number, but it is expensive representation) but I guess - there should be some trends due to immense application of such logics.
So far I have found two trends:
  1.  modal logics with nominals i.e. hybrid logics
  2.  graded modal logics
But maybe there is something else.
So, one look of this problem is trying to introduce numbers in logic, but other approach is trying to express boolean variables and constraints as numbers in integer programming approach. But I guess that the first approach is more appealing (due to predicatable integration in AI applications).
 A: Something like $\square_e P_2$, where $\square_e$ is interpreted as "is even" and $P_2$ is interpreted as (e.g.) the number 2? 
Since numbers themselves don't have truth values, you'd also have to set interpretations for a $F \wedge G$, $\square A$ etc. such that they makes sense. 
One natural way to go might be ($f$ being some helper function):


*

*$f(P_n) = \{n\}$

*$f(\top) = U$ (universe)

*$f(F \wedge G) = F \cap G$

*$f(\neg F) = U \setminus F$

*$f(\square_R A) = \{x\in U|x \in A \rightarrow R(x) \}$


If $e(n) = (\exists k\in U)(2*k = n)$ and we regard formula $F$ as true if $f(F) = U$ then for natural numbers $k, n$:


*

*$P_n, \neg P_n$ aren't theorems 

*$P_n \vee \neg P_n$,  $\square_eP_{2k}$, $\Diamond_e P_{2k +1} \rightarrow P_{2k + 1} $ are theorems


Try to see whether $(\square (A \rightarrow B) \wedge \square(A)) \rightarrow \square B$ holds. Or compare it with the version in which $f(F \wedge G) = F \cup G$. Another thing to try would be to allow infinitary conjunctions. Also to see whether this or similiar system can be made into a NML. 
