A refined isomorphism theorem in categorical abstract algebraic logic

José Gil-Férez

University of Barcelona

In [1] a characterization of algebraizability of a sentential logic $\mathcal S$ is obtained in terms of the existence of an isomorphism between the lattice of theories of $\mathcal S$ and the lattice of theories of the equational consequence of its equivalent algebraic semantics $\mathbf K$, 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 $k$-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 $\pi$-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. $\pi$-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 $\mathcal I$ and $\mathcal I'$ are two term $\pi$-institutions, then they are deductively equivalent if, and only if, there exists an adjoint equivalence $\langle F,G,\eta,\varepsilon\rangle:\mathbf{Th}\mathcal I\rightharpoonup\mathbf{Th}\mathcal I'$ 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 $k$-systems can) as term $\pi$-institutions. This shows that this condition is probably too strong. But it cannot be just removed: I will provide two $\pi$-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 $\pi$-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 $\mathbf{Cat}$-valued functor will be used. We obtain then the following extended version of the Isomorphism Theorem:

Theorem. If $\mathcal I$ and $\mathcal I'$ are two multi-term $\pi$-institutions, then they are deductively equivalent if, and only if, there exists an adjoint equivalence $\langle F,G,\eta,\varepsilon\rangle:\mathbf{Th}\mathcal I\rightharpoonup\mathbf{Th}\mathcal I'$ 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).