But, it is not directly possible to talk _about_ groups in
formulas though this is absolutly common in mathematics. It is
not possible in this "theory" representation unless we redefine
the whole theory again as a predicate.
My question is now: Are there any other theorem proving systems
which offer an explicit theory notion and allow to do the
described change of viewpoint in a more elegant way?
This, I maintain, is what linear logic is *really* the logic of. LL
makes most sense to me when
(i) the formulas of LL are interpreted as the objects of mathematics:
sets, groups, vector spaces, binary relations, Boolean algebras, etc.,
organized as a single category of concrete objects;
(ii) the sequents of LL as the morphisms of that category; and
(iii) the inference rules of LL as endofunctors on that category.
When the LL variables are left uninterpreted the formulas become
sesquifunctors (functors containing both covariant and contravariant
occurrences of the same variable) and the objects dinatural
transformations. This is what LL is about.
This homogenization of category (Grp, Rng, etc as mere full concrete
subcategories of the one supercategory) forces the issue of where to
put the signature: there is no obvious place to put it but in the
objects themselves, any other place is a bear to manage. This is where
Chu spaces enter the picture: they provide a simple and uniform
mechanism for storing arbitrarily variable signature in objects. This
mechanism is simultaneously *much* simpler and *much* more general than
that of institutions.
Clearly we are a long way from even reaching consensus on this role for
LL, let alone converting it into anything as concrete as a theorem
prover that allows one to reason "linearly" about whole groups and
rings. This is the general direction I'm working in.
What there *is* consensus on is that the sequents of LL are dinaturals
between sesquifunctors; it is the relevance of this to general
mathematics that is up for grabs here. Clouding the issue here is that
not all familiar categories appear as canonical subcategories---posets,
distributive lattices, algebraic lattices, etc. are fine, Grp is not
(yet). This is a legitimate concern, but one that I see as less a
show-stopper than a curiosity of the mathematical landscape.
If anyone else is working on reasoning linearly about mathematical
objects I'd love to correspond.
My Linear'96 talk in Japan at the end of this month, "Linear Logic
complements Classical Logic," is on this topic. QED sits squarely in
the CL camp; it is a good camp, but as Florian's message, along with
the last couple of generations of algebra texts, should make clear, it
is not the only camp. Algebra from the category perspective is just as
big, and LL is its logic.
Vaughan Pratt