General logics. (English) Zbl 0691.03001

Logic colloq. ’87, Proc. Colloq., Granada/Spain 1987, Stud. Logic Found. Math. 129, 275-329 (1989).
[For the entire collection see Zbl 0673.00006.]
In order to capture the essence of the interaction between logic and computer science, the author introduces a new axiomatization of logic. On this basis, he axiomatizes logic programming, one of the areas where logic and computer science interact most strongly.
The author observes that the previous axiomatizations of logic tend to fall within two main approaches: the model-theoretic approach and the proof-theoretic approach. While the model-theoretic approach takes the satisfaction relation between models and sentences as basic, the proof- theoretic approach takes the entailment relation between sets of sentences as basic. The author has found that neither of these approaches is by itself sufficient to axiomatize logic programming. Thus, he proposes an axiomatization of logic which unifies both approaches and yields the desired axioms of logic programming. Beyond their application to logic programming, the axioms for general logics given in the paper will certainly have wide applicability within logic and computer science.
Although the paper has goals that are in full agreement with those of J. A. Goguen and R. M. Burstall’s theory of institutions [Lect. Notes Comput. Sci. 164, 221-256 (1984; Zbl 0543.68021)], the proposed theory addresses proof-theoretic aspects not addressed by institutions. The author remarks that institutions can be viewed as the model-theoretic component of the new theory.
One of the main new contributions in the paper is a general axiomatic theory of entailment and proof, which covers the proof-theoretic aspects of logic and the many proof-theoretic uses of logic in computer science. As the entailment relation asserts provability but says nothing about how a sentence is actually proved, in order to account for proofs and for their internal structure the author introduces the new axiomatic notion of proof calculus which is very general and does not favor any particular proof-theory style. The computer science counterpart of a proof calculus is the notion of “operational semantics”. The flexibility of the axioms given for proof calculi permits putting them and operational semantics on a common abstract basis, offering the possibility of a more intense mutual iteraction between the two fields. On this basis, operational semantics could be placed on firmer logical fundamentals and proof theory could be enriched with new and more flexible proof systems.
Perhaps the most important contribution is the new concept of mappings that interpret one logic (or proof calculus) in another. Mappings play a key role in relating different logics and different computer systems, and such relationships are conceptually and practically very important. The study of mappings may also suggest new methods for the rigorous design and development of computer systems.
Two other contributions of great importance, suggesting new possibilities for language design, are: a general definition of categorical logic and the axioms for logic programming.
Starting from the need to better understand and relate the many different logics currently being used in computer science and from the related need for new approaches to the rigorous design of computer systems, the author proposes some new and very interesting concepts and sets the basis for new research directions in logic and computer science.
Reviewer: D.Savin


03B30 Foundations of classical theories (including reverse mathematics)
03B70 Logic in computer science
68N01 General topics in the theory of software
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03G30 Categorical logic, topoi
68Q65 Abstract data types; algebraic specification