Phase semantics

Warning : This page is under construction.

Propositional case

Phase spaces - Phase models - Syntactical model

Theorem: If A is a propositional formula, the following properties are equivalent:

  1. A is provable;
  2. A holds in any phase model;
  3. A holds in the syntactical model;
  4. A is cut-free provable.
Corollary: cut elimination (propositional case)


Finite model property

Finite models  - Semilinear models

MLL = Multiplicative Linear Logic
MALL = Multiplicative Additive Linear Logic
MELL = Multiplicative Exponential Linear Logic
LL = Linear Logic
WLL = Affine Linear Logic
 
 
MLL
MALL
MELL
LL
WLL
finite model property
yes
yes
no
no
yes
semilinear model property
yes
yes
?
no
yes
decidability
yes
yes
?
no
yes