Abstract
Traditional logics manipulate formulas.
The message of this book is to manipulate pairs;
formulas and labels. The labels annotate the formulas. This sounds very simple
but it turned out to be a big step, which makes a serious difference, like the
difference between using one hand only or allowing for the coordinated use of
two hands. Of course the idea has to be made precise, and its advantages and
limitations clearly demonstrated. `Precise' means a good mathematical
definition and `advantages demonstrated' means case studies and applications in
pure logic and in AI.
To achieve that we need to address the following:
\begin{enumerate}
\item Define the notion of {\em LDS}, its proof theory and semantics and relate
it to traditional logics.
\item Explain what form the traditional concepts of cut elimination, deduction
theorem, negation, inconsistency, update, etc.\ take in {\em LDS}.
\item Formulate major known logics in {\em LDS}. For example, modal and
temporal logics, substructural logics, default, nonmonotonic logics, etc.
\item Show new results and solve long-standing problems using {\em LDS}.
\item Demonstrate practical applications.
\end{enumerate}
This is what I am trying to do in this book. Part I of the book is an
intuitive presentation of {\em LDS} in the context of traditional current views
of monotonic and nonmonotonic logics. It is less oriented towards the pure
logician and more towards the practical consumer of logic. It has two tasks,
addressed in two chapters.
These are:
\begin{itemlist}{Chapter 1:}
\item [Chapter1:] Formally motivate {\em LDS} by starting from the traditional
notion of `What is a logical system' and slowly adding features to it until it
becomes essentially an {\em LDS}.
\item [Chapter 2:] Intuitively motivate {\em LDS} by showing many examples
where labels are used, as well as some case studies of familiar logics (e.g.\
modal logic) formulated as an {\em LDS}.
\end{itemlist}
The second part of the book presents the formal theory of {\em LDS} for the
formal logician. I have tried to avoid the style of definition-lemma-theorem
and put in some explanations. What is basically needed here is the formulation
of the mathematical machinery capable of doing the following.
\begin{itemize}
\item Define {\em LDS} algebra, proof theory and semantics.
\item Show how an arbitrary (or fairly general) logic, presented traditionally,
say as a Hilbert system or as a Gentzen system, can be turned into an {\em LDS} formulation.
\item Show how to obtain a traditional formulations (e.g.\ Hilbert) for an
arbitrary {\em LDS} presented logic.
\item Define and study major logical concepts intrinsic to {\em LDS} formalisms.
\item Give detailed study of the {\em LDS} formulation of some major known logics (e.g.\
modal logics, resource logics) and demonstrate its advantages.
\item Translate {\em LDS} into classical logic (reduce the `new' to the `old'),
and explain {\em LDS} in the context of classical logic (two sorted logic,
metalevel aspects, etc).
\end{itemize}
\begin{itemlist}{Chapter 1:}
\item [Chapter 3:] Give fairly general definitions of some basic concepts of {\em
LDS} theory, mainly to cater for the needs of the practical consumer of logic
who may wish to apply it, with a detailed study of the metabox system.
The presentation of Chapter 3 is a bit tricky. It may be too formal for the
intuitive reader, but not sufficiently clear and elegant for the mathematical
logician. I would be very grateful for comments from the readers for the next
draft.
\item [Chapter 4:] Presents the basic notions of algebraic {\em LDS}. The
reader may wonder how come we introduce algebraic {\em LDS} in chapter 3 and
then again in chapter 4. Our aim in chapter 3 is to give a general definition
and formal machinery for the applied consumer of logic. Chapter 4 on the other
hand studies {\em LDS} as formal logics. It turns out that to formulate an
arbitrary logic as an {\em LDS} one needs some specific labelling algebras and
these need to be studied in detail (chapter 4). For general applications it is
more convenient to have general labelling algebras and possibly mathematically
redundant formulations (chapter 3). In a sense chapter 4 continues the topic of the
second section of chapter 3.
\item [Chapter 5:] Present the full theory of {\em LDS} where labels can be
databases from possibly another {\em LDS}. It also presents Fibred Semantics for
{\em LDS}.
\item [Chapter 6:] Presents a theory of quantifers for {\em LDS}. The material
for this chapter is still under research.
\item [Chapter 7:] Studies structured consequence relations. These are logical
system swhere the structure is not described through labels but through some
geometry like lists, multisets, trees, etc. Thus the label of a wff $A$ is
implicit, given by the place of $A$ in the structure.
\item [Chapter 8:] Deals with metalevel features of {\em LDS} and its
translation into two sorted classical logic.
\end{itemlist}
Parts 3 and 4 of the book deals in detail with some specific families of logics.
Chapters 9--11 essentailly deal with substructural logics and their variants.
\begin{itemlist}{Chapter10:}
\item [Chapter 9:] Studies resource and substructural logics in general.
\item [Chapter 10:] Develops detailed proof theory for some systems as well as
studying particular features such as negation.
\item [Chapter 11:] Deals with many valued logics.
\item [Chapter 12:] Studies the Curry Howard formula as type view and how it
compres with labelling.
\item [Chapter 13:] Deals with modal and temporal logics.
\end{itemlist}
Part 5 of the book deals with {\em LDS} metatheory.
\begin{itemlist}{Chapter15:}
\item [Chapter 14:] Deals with labelled tableaux.
\item [Chapter 15:] Deals with combining logics.
\item [Chapter 16:] Deals with abduction.
\end{itemlist}
