Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Game semantics for the constructive $μ$-calculus

Leonardo Pacheco

TL;DR

These game semantics are used to prove that the $\mu$-calculus collapses to modal logic over CS5 frames and the completeness of $\mathsf{\mu CS5}$ over frames is proved.

Abstract

We define game semantics for the constructive $μ$-calculus and prove its equivalence to bi-relational semantics. As an application, we use the game semantics to prove that the $μ$-calculus collapses to modal logic over the modal logic $\mathsf{IS5}$. We then show the completeness of $\mathsf{IS5}$ extended with fixed-point operators.

Game semantics for the constructive $μ$-calculus

TL;DR

These game semantics are used to prove that the -calculus collapses to modal logic over CS5 frames and the completeness of over frames is proved.

Abstract

We define game semantics for the constructive -calculus and prove its equivalence to bi-relational semantics. As an application, we use the game semantics to prove that the -calculus collapses to modal logic over the modal logic . We then show the completeness of extended with fixed-point operators.
Paper Structure (23 sections, 21 theorems, 17 equations, 1 figure, 1 table)

This paper contains 23 sections, 21 theorems, 17 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Outline
  3. Acknowledgements
  4. Constructive mu-calculus
  5. Syntax
  6. Semantics
  7. The modal logic $\mathsf{IS5}$
  8. The fixed-point logic $\mathsf{\mu IS5}$
  9. Game semantics for the constructive mu-calculus
  10. Definition
  11. Correctness of game semantics
  12. The collapse to modal logic over IS5 models
  13. The key lemma
  14. The collapse
  15. The completeness of muIS5
  16. ...and 8 more sections

Key Result

Proposition 1

Fix a $\mathsf{CK}$-model $M={\langle W, W^\bot,\preceq,R, V \rangle}$ and a formula $\varphi(X)$ with $X$ positive. Then the operator $\Gamma_{\varphi(X)}$ is monotone. Therefore the valuations of the fixed-point formulas $\mu X.\varphi$ and $\nu X.\varphi$ are well-defined.

Figures (1)

  • Figure 1: Schematics for forward and backward confluence.

Theorems & Definitions (42)

  • Definition 1
  • Definition 2
  • Proposition 1
  • proof
  • Definition 3
  • Theorem 2: Mendler, de Paiva mendler2005constructive
  • Definition 4
  • Theorem 3: Ono ono1977intuitionistic, Fischer Servi fischerservi1978finite
  • Lemma 4
  • proof
  • ...and 32 more