Phase semantics

Propositional case

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.

Finite model property

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