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.