Situation-Tree Logic on a Profunctor

Let $\ct F:\ct S\ag\ct M$ be a given profunctor. We regard it as a category, fully containing both $\ct S$ and $\ct M$ , with additional heteromorphisms $S\to M$ .
Objects of $\ct S$ will be regarded as abstract situations (we are given this and that perhaps with certain elementary conditions), objects of $\ct M$ will be called models, and a heteromorphism $S\to M$ is regarded as an interpretation of situation $S$ in model $M$ .

We define a formal logic $(Ob\ct M,\models,\mathrm{Tree}(\ct S))$ by introducing the formulas as diagrams in $\ct S$ of shape of a directed rooted tree, which doesn’t have infinite path (but may have infinite branches at any node).

Definition. Such a given tree $\fii$ is said to be valid in a given model $M$ (in notation $M\models\fii$ ), if Eve has a winning strategy against Adam in the following game:
– Adam starts the game by saying an interpretation $R\to M$ of the root $R$ of $\fii$ in the model. [Eve automatically wins if there is no such interpretation.]
– After a move $u:S\to M$ , the other player has to find a next arrow $f_i:S\to T_i$ in the tree and say an interpretation $v_i:T_i\to M$ making the triangle commutative: $u=f_iv_i$ .
– If a player cannot make a next move (either a leaf is reached, or there is no such interpretation), loses.

For example, if a tree consists of a single arrow $f:R\to S$ , then $M\models f$ means that $M$ is an $f$ -injective object (all interpretations of $R$ in $M$ extend to interpretations of $S$ along $f$ ), in other words, that $f$ has the left lifting property with respect to $0\to M$ , where $0$ is an initial object of $\ct M$ .
In general, the moves of Adam correspond to universal choices (‘ $\forall$ ‘), the branches which he can choose -on even levels-, correspond to conjunction (‘ $\land$ ‘), and dually the moves of Eve correspond to existential choices (‘ $\exists$ ‘), and her branches -on odd levels- to disjunction (‘ $\lor$ ‘).

We define a first order situation for a fixed similarity type $\tau$ , to be a pair $(X,\Gamma)$ where $X$ is any set and $\Gamma$ is a set of elementary formulas (using the given relations symbols or equality for terms) built up by variables from $X$ .
We can simply set $\ct S_\tau$ be the preorder category induced by $(X,\Gamma)\subseteq(Y,\Theta)$ if ( $X\subseteq Y$ and $\Gamma\subseteq\Theta$ ).
An interpretation $u:(X,\Gamma)\to M$ in a $\tau$ type first order model $M$ is a mapping $u:X\to M$ such that each element of $\Gamma$ holds under the evaluation $u$ .