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
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 .