Goal-directed proof theory

Publication date 25 February 2002

Published in Applied Logic Series (Search for Journal in Brave)

backwards proofs goal-directed proof Kripke models proof systems propositional calculus

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Abstract deductive systems (03B22) Proof theory in general (including proof-theoretic semantics) (03F03)

Review text

Goal-directed proofs are what we, humans, do naturally. Facing the task \(\Gamma\overset {?} \vdash {A} B\), i.e. to know whether \(A\to B\) follows from \(\Gamma\), you immediately reduce it to \(\Gamma,A\overset {?}\vdash B\), and to \(\Gamma\overset{?}\vdash C\) when \(A\) is \(C\to B\), and further and further backwards. You don't put \(\bigwedge \bigwedge\Gamma\wedge\neg(A\to B)\) in a normal form first and then look for a resolution or whatever, as machines do. (Or do you?) In this monograph, the authors formulate and systematize this human way of backwards proofs. They state, outright, that it ``contains the beginnings of our research program and ``is directed to researchers, undergraduate or gradute students with some knowledge of logic. Indeed, this is just a beginning, as they consider propositional calculus almost exclusively, and implicational fragments at that, but they do quite a number of logical systems. They start from classical and intuitionistic logics, then intermediate ones (bounded heights, Dummett's LC), and about ten each of modal and of substructural logics (K, S4; Lambek calculus, relevant and linear logics). The general format of proof systems consists of success \((\Gamma\overset{?}\vdash A\) is a success if \(A\) is in \(\Gamma\)), implication, reduction (see the second sentence above), and restart. The restart rule is used, for instance, to handle the disjunction in intuitionism. From \(\Gamma\overset{?}\vdash A\vee B\), one steps to \(\Gamma\overset{?}\vdash A\) or \(\Gamma\overset{?}\vdash B\). But which one to work with, first? To keep track of what's going on, the authors attach labels to formulas and keep one disjunct in `history'. When the proof process gets stuck, one can restart by working on a formula in history if it bears an appropriate label. On the semantical side, the authors introduce Kripke models and their variants, and show soundness and completeness of their proof systems, by making canonical models after proving the admissibility of the cut rule. Of course, the descriptions given here are very crude. The authors offer taylor-made versions of definitions, procedures, etc. for the situation at hand. For instance, formulations of the cut rule for some substructural logics are quite an art. The \((\forall,\to)\)-fragment of intuitionistic logic is the only case where quantifiers are considered. There, Skolem functions and unifications are used. In connection with LC, Avon's hypersequents are introduced. Intuitionistic versions of modalities require families of Kripke models arranged in appropriate ways. Efficiency and decidability of a proof procedure are touched upon here and there. So are Harrop and Horn formulas. This is an enjoyable book: good explanation, a lot of examples, clear organization, good guide to the literature, open problems, and conjectures to be checked. Introduction and Conclusions give the nature and the perspective of the work. On the negative side, there are a number of careless misprints, etc., and the index is skimpy. Since the same words (database, restart) denote different things according to the context, it would have been helpful to have had some good tables, charts, etc., that summarize and compare definitions, systems and so forth.

Recommendations

Cited in

(24)

This page was built for publication: Goal-directed proof theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5956945)