| |
| |
| |
| Propositional Logic from the Viewpoint of Analytic Tableaux | |
| |
| |
| |
| Preliminaries    | |
| |
| |
| |
| Foreword on Trees    | |
| |
| |
| |
| Formulas of Propositional Logic    | |
| |
| |
| |
| Boolean Valuations and Truth Sets | |
| |
| |
| |
| Analytic Tableaux    | |
| |
| |
| |
| The Method of Tableaux    | |
| |
| |
| |
| Consistency and Completeness of the System | |
| |
| |
| |
| Compactness    | |
| |
| |
| |
| Analytic Proofs of the Compactness Theorem    | |
| |
| |
| |
| Maximal Consistency: Lindenbaum's Construction    | |
| |
| |
| |
| An Analytic Modification of Lindenbaum's Proof    | |
| |
| |
| |
| The Compactness Theorem for Deducibility | |
| |
| |
| |
| First-Order Logic | |
| |
| |
| |
| First-Order Logic | |
| |
| |
| Preliminaries    | |
| |
| |
| |
| Formulas of Quantification Theory    | |
| |
| |
| |
| First-Order Valuations and Models    | |
| |
| |
| |
| Boolean Valuations vs. First-Order Valuations | |
| |
| |
| |
| First-Order Analytic Tableaux    | |
| |
| |
| |
| Extension of Our Unified Notation    | |
| |
| |
| |
| Analytic Tableaux for Quantification Theory    | |
| |
| |
| |
| The Completeness Theorem    | |
| |
| |
| |
| The Skolem-Lowenheim and Compactness Theorems for First-Order Logic | |
| |
| |
| |
| A Unifying Principle    | |
| |
| |
| |
| Analytic Consistency    | |
| |
| |
| |
| Further Discussion of Analytic Consistency    | |
| |
| |
| |
| Analytic Consistency Properties for Finite Sets | |
| |
| |
| |
| The Fundamental Theorem of Quantification Theory    | |
| |
| |
| |
| Regular Sets    | |
| |
| |
| |
| The Fundamental Theorem    | |
| |
| |
| |
| Analytic Tableaux and Regular Sets    | |
| |
| |
| |
| The Liberalized Rule D | |
| |
| |
| |
| Axiom Systems for Quantification Theory    | |
| |
| |
| |
| Foreword on Axiom Systems    | |
| |
| |
| |
| The System Q subscript 1    | |
| |
| |
| |
| The Systems Q subscript 2, Q* subscript 2 | |
| |
| |
| |
| Magic Sets    | |
| |
| |
| |
| Magic Sets    | |
| |
| |
| |
| Applications of Magic Sets | |
| |
| |
| |
| Analytic versus Synthetic Consistency Properties    | |
| |
| |
| |
| Synthetic Consistency Properties    | |
| |
| |
| |
| A More Direct Construction | |
| |
| |
| |
| Further Topics in First-Order Logic | |
| |
| |
| |
| Gentzen Systems    | |
| |
| |
| |
| Gentzen Systems for Propositional Logic    | |
| |
| |
| |
| Block Tableaux and Gentzen Systems for First-Order Logic | |
| |
| |
| |
| Elimination Theorems    | |
| |
| |
| |
| Gentzen's Hauptsatz    | |
| |
| |
| |
| An Abstract Form of the Hauptsatz    | |
| |
| |
| |
| Some Applications of the Hauptsatz | |
| |
| |
| |
| Prenex Tableaux    | |
| |
| |
| |
| Prenex Formulas    | |
| |
| |
| |
| Prenex Tableaux | |
| |
| |
| |
| More on Gentzen Systems    | |
| |
| |
| |
| Gentzen's Extended Hauptsatz    | |
| |
| |
| |
| A New Form of the Extended Hauptsatz    | |
| |
| |
| |
| Symmetric Gentzen Systems | |
| |
| |
| |
| Craig's Interpolation Lemma and Beth's Definability Theorem    | |
| |
| |
| |
| Craig's Interpolation Lemma    | |
| |
| |
| |
| Beth's Definability Theorem | |
| |
| |
| |
| Symmetric Completeness Theorems    | |
| |
| |
| |
| Clashing Tableaux    | |
| |
| |
| |
| Clashing Prenex Tableaux    | |
| |
| |
| |
| A Symmetric Form of the Fundamental Theorem | |
| |
| |
| |
| Systems of Linear Reasoning    | |
| |
| |
| |
| Configurations    | |
| |
| |
| |
| Linear Reasoning    | |
| |
| |
| |
| Linear Reasoning for Prenex Formulas    | |
| |
| |
| |
| A System Based on the Strong Symmetric Form of the Fundamental Theorem | |
| |
| |
| References | |
| |
| |
| Subject index | |