Provability, Computability and Reflection (eBook)

Front Cover 1
Solvable Cases of the Decision Problem 4
Copyright Page 5
CONTENTS 6
CHAPTER I. VALIDITY AND SATISFIABILITY IN FINITE DOMAINS 10
1. Well-formed formulas 10
2. Valuation of well-formed formulas in a finite domain. Validity and satisfiability 13
CHAPTER II. THE DECISION PROBLEM 18
1. Valuation in arbitrary domains. Universal validity 18
2. Equivalences 21
3. S-formulas. Elimination of the propositional variables 24
4. Normal forms 28
5. Three forms of the decision problem 31
CHAPTER III. SOLUTION OF THE DECISION PROBLEM FOR EQUALITY FORMULAS 33
1. Solution of the form II of the decision problem 33
2. Another criterion for the universal validity of equality formulas 35
CHAPTER IV. SOLUTION OF THE DECISION PROBLEX FOR WELL- FORMED FORMULAS CONTAINING ONLY MONADIC PREDICATE VARIABLES 43
1. Solution of the form II of the decision problem for wffs which do not contain bound predicate variables and the sign of equality 43
2. Elimination theorems 46
3. General solution of the decision problem for wffs with only monadic predicate variables 50
CHAPTER V. SOME GENERAL THEOREMS ABOUT THE VALIDITY OF FORMULAS OF THE PREDICATE CALCULUS OF FIRST ORDER INCLUDING EQUALITY 57
1. Skolem’s normal form 57
2. Theorems about the validity of wffs not containing the sign of equality 59
3. Theorems about the validity of wffs which may contain the sign of equality 61
CHAPTER VI. SOLUTION OF THE DECISION PROBLEM FOR WFFS WITH SPECIAL PREFIXES 69
1. Remarks on the selection of special cases of the decision problem 69
2. Solution for wffs having prefixes consisting solely of universal quantifiers 71
3. Solution for wffs having prefixes consisting solely of existential quantifiers 72
4. Reduction of the decision problem for wffs with certain prefixes to that for wffs with simpler prefixes 76
5. Solution for wffs having prefixes such that all the universal quantifiers precede all the existential ones 79
CHAPTER VII. FURTHER CLASSES OF PREFIXES FOR WHICH THE DECISION PROBLEM CAN BE SOLVED 81
1. Solution for wffs having prefixes containing only one existential quantifier 81
2. Solution for wffs having prefixes containing only two existential quantifiers which are not separated by universal quantifiers 84
CHAPTER VIII. GENERAL REMARKS ABOUT FURTHER INVESTIGATIONS 92
1. Limitation of the range of the method hitherto used 92
2. Some other cases for which the decision problem has been solved 94
3. A general theorem about the validity of wffs 99
CHAPTER IX. THE DECISION PROBLEM FOR WFFS WITH FUNCTIONAL VARIABLES 107
1. Introduction of wffs with functional variables 107
2. Special cases for which the decision problem is solved for wffs with functional variables 109
BIBLIOGRAPHY 117
INDEX 122