[Prev][Next][Index][Thread]

Lindenbaum algebras and linear logic



Date: Fri, 10 Jan 92 22:35:00 EST

Recently Jean Gallier brought up:
 
>>It is well known that in classical logic (say propositional,
>>to simplify matters), to any consistent theory T (set of propositions
>>closed under logical consequence) on can associate a boolean
>>algebra B_T, the so-called "Lindenbaum algebra" of T.
>>B_T consists of the equivalence classes of propositions
>>under the equivalence relation A \equiv B iff T |- A <=> B

adding..

>> Is there a finite model property for these
>>structures?
>>Even for the pure multiplicative fragment, I don't know if this
>>is true. 

This is certainly an interesting question, and it is one approach Jawahar 
Chirimar and I have taken to studying decidability  of some  fragments of LL.

  In particular, for the Tensor-bang fragment (TBLL),
 one can define a notion of Kripke model, namely a monoid M,
with a distinguished class of idempotents (closed under multiplication) with
some additional "filtrability conditions" such that 

  1) the Lindenbaum monoid is a model
  2) every model is elementarily equivalent to a finite quotient 
       (the so-called "filtration")

hence, (since the fragment is axiomatizable and truth of a sequent in a finite
model is decidable) this gives a decision method for TBLL.

we have also worked with partial monoids in order to develop tableaux proof
methods for these fragment.

  We expect to have a tech report available by mid february.

Jim Lipton                             J. Chirimar
Dept. of Mathematics                   Department of CIS
                  University of Pennsylvania             
                  Philadelphia, PA  19104                
E-MAIL: lipton@saul.cis.upenn.edu    chirimar@saul.cis.upenn.edu