Finite Models for Linear Logics

Wojciech Buszkowski

Lafont [3] proves the finite model property (fmp) for Multiplicative-Additive Linear Logic (MALL), using a cut-free Gentzen style proof system for MALL. We provide another proof which uses special integer counts for formulas, called barriers. This method has been used in [2] to prove fmp for the logic BCI and its subsystems, being different variants of the Lambek calculus. We show that MALL is syntactically interpretable in the extension of BCI admitting the additive conjunction ∧ and the top T with rules:

(R1) from Γ, A ⊢ C (resp. Γ, B ⊢ C) infer Γ, A ∧ B ⊢ C,

(R2) from Γ ⊢ A and Γ ⊢ B infer Γ ⊢ A ∧ B,

(AT) Γ ⊢ T.

The proof of fmp for BCI, given in [2], can also be applied to this extension of BCI, which yields fmp for MALL. The same method of proof can be used for noncommutative systems, in particular to Cyclic MALL of Yetter [4]. Precisely, the method of barriers yields a proof of fmp for the product-free Lambek calculus with ∧, T and a special constant ⊥ with the rule:

(R3) from Γ, Δ ⊢ ⊥ infer Δ, Γ ⊢ ⊥,

and Cyclic MALL is syntactically interpretable in the latter logic (we use the semantics of Abrusci [1]).

Our method does not rely upon the structure of cut-free proofs, hence it can also be applied to some finitely axiomatizable theories over BCI and the Lambek calculus. The construction of a finite model falsifying a given unprovable formula is effective, and the models are based on simple algebras of finite sets of sequences of formulas (finite languages).

[1] V.M. Abrusci, Phase semantics and sequent calculus for pure noncommutative propositional linear logic, Journal of Symbolic Logic 56 (1991), 1403-1451.

[2] W. Buszkowski, The finite model property for BCI and related systems, Studia Logica 57 (1996), 303-323.

[3] Y. Lafont, The finite model property for various fragments of linear logic, manuscript, 1995.

[4] D.N. Yetter, Quantales and non-commutative linear logic, Journal of Symbolic Logic 55 (1990), 41-64.

Address: Faculty of Mathematics and Computer Science, Adam Mickiewicz University in Poznań, Poland

E-mail: buszko@amu.edu.pl