Game semantics

This article presents the game-theoretic fully complete model of MLL. Formulas are interpreted by games between two players, Player and Opponent, and proofs are interpreted by strategies for Player.

Preliminary definitions and notations

• If M is a set, M ^* will denote the set of finite words on M;
• If $s\in M^*$, | s | will denote the length of s;
• If $1\leq i\leq |s|$, s_i will denote the i-th move of s;
• We define $\overline{(\_)}:\{O,P\}\to \{O,P\}$ with $\overline{O} = P$ and $\overline{P} = O$
• We denote by $\sqsubseteq$ the prefix partial order on M ^*

Games and Strategies

Definition (Games)

A game A is a triple (M_A,λ_A,P_A) where:

• M_A is a finite set of moves;
• $\lambda_A: M_A \to \{O,P\}$ is a polarity function;
• P_A is a subset of $M_A^*$ such that
  • Each $s\in P_A$ is alternated, i.e. if we define λ_A(s_i) = Q then, if defined, $\lambda_A(s_{i+1}) = \overline{Q}$;
  • A is finite: there is no infinite strictly increasing sequence $s_1 \sqsubset s_2 \sqsubset \dots$ in P_A.