The concept of a labelled deductive system (LDS) can be considered as a general approach to the theory of logical systems enabling to cover, in a uniform way, many other different concepts of a logical system.
In the first chapter, by answering the question: “What is a logical system?”, the author considers the notion of a logical system through the following four stages. The starting point is a logical system defined in a traditional way as a consequence relation on sets of formulae satisfying reflexivity, monotonicity and transitivity conditions. The next stage is a logical system as an algorithmic proof system generating the corresponding consequence relation, followed by a logical system as an algorithmic structured consequence relation and, finally, the central concept presented in this chapter is the LDS approach which can be roughly considered as an ordered triple \(({\mathcal A}, {\mathbf L},R)\), where \({\mathbf L}\) is a logical language consisting of symbols for logical operators and formulae, \({\mathcal A}\) is an algebra with some operations on labels and \(R\) is a discipline of labelling formulae of the logic from the algebra \({\mathcal A}\), together with the corresponding deduction rules and the ways of propagating the labels via the application of the deduction rules. The chapter concludes with an outline of the author’s view of semantics.
The second chapter motivates LDS through many examples including the various known systems of monotonic and nonmonotonic logics, based on propositional, modal or predicate language, followed by an overview of interactive practical reasoning systems.
The central notion of the third chapter is that of an algebraic LDS, as most suitable for applications. They are a kind of LDS which arise in turning any specific logical system into an LDS, and have the form \(({\mathcal A}, {\mathbf L})\), where \({\mathcal A}\) is an algebra of labels. All labels in an algebraic LDS are from \({\mathcal A}\) and all formulae are from \({\mathbf L}\). In this context a declarative unit has the form \(t:A\), and a database has the form \((D, {\mathbf f}, d)\), where \(D\) is a diagram of the theory of \({\mathcal A}\), containing labels and some relations between them of the form \(\varphi (x,y)\), \(\sim \varphi (x,y)\), \(x \leq y\), \(\sim x \leq y\) and some equalities, and the function \({\mathbf f}\) associates with each \(t \in D\), a \(\text{wff} {\mathbf f} (t)\). In the introductory section, a simplified version of the basic definitions of algebraic LDS are presented, followed by the proof-theoretical considerations based on a generalized natural deduction system. As the labels can be used for metalevel control, we need only elimination rules to define the system, due to the fact that the introduction rules can be obtained immediately from the elimination rules. The chapter proceeds to deal with the propositional implicational LDS and with the metabox system, the formal mechanism used in LDS, which is a way of formulating special introduction rules for presenting particular logics.
As the author says, the fourth chapter gives a quick glimpse of general LDS and their fibred semantics (because a full treatment of this subject is left for Volume 2 of the book). The label is supposed to give more information about the formula it annotates and consequently a label can itself be a database. On the other hand, a formula is, in general, a logical declarative statement being by its nature a database. Thus, a definition of an LDS allowing for declarative units of the form \(\Delta_1 : \Delta_2\), where \(\Delta_1\) is a database from one LDS serving as a label and \(\Delta_2\) is a database from another LDS serving as a formula, is needed. For instance, in the context of modal logic the declarative unit of the form \(\Delta_1 : \Delta_2\) contains \(\Delta_1\) as a name for a possible world and \(\Delta_2\) as a formula holding at that world.
The fifth chapter illustrates the use of the metabox system, introduced in the third chapter, to define some of the known logics, with particular attention to the class of logics called resource logics, which use the labels to observe and record the use of the assumptions. Important subclasses of resource logics are linear logic, relevance logic and their neighbours. Another subclass contains the so-called prioritised logics, where the main restrictions are on how to use the inference rules.
The fundamental concepts involved in the relationship between meta-language and object language features are clarified in the sixth chapter. The conceptual framework revolves around the notions of a proper meta-language and that of an object language \({\mathbf L}\) implementing meta-language features for a language \({\mathbf M}\). As a suitable context for this consideration first-order classical logic is used.
As the LDS approach presents a general method in the theory of logical systems, the seventh chapter describes how to give an LDS formulation to traditionally formulated logics, where the traditionally formulated logics include Hilbert type systems, Gentzen type systems, tableaux systems and algebraic semantics. Roughly speaking, the problem is to create an LDS for a logic by bringing some of its semantics into the syntax. In case of modal logic the labels are possible worlds and the algebra of labels is the first-order theory of its Kripke semantics. The problem is solved through the following stages. First, it is shown how to give possible world-like semantics for an almost arbitrary consequence relation. It follows from the fact that any nonmonotonic consequence relation can be obtained as a preferential semantics derived from a monotonic consequence relation. Secondly, it is shown how to use the semantics to give an LDS formulation to a logic. In the last stage, it is shown how to find such semantics automatically and hence formulate the corresponding LDS.
The eighth chapter extends the Curry-Howard interpretation to LDS. The basic tool arises from the fact that exiting a metabox in LDS terminology corresponds to \(\lambda\)-abstraction in the Curry-Howard methodology.
In many applications one is interested in the notion of \(\Delta \vdash B\), where we want to ignore the labels and just give a yes or no answer to the query “Does \(B\) follow from \(\Delta\)?” In such a case we are actually hiding the labels and all we have is a structured database \(\Delta\) proving or not proving a formula \(B\). We can define axiomatically the properties of the consequence \(\Delta \vdash B\) and thus end up with a notion of consequence between \(\Delta\) and \(B\), where \(\Delta\) is structured and the labels in \(\Delta\) are hidden and used only in the proof system. This simplified notion can be developed on its own as a direct extension of the notion of monotonic consequence relation. On the other hand, many nonmonotonic databases and assumptions of a nonmonotonic consequence relation are naturally structured. Thus the notion structured consequence relation arises immediately in this context. A general theory of structured consequence relations is developed in the ninth chapter.
The tenth chapter, entitled “Labelled analytic deduction”, presents tableaux methodology for LDS, based on a paper of M. D’Agostino and the author [J. Autom. Reasoning 13, 243-281 (1994; Zbl 0816.03012)].
The last chapter is devoted to an intuitive theory of abduction within the framework of LDS. The two starting points in this consideration are that abduction depends on proof procedures and that a declarative item of data can be either a labelled formula or a principle of abduction.
The whole exposition has been permeated with instructive, interesting and witty examples. The book opens a number of new interesting model-theoretic, proof-theoretic and foundational questions and seems to be a reasonable basis for new further investigations, interesting not only to those engaged in logic or the philosophy of mathematics, but also to those who work in the fields of expert systems, fuzzy systems, artificial intelligence etc. Undoubtedly, this will be one of the inspiring sources motivating others to work in those fields.