Untangling conditions from responsibility

I've re-read the introduction to computability logic, and found that I might want to define my own version of it (or at least to try that).
For example, in CL it is not possible to define arbitrary predicates for branching - only those that can be assembled from conjunction and negation. It may sound funny at the first glance (and/not is a sufficient set of operations, as is Sheffer stroke, for example, right?), but this only holds in classical logic - as games are stateful in a way, one should not duplicate them lightheartedly, so some kind of linearity is needed. For example, XOR or EQ cannot be defined using AND and NOT without duplicating the parameters (A XOR B is !(!A & !B) & !(A & B)).

To overcome this problem, I prospose to replace conjunction and negation in the logic by a branching operator with attached truth table. So NOT A becomes BRANCH(a:A; not a), AND A B - BRANCH(a:A, b:B; a and b), XOR A B - BRANCH(a:A, b:B; a xor b) - where I write truth tables as classical logic formulas for brevity. Note that each subgame is mentioned by branch exactly once.

I have to explore the issues raised by the fact that now it becomes possible to define branches with not monotonically non-decreasing condition. The previous encoding elegantly combined conditions with switching responsibility. I would like to untangle one from another if only to prove that it was unnecessary. So in addition to replacing and/not by branch, I would like to explicitly annotate choices and quantifications by the party responsible for them, and make this annotation unaffected by branching conditions. This will yield more verbose formulas, but has potential of uncovering some independence between features that were coupled.

Also, for various reasons, I will use game variables instead of predicates as a base case.

All in all, game language could be defined as:
G = branch (Seq n G) satisfying (Seq n Bool -> Bool)
| hide x in G by Bool
| choose (Seq n G) by Bool -- in future also dependently-typed version of this
| let x = G in G -- recursion definition
| x -- recursion backlink
| v -- external game variable
| replicate G by Bool -- replication, may add some constraints on cardinality later

I may want to drop recursion and move to representing games as directed graphs at some point. ATM, textual representation is more handy, though.

The next installment will probably discuss terms (err, runs) for these types (games) or theories and models of this language.