[Prev][Next][Index][Thread]
Lindenbaum algebras and linear logic
To: linear@cs.stanford.edu
Date: Fri, 03 Jan 92 11:17:33 EST
In view of discussions regarding various semantics of linear logic,
I thought it might be interesting to make the following remark.
I will also state some problems for which I have no answer.
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
(where <=> denotes logical equivalence).
There is a correspondence between truth assignments satisfying T
and ultrafilters over B_T (basically because given an ultrafilter
U in B_T, the quotient B_T/U is isomorphic to {false, true}).
This leads to a proof of completeness for classical
propositional logic w.r.t. to truth assignments (cute proof, but
somewhat contorted).
Of course, what is nice about classical logic (but also a limitation!)
is that if a proposition is not provable, then a FINITE
counter example over {false, true} can be produced.
Similarly, we can associate an algebraic structure H_T to a theory T
in intuitionistic logic. This time, we don't get a boolean algebra,
but a Heyting algebra (see for example, the draft of the book
by Nerode and Odiffreddi). H_T is a lattice with an additional
operation --> such that
a /\ b <= c iff a <= b --> c.
One can also say that a Heyting algebra is a bicartesian closed
category such that for any two objects a and b, Hom(a,b) U Hom(b,a)
has at most one element.
We also get a completeness theorem w.r.t Heyting algebras, but
it is not very exciting. Indeed, if a proposition is not
provable intuitionistically, the completeness proof only gives
an infinite counter model. One needs to work harder to show
that a finite counter example exists. In fact, I haven't
seen any proof that doesn't appeal to Kripke models first, and the
fact that from a Kripke model, one can construct a topological
Heyting algebra (Stone 1937, Tarski, 1938) using the order topology.
Question 1: Does anybody have a DIRECT proof (not using Kripke
models) of a finite model property w.r.t Heyting algebras
for intuitionistic logic?
I now come to linear logic (excluding the exponentials).
We run into a first difficulty. Given a set T of propositions,
T |- A -o B and T |- B -o C not longer implies that T |- A -o C
(but T, T |- A -o C). So, let's consider T = empty.
We get an algebraic structure
(should we call it the "linear Lindenbaum algebra", Yuk, no!)
on the set of equivalence classes
under the equivalence A \equiv B iff |- A -o B and |- B -o A.
In fact, this thing is simultaneously a lattice
with an involution, and a commutative
monoid. Furthermore, tensor is monotonic w.r.t to <=
(where [A] <= [B] iff |- A-o B),
[A] par [B] = ([A^\perp] tensor [B^perp])^perp,
and
a tensor b <= c iff a <= b^perp par c.
These structures have been used by Avron, Abrusci, Ono, Troelstra,
and others.
In the intuitionistic case, it is the degenerate case of
closed symmetric monoidal categories with finite products and coproducts
(Lafont, thesis). In the classical case, I suppose it is
a degenerate case of *-automomous categories (but please,
forgive my ignorance, and if you are mad at me, send me mail directly!)
One can easily prove a completeness theorem w.r.t these structures.
It is not quite Girard's completeness theorem, because Girard
uses phase structures. The connection between Girard's phase
structures and the structures mentioned above
is that the perp operation
on a phase structure yields a closure operation
X -> (X^perp)^perp, and so the set of facts forms a complete lattice
together with a commutative monoid structure
(in fact, the closure "double perp" arises from a Galois connection).
However, it is possible to imbed any lattice into a complete one
in such a way that existing infs and sups are preserved by using the
Mac Neille completion (basically Dedeking cuts), and in fact
structures as above where the lattice is complete arise from
phase spaces, and conversely induce phase spaces.
These complete lattices are also known under the name of
quantales (I think?).
In any case, one obtain another proof of Girard's completeness
theorem w.r.t quantales (or equivalently phase spaces).
(By the way, Troelstra's book and my paper part II discuss these
things, who have also been discussed earlier by Avron in his TCS paper).
Question 2: Is there a finite model property for these
structures?
Even for the pure multiplicative fragment, I don't know if this
is true.
In conclusion, it seems to me that even if these semantics are not
the most exciting for (pure) logicians, from the computer science
point of view, they are interesting. In particular, they are important for
decidability reasons.
By the way, the interpretation of the additives in the
"linear Lindenbaum algebra" as lattice operations seem to suggest
that Girard's naming of the constants is skewed. The additive
constants correspond to the bottom and top element of the
lattice, and the notation \top and 0 seems unfortunate, especially
because the multiplicative constants 1 and \bot are identities for
tensor and par. But Jean Yves has said that the interpretation
of the additives as lattice operations is "boring", and
now, he wants a phase space to be based on a ring, so
I will be patient and see what happens next!
-- Jean