José Gil-Férez
In [1] a characterization of algebraizability of a sentential logic
is obtained in terms of the existence of an isomorphism
between the lattice of theories of
and the lattice of
theories of the equational consequence of its equivalent algebraic
semantics
, commuting with substitutions. In [2] we find a
generalization of this result in Teorem V.3.5, stating that two
deductive systems are equivalent if, and only if, there exists an
isomorphism between their lattices of theories, commuting with
substitutions. In turn, in [5] a new generalization of this result is
exhibited for Gentzen systems: Theorem 2.19.
Each of these systems is a generalization of the previous one:
sentential logics and equational consequences of a class of algebras
are particular cases of -deductive systems, which are particular
cases of Gentzen systems. But there are other kinds of deductive
systems with a similar Isomorphism Theorem that are not, nor extend,
Gentzen systems.
A generalization of all these systems are -institutions, which
were introduced for the first time by Fiadeiro and Sernadas in [3],
inspired by the work on institutions of Goguen and Burstall in [4].
Institutions cover all these deductive systems and also formalize other
multi-sorted ones coming form computing science.
-institutions in
turn focus attention in the syntax instead of in semantics, as do
institutions. For both, a categorical context organizing the
information is required.
In [6] Voutsadakis proved the following result:
Theorem (Voutsadakis). If and
are two term
-institutions, then they are deductively equivalent if, and only
if, there exists an adjoint equivalence
that commutes with
substitutions.
This result is a generalization of Theorem V.3.5 of [2]. However, in
spite of its abstraction level, it is not a generalization of
Theorem 2.19 of [5], since not all Gentzen systems can be exhibited (in
fact, only those that are -systems can) as term
-institutions.
This shows that this condition is probably too strong. But it cannot be
just removed: I will provide two
-institutions which are not
deductively equivalent but with isomorphic categories of theories
(through an isomorphism commuting with substitutions).
The objective of eliminating absolutely the conditions over the
-institutions in the characterization theorem of deductive
equivalence is then vane. However, I will offer a way of extending the
result which will cover Gentzen systems among others. To do this, the
notion of Grothendieck construction of a
-valued functor
will be used. We obtain then the following extended version of the
Isomorphism Theorem:
Theorem. If and
are two
multi-term
-institutions, then they are deductively equivalent if, and only
if, there exists an adjoint equivalence
that commutes with
substitutions.
References
[1] W.J. Blok and D. Pigozzi. Algebraizable Logics, volume 77 of the Memoirs of the American Mathematical Society. A.M.S., Providence, January 1989.
[2] W.J. Blok and D. Pigozzi. Abstract algebraic logic and the deduction theorem. Buletin of Symbolic Logic, to appear.
[3] J. Fiadeiro and A. Sernadas. Structuring theories on consequence. In Recent Trends in Data Type Specification, volume 332 of Lecutre Notes in computer Science, pages 44-72. Springer-Verlag, New York, 1988.
[4] J.A. Goguen and R.M. Burstall. Introducing institutions. In Logics of programs (Pittsburgh, Pa., 1983), volume 164 of Lecture Notes in Computer Science, pages 221-256. Springer, Berlin, 1984.
[5] J. Rebagliato and V. Verdú. Algebraizable Gentzen systems and the deduction theorem for Gentzen systems. Mathematics Preprint Series, (175), June 1995.
[6] George Voutsadakis. Categorical abstract algebraic logic:
equivalent institutitions. Studia Logica, 74(1-2):275-311, 2003.
Abstract algebraic logic, Part II (Barcelona, 1997).