[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