Indexed flows in temporal × modal logic with functional semantics

Two classical semantical approaches to studying logics which combine time and modality are the T × W-frames and Kamp-frames (Thomason (1984)). In this paper we study a new kind of frame that extends the one introduced in Burrieza et al. (2002). The motivation is twofold: theoretical, i.e., representing properties of the basic theory of functions (definability); and practical, their use in computational applications (considering time-flows as memory of computers connected in a net, each computer with its own clock). Specifically, we present a temporal × modal (labelled) logic, whose semantics are given by ind-functional frames in which accessibility functions are used in order to interconnect time-flows. This way, we can: (i) specify to what time-flow we want to go; (ii) carry out different comparisons among worlds with different time measures; and (iii) define properties of certain kinds of functions (in particular, of total, injective, surjective, constant, increasing and decreasing functions), without the need to resort to second-order theories. In addition, we define a minimal axiomatic system and give the completeness theorem (Henkin-style).