Let be a given profunctor. We regard it as a category, fully containing both and , with additional heteromorphisms .

Objects of will be regarded as abstract *situations* (we are given this and that perhaps with certain elementary conditions), objects of will be called *models*, and a heteromorphism is regarded as an *interpretation* of situation in model .

We define a formal logic by introducing the formulas as diagrams in 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 is said to be *valid* in a given model (in notation ), if `Eve`

has a winning strategy against `Adam`

in the following game:

– `Adam`

starts the game by saying an interpretation of the root of in the model. [`Eve`

automatically wins if there is no such interpretation.]

– After a move , the other player has to find a next arrow in the tree and say an interpretation making the triangle commutative: .

– 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 , then means that is an -injective object (all interpretations of in *extend* to interpretations of along ), in other words, that has the *left lifting property* with respect to , where is an initial object of .

In general, the moves of *universal* choices (‘‘), the branches which he can choose -on even levels-, correspond to *conjunction* (‘‘), and dually the moves of `Eve`

correspond to *existential* choices (‘‘), and her branches -on odd levels- to *disjunction* (‘‘).

We define a *first order situation* for a fixed similarity type , to be a pair where is any set and is a set of elementary formulas (using the given relations symbols or equality for terms) built up by variables from .

We can simply set be the preorder category induced by if ( and ).

An interpretation in a type first order model is a mapping such that each element of holds under the evaluation .