No label defined (Q4484080)

Preface: The purpose of this work is to study the method of syntactic refutations in certain important nonclassical propositional logics. Chapter 1 is introductory. We present basic concepts, notably that of a refutation rule, and describe the essentials of Scott's method of proving syntactic completeness. We also discuss general aspects of syntactic refutations and formulate some interesting formal problems concerning refutation rules for nonclassical logics. In Chapter 2 we start a systematic exposition of the method of syntactic refutations in the intuitionistic propositional logic. It is essentially Scott's method but we slightly modify it and present a uniform normal form procedure that may be applied to other nonclassical logics. In Chapter 3 we turn the syntactic completeness proof into a semantic one by constructing models out of syntactic refutation trees. This also gives us a new constructive proof of the fact that INT is characterized by the Jaśkowski trees. In Chapter 4 we obtain some standard algebraic characterizations of INT as corollaries of the results in Chapter 2. We also show that Jaśkowski's construction \(+\) of adding a new unit element is characteristic for INT. Thus we obtain constructive proofs of several standard results about INT by using the simple concept of a refutation rule. Chapter 5 is devoted to syntactic characterizations of INT. First we describe Yankov-style characteristic formulas and remark that they provide refutation systems for all intermediate logics with the finite model property. Then we introduce some characteristic formulas corresponding to Jaśkowski's construction \(+\) and we use them for finding a kind of disjunction property that is characteristic for INT. This also gives us a new proof of the fact that Kleene's property characterizes INT. The remaining chapters are devoted to the modal logic S4 and Grzegorczyk's logic, which are important modal systems. We present a solution to the difficult problem of a complete syntactic refutation procedure for S4. Our technique seems to work rather well in normal extensions of S4. In a smooth way it generates semantic, algebraic, and syntactic characterizations of S4 and Grz. Moreover, in Chapter 7 we establish some specific refutation rules that are valid in S4 and provide rapid refutation procedures for classes of formulas. And in Chapter 9 we introduce certain sequential refutation systems that provide a refutation system for every normal modal logic with the finite model property. In this work the standard definitions and facts we need are given without references. The remaining results are either new or based on the author's articles indicated in the bibliography. In particular, the chapters 3, 4, 7, 8, 10 are completely new. And in the chapters 2, 5, 6, 9 the presentation and the proofs are new. Finally, we wish to emphasize that in this work we study refutation rules as a formal tool for characterizing specific propositional logics and from these syntactic characterizations we generate surprisingly many standard results about these logics. But we do not study abstract theories connected with refutations.