First-Order Logic

Except for this preface, this study is completely self-contained. It is intended to serve both as an introduction to Quantification Theory and as an exposition of new results and techniques in &quote;analytic&quote; or &quote;cut-free&quote; methods. We use the term &quote;analytic&quote; to apply to any proof procedure which obeys the subformula principle (we think of such a procedure as &quote;analysing&quote; the formula into its successive components). Gentzen cut-free systems are perhaps the best known example of ana- lytic proof procedures. Natural deduction systems, though not usually analytic, can be made so (as we demonstrated in [3]). In this study, we emphasize the tableau point of view, since we are struck by its simplicity and mathematical elegance. Chapter I is completely introductory. We begin with preliminary material on trees (necessary for the tableau method), and then treat the basic syntactic and semantic fundamentals of propositional logic. We use the term &quote;Boolean valuation&quote; to mean any assignment of truth values to all formulas which satisfies the usual truth-table conditions for the logical connectives. Given an assignment of truth-values to all propositional variables, the truth-values of all other formulas under this assignment is usually defined by an inductive procedure. We indicate in Chapter I how this inductive definition can be made explicit-to this end we find useful the notion of a formation tree (which we discuss earlier).