# Finitary assignment functions and typed modal languages

I'm working through Giovanna Corsi's article on Counterpart Semantics for Modal Logic. She is working with a typed modal language $\mathscr{L}^{t}$. Where this differs from usual presentations I've seen of modal logic is that she utilizes finitary variable assignment functions.

A counterpart frame $\mathcal{F}$ for $\mathscr{L}^t$ is a quadruple $\langle W, R, D, \mathfrak{C} \rangle$, where $W \neq \emptyset$, $R \subseteq W^2$, $D$ is a domain function such that $D_w$ is a set (i.e., the domain of $w$) for every $w \in W$, and $\mathfrak{C}$ is the counterpart relation such that $\mathfrak{C} = \uplus_{\langle w, v\rangle \in W}\, \{\mathfrak{C}_{\langle w, v\rangle}\}$, where for any $\langle w, v\rangle \in W$ such that $wRv$, $\mathfrak{C}_{\langle w, v\rangle} \subseteq (D_w \times D_v)$.

A counterpart model $\mathcal{M}$ for $\mathscr{L}^t$ is a pair $\langle \mathcal{F}, I \rangle$, where $\mathcal{F}$ is a counterpart frame and $I$ is a function that for each $w \in W$ determines an interpretation function $I_w$ such that:

• for any predicate $P^n$ of $\mathscr{L}^t$, $I_w(P^n) \subseteq (D_w)^n$
• $I_w (=)$ $=$ $\{{\langle a, a \rangle : a \in D_w}\}$
• for any individual constant $i$ of $\mathscr{L}^t$, $I_w(i) \in D_w$
• for any function symbol $f^n$ of $\mathscr{L}^t$, $I_w(f^n) : (D_w)^n \rightarrow D_w$

The meat of my question centers on how she wants to understand typed formulas. She says that a wff $A$ is of type $n$ iff the free variables occurring in $A$ are $x_1,\ldots, x_n$. She clarifies further that the type of a wff can be seen as the context with respect to which the formula is meaningful (pg. 33).

Finitary assignments are functions defined on initial segments of the sequence $x_1$, $x_2$, $\ldots$, $x_n$ of the variables of $\mathscr{L}^t$. Since assignments are supposed to give us the context relevant to assessing the truth of a sentence, we restrict assignments to the salient world. For each $w \in W$, the finitary assignments relative to $w$ are just $n$-tuples $\langle a_1,...,a_n \rangle,\, n \geq 1$, of elements of $D_w$, letting $a_i$ be the value for $x_i$.

If we have a one-place predicate $P(x)$, and a class of projection functions $\pi^m_k : X^m \rightarrow X$, $1 \leq k \leq m$, such that

$$\pi^m_k (u_1,\dots, u_m) = u_k$$

then, unlike in the classical setting with infinitary assignments, the following equivalence doesn't hold $$(1)\, \langle a_1 \rangle \models_w \Box P (\pi^1_1 (x))\, \text{ iff } \,(2)\, \langle a_1, a_2 \rangle \models_w \Box P (\pi^2_1 (x, y))$$

Since (1) must take into consideration all accessible worlds with a counterpart of $a_1$, while (2) must consider systems with counterparts of both $a_1$ and $a_2$ (see Corsi p. 12).

But what if I wanted to say something like "2 is necessarily prime", and I thought that the relevant context for evaluating claims about the natural numbers was relative to the entire (infinite) sequence of natural numbers? Is there any way to capture this using finitary assignments? My only thought was that maybe if a statement like "2 is necessarily prime" holds for every finite assignment of n-length sequences of natural numbers it would hold for an infinite sequence of natural numbers (something like a variable assignment version of compactness). But I don't know if that even makes any sense, let alone if it provides a way of respecting the intuition that modal claims about the natural numbers must be evaluated relative to the entire infinite sequence of natural numbers.

TL;DR Is there any way to simulate the evaluation of formulas relative to infinite sequences of elements when you're working with finitary assignments in a type modal language?