Un μ-calcul est une logique propositionnelle avec des opérateurs de point fixe μ et ν. Par exemple, étant donnée une formule propositionelle t(x) dont l'interprétation est une fonction monotone f: L → L sur un treillis complet, on ajoute deux nouvelle formules μx.t(x) et νx.t(x) pour dénoter les plus petit point fixe et les plus grand point fixe de f, respectivement.
Les opérateurs μ et ν sont semblables à des quantificateurs, et on définit des classes Sn et Pn comme il suit: S0 = P0 est la classe des tous les termes sans application des opérateurs de point fixe; Sn+1 est la clôture de Sn et Pn sous la substitution et l'opérateur μ; Pn+1 est la clôture de Sn et Pn sous la substitution et l'opérateur ν.
Dans cet exposé je vais montrer comment on peut utiliser des outils de la théorie des preuves pour montrer le fait suivant: soient t dans Pn+1 et s dans Sn+1 deux μ-termes dans la signature des treillis; si pour toute interprétation dans un treillis complet on a |t| ≤ |s|, alors ils existe un μ-terme r tel que: 1) pour toute interprétation |t| ≤ |r| et |r| ≤ |s|, 2) il appartient à la clôture de Sn et Pn sous la seule opération de substitution.
Les preuves que nous considérons sont en effet des stratégies gagnantes dans des jeux de la forme G → H, où G et H sont des jeux de parité. Car le jeu G → H peut bien avoir des cycles, les stratégies gagnantes dans ce jeu peuvent aussi contenir des cycles.