# schutte-proof theory

下载积分：850

内容提示： Grundlehren der mathematischen Wissenschaften 225 A Series of Comprehensive Studies in Mathematics Editors S. S. Chern J. L. Doob J. Douglas, jr. A. Grothendieck E. Heinz F. Hirzebruch E. Hopf S. Mac Lane W. Magnus M. M. Postnikov W. Schmidt D. S. Scott K. Stein J. Tits B. L. van der Waerden Managing Editors B. Eckmann J. K. Moser Kurt Schutte Proof Theory Translation from the German by J. N. Crossley Springer-Verlag Berlin Heidelberg New York 1977 Kurt Schutte Mathematisches Institut, Ludwig-Maximil...

文档格式：PDF|
浏览次数：2|
上传日期：2015-04-08 10:18:00|
文档星级：

**********
Grundlehren der mathematischen Wissenschaften 225 A Series of Comprehensive Studies in Mathematics Editors S. S. Chern J. L. Doob J. Douglas, jr. A. Grothendieck E. Heinz F. Hirzebruch E. Hopf S. Mac Lane W. Magnus M. M. Postnikov W. Schmidt D. S. Scott K. Stein J. Tits B. L. van der Waerden Managing Editors B. Eckmann J. K. Moser
Kurt Schutte Proof Theory Translation from the German by J. N. Crossley Springer-Verlag Berlin Heidelberg New York 1977
Kurt Schutte Mathematisches Institut, Ludwig-Maximilians-Universitat, 8000 Munchen 2/Germany Translator: J. N. Crossley Department of Mathematics, Monash University, Clayton, Victoria 3168/ Australia Translation of the revised version of "Beweistheorie", 1 st edition, 1960; Grundlehren der mathematischen Wissenschaften, Band 103 AMS Subject Classification (1970): 02B 10, 02B99, 02C 15, 02Dxx, 02E99, ION99 ISBN-13: 978-3-642-66475-5 DOl: 10.1007/978-3-642-66473-1 e-ISBN-13: 978-3-642-66473-1 Library of Congress Cataloging in Publication Data. Schutte, KUTt. Proof theory. (Grundlehren def mathematischen Wissenschaften; 225). Translation of Beweistheorie. Bibliography: p. index. I. Proof theory. I. Title. II. Series: Die Grundlehren dec mathematischen Wissenschaften in Einzeldarstellungen; 225. QA9.54.S3813. 511'.3. 76-45768. This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically those of translation. reprinting, re-use of illustrations, broadcasting, reproduction by photocopying machine or similar means, and storage in data banks. Under §54 of the German Copyright Law where copies are made for other than private use, a fee is payable to the publisher, the amount of the fee to be determined by agreement with the publisher. Includes © by Springer-Verlag Berlin Heidelberg 1977. Softcover reprint of the hardcover 1st edition 1977 2141/314()-543210
Preface This book was originally intended to be the second edition of the book "Beweis-theorie" (Grundlehren der mathematischen Wissenschaften, Band 103, Springer 1960), but in fact has been completely rewritten. As well as classical predicate logic we also treat intuitionistic predicate logic. The sentential calculus properties of classical formal and semiformal systems are treated using positive and negative parts of formulas as in the book "Beweistheorie". In a similar way we use right and left parts of formulas for intuitionistic predicate logic. We introduce the theory of functionals of finite types in order to present the Gi:idel interpretation of pure number theory. Instead of ramified type theory, type-free logic and the associated formalization of parts of analysis which we treated in the book "Beweistheorie", we have developed simple classical type theory and predicative analysis in a systematic way. Finally we have given consistency proofs for systems of l I ~ - a n a l y s i s following the work of G. Takeuti. In order to do this we have introduced a constni'ctive system of notation for ordinals which goes far beyond the notation system in "Beweistheorie". My hearty thanks are due to Professor J. N. Crossley for his translation of my German manuscript and for his careful checking of the proof sheets. I also wish to thank Dr. W. Pohlers and Dr. W. Buchholz for the help which they have given me technically and also in reading the proofs. I would especially like to thank Frau Ernst (Munich) and Ms. Vandenberg (Monash University) for their very careful typing of the text. I wish to thank Springer-Verlag for their kindness and help in the production of the book. Munich, March 1977 Kurt Schutte
Table of Contents Introduction . 1 Part A. Pure Logic 5 Chapter 1. Fundamentals 7 § 1. Classical Sentential Calculus . 1. Truth Functions 2. Sentential Forms . 3. Complete Systems of Connectives 4. A Formal Language for the Sentential Calculus 5. Positive and Negative Parts of Formulas 6. Syntactic Characterization of Valid Formulas 7 7 8 8 9 10 12 § 2. Formal Systems 1. Fundamentals . 2. Deducible Formulas 3. Permissible Inferences . 4. Sentential Properties of Formal Systems. 5. The Formal System CS of the Classical Sentential Calculus 13 13 14 15 16 17 Chapter II. Classical Predicate Calculus 19 § 3. The Formal System CP . 1. Primitive Symbols . 2. Inductive Definition of the Formulas 3. P-Forms and N-Forms 4. Positive and Negative Parts of a Formula 5. Axioms. 6. Basic Inferences 19 19 20 . 20 20 20 20 § 4. Deducible Formulas and Permissible Inferences 1. Generalizations of the Axioms 2. Weak Inferences 3. Further Permissible Inferences 4. Defined Logical Connectives. 21 21 22 24 25
VIn § 5. Semantics of Classical Predicate Calculus 1. Classical Models 2. The Consistency Theorem. 3. The Completeness Theorem 4. The Satisfiability Theorem 5. Syntactic and Semantic Consequences Chapter III. Intuitionistic Predicate Calculus . § 6. Formalization of Intuitionistic Predicate Calculus. 1. The Formal System IPI 2. The Formal System IP2 3. Left and Right Parts of Formulas 4. The Formal System IP3 Table of Contents 26 27 28 28 32 35 36 36 36 38 39 40 § 7. Deducible Formulas and Permissible Inferences in the System IP3 1. Generalizations of the Axioms 2. Weak Inferences 3. More Permissible Inferences . 4. Special Features of Intuitionistic Logic 5. Properties of Negation. '. 6. Syntactic Equivalence . 42 42 42 44 46 47 47 § 8. Relations between Classical and Intuitionistic Predicate Calculus 1. Embedding IP3 in CP . 2. Interpretation of CP in IP3 48 48 49 § 9. The Interpolation Theorem . 1. Interpolation Theorem for the System IP3 2. Interpolation Theorem for the System CP 3. Finitely Axiomatisable Theories 4. Beth's Definability Theorem . Chapter IV. Classical Simple Type Theory. § 10. The Formal System CT 1. The Formal Language. 2. Chains of Subterms 3. Axioms and Basic Inferences 4. Deducible Formulas and Permissible Inferences 5. The Cut Rule § 11. Deduction Chains and Partial Valuations 1. Definition of Deduction Chains 2. Partial Valuations . 3. Principal Lemmata. § 12. Semantics . 1. Total Valuations over a System of Sets 2. Soundness Theorem 51 51 54 54 55 56 56 56 57 60 60 62 62 62 63 64 65 65 66
Table of Contents 3. Extending a Partial Valuation 4. Completeness Theorem and Cut Rule Part B. Systems of Arithmetic Chapter V. Ordinal Numbers and Ordinal Terms. IX 67 69 71 73 § 13. Theory of Ordinals of the 1st and 2nd Number Classes 1. Order Types of Well-Ordered Sets 2. Axiomatic Characterization of the 1st and 2nd Number Classes 3. Zero, Successor and Limit Numbers and Supremum 4. Ordering Functions 5. Addition of Ordinals . 6. a-Critical Ordinals . 7. Maximal a-Critical Ordinals 73 73 74 75 76 79 81 84 § 14. A Notation System for the Ordinals <To 1. Definition of Ordinal Terms . 2. The Ordering of the Ordinal Terms 3. Addition of Ordinal Terms 4. Ordinal Terms cPaf3. 5. Ordinal Terms wa, wa·n and wa.f3 . 6. Ordinal Terms n·f3, 2a and 2a.f3 7. Ordinal Terms Ca' wn(a) and (n 8. A Mapping onto the Natural Numbers Chapter VI. Functionals of Finite Type § 15. The System of Terms of Finite Type. 1. Types 2. Terms 3. Interpretation 4. Reduction Procedure for Terms 5. Characterization of Numerals 6. Substitution Properties 7. The Normal Form of a Term . § 16. Orders of Terms 1. Natural Sum and Natural Product of Ordinal Terms 2. Assigning Ordinal Terms to Terms 3. Estimates of the Order of Terms . 4. Equality of Terms . § 17. The Formal System FT of Functionals of Finite Type. 1. The Formal Language. 2. Deduction Procedures . 3. The Consistency of the System FT 4. Fundamental Deduction Rules 86 86 88 89 90 92 94 95 96 98 98 98 98 99 100 101 101 104 105 105 106 108 112 113 113 114 115 117
x Table of Contents 5. Addition and Multiplication . 6. The Indentity Functional I, and A-Abstraction . 7. The Predecessor Functional and the Arithmetic Difference 8. The Recursor . 9. Simultaneous Recursion . 10. The Characteristic Term of a Basic Formula 120 121 122 124 126 129 Chapter VII. Pure Number Theory. 134 § 18. The Formal System PN for Pure Number Theory. 1. The Formal Language. 2. The Deduction Procedure. 3. Basic Properties of Deducibility 4. Properties of Negation. 5. Positive and Negative Parts of Formulas 6. The Consistency of the System PN . 134 134 135 136 138 142 147 § 19. Interpretation of PN in FT . 1. Sequences of Terms of the System FT 2. The Formal System QFT . 3. Interpreting Formulas. 4. Interpretations of the Axioms of the System PN 5. Interpretations of the Basic Inferences in the System PN 148 148 149 155 157 158 Part C. Subsystems of Analysis . 165 Chapter VIII. Predicative Analysis. 167 § 20. Systems of L l ~ - A n a l y s i s 1. The Formal Language of Second Order Arithmetic 2. The Formal System DA . 3. Deducible Formulas and Permissible Inference of the System DA 4. The Semi-Formal System DA * 5. Embedding DA in DA * 6. General Properties of Deduction in the System DA * 7. Subsystems ofDA and DA* . 167 167 170 171 174 175 176 176 § 21. Deductions of Transfinite Induction. 1. Formalisation of Transfinite Induction 2. Deductions in EN . 3. Deductions in EN*. 4. Deductions in EA and EA* 5. The Formula ~6. Deductions in DA . 7. Deductions in DA* 177 177 179 181 182 184 188 192 [P, Q, t] § 22. The Semi-Formal System RA* for Ramified Analysis. 1. The Formal Language. 197 197
Table of Contents Xl 2. The Deduction Procedures 3. Weak Inferences 4. Elimination of Cuts 5. Further Properties of Deductions 6. Interpretations of EA * and DA * in RA * 200 201 201 204 207 § 23. The Limits of the Deducibility of Transfinite Induction 1. Orders of Deductions of Induction in RA * . 2. The Limiting Numbers of the Systems EN, EA and DA 3. The Autonomous Ordinal Terms of the Systems EN*, EA* and DA* . 4. The Autonomous Ordinal Terms of the System RA * 5. The Limits of Predicativity 209 209 211 213 217 220 Chapter IX. Higher Ordinals and Systems of 1 I ~ - A n a l y s i s 221 § 24. Normal Functions on a Segment 0* of the Ordinals 1. Axiomatic Characterization of the Segment 0* of the Ordinals 2. Basic Properties of 0* . 3. Definition of the Functions (Jrx 4. Properties of the (J Functions . 5. The Sets In(a) and Functions {}rx 221 221 222 224 225 230 § 25. A Notation System for Ordinals Based on the (Jrx Functions 1. The Set {}(Q) of Ordinals . 2. Sets of Coefficients . 3. The Systems T* and OT* of Terms 4. Subsystems {}(r) of {}(Q) 5. The Ordinal Ao . 6. Relations between Cr (a) and In (a) 234 234 234 236 238 239 240 § 26. Level-Lowering Functions of the Ordinals. 1. Basic Concepts . 2. Properties of the Sets of Coefficients . 3. The Ordinal Term dia 4. The Natural Sum . 5. Deduction Functions 241 242 242 245 248 248 § 27. The Formal System GPA for a Generalized 1 I ~ - A n a l y s i s . 1. The Formal Language. 2. Axioms, Basic Inference and Substitution Inferences 3. Deductions. 4. Orders of Normal Deductions 5. Transformations of Normal Deductions. 6. Reducible Normal Deductions 7. Singular Normal Deductions. 8. Reduction of a Suitable Cut . 9. The Consistency of the System GPA. 10. The Subsystem PA of GPA . 252 252 253 255 257 258 259 261 262 268 268
xu Table of Contents § 28. The Semi-Formal System PA* I. Axioms and Basic Inferences of the System PA * 2. The Strength of a Formula 3. Basic Deductions in the System PA*. 4. Embedding ofPA in PA* . 5. Elimination of Strong Cuts in PA * . 6. Normal Deductions in the System PA* 7. Reducible Normal Deductions 8. Elimination of Cuts in PA* 269 269 270 271 272 273 275 277 278 § 29. Proof of Well-Ordering . I. A Constructive Proof of Well-Ordering for Subsystems of B(Q) 2. The Formal System IDn of n-Fold Iterated Inductive Definitions. 285 3. Formalization of the Proof of Well-Ordering of B(N) in IDN 4. Embedding IDn in a Subsystem of PA 281 281 287 .. 289 Bibliography . 293 Subject Index . 297
Introduction In mathematics, dealing with infinite number systems and other infinite sets brings a fundamental problem with it. For example consider the two statements: I. Every even number greater than 2 can be represented as the sum of two primes. II. There is an even number which is greater than 2 but cannot be represented as the sum of two primes. According to classical logic the second statement is the contradictory of state-ment I. So far neither of these two statements can be proved. We cannot prove statement I by testing its validity for all even numbers since there are infinitely many such numbers. In order to prove statement I we must rather solve the following problem: (I) To give a general procedure which assigns to each even number g > 2 two primes peg) and q(g) such that the equation g = peg) + q(q) is satisfied for all g > 2. If one does not succeed in solving this problem then one must attempt to prove the opposite statement, II. Then one is dealing with an existential statement. If one takes the existential question seriously then in order to prove statement II one must solve the following problem: (II) To give an even number go> 2 which one can recognize as not being repre-sentable as the sum of two prime numbers. We now ask whether either of the two statements I and II is fundamentally correct. Now the correctness of a mathematical statement can only be determined by a proof. There is no sense in accepting a mathematical truth which is not possibly provable. So we can only ask whether one of statements I and II is provable in principle. If one says this question is solvable in the affirmative then one must be certain that one of problems (I) or (II) really is solvable. But such certainty is not attainable. In fact one cannot even deduce from the assumption that problem (I) is unsolvable that a number go, which satisfies problem II, can actually be shown to exist. Neither can one deduce, from the assumption that problem (II) is unsolvable, that there is a general procedure for solving problem (I).
2 Introduction We therefore have no grounds for assuming that one of the two statements I and II is correct. The assumption would only be justified if a proof of I or II were given. But then the general situation regarding the provability of mathematical propositions would not be altered since there are always other cases where the question Of provability of a statement or its contradictory remains open. Therefore there is no immediate sense in saying that the principle of Tertium non datur, which says that either a proposition or its logical contradictory is correct, be accepted as satisfactory for mathematical propositions. This brief critique of Tertium non datur leads us to the basic problem of proof theory. We start from the premise that in mathematics Tertium non datur is not meaningful as a general basic principle. But if one gives up this principle as a method of proof then one loses the right to indirect proof procedures such as one cannot do without in classical mathematics. In order to guarantee the correctness of classical mathematics in a logically unobjectionable way there only remains the possibility of basing mathematical statements not on provability as such hut on formal deducibility. This deducibility which may be regarded as a notional provability must be given axiomatically so that it is sufficient for the basic theorems of classical mathematics. In this way one does not need to interpret the concept of deducibility in a meaningful way, but only to establish its formal admissibility by means of a consistency proof. This is in fact Hilbert's programme: to establish the consistency of mathematics in its classical form. Hilbert called the theory which solves this problem proof theory (Beweis-theorie). The object of a proof-theoretic investigation is a mathematical theory which is precisely determined not only by its mathematical notions and axioms but also by the basic logical concepts and modes of inference which it allows. Now one must distinguish clearly between the laws of the theory which are to be investigated and those of the theory in which the investigation is to be carried out. The notions and theorems of the theory under investigation are represented in a formal system and treated purely formally without reference to their meaning, while the proof-theoretic investigation is concerned with the logical meaning of the notions and inference modes. Thus the formal theory is complemented by a meaningful meta-theory (proof theory). This metatheory is also called "metalogic" or "meta-mathematicl'. This does not mean that one is extending the usual logic or mathe-matics, as/ts the case with metaphysics and physics. Here it only delineates the distinction between formalized mathematics and the logic in which the investigation is carried out. If proof theory is to provide a foundation for a problematic area of mathe-matics then its own methods and notions and modes of inference must be restricted to those which lie outside this problematic area. The methods which Hilbert called "finitist" (fin it) do lie outside. These consist of just elementary logical and mathematical relations of a combinatorial nature which are used as bases for all theoretical investigations and are generally acknowledged as admissible. In a finitist proof Tertium non datur may not be used for propositions concerning in-finite totalities and existential propositions are only to be treated as valid if the object whose existence is asserted can in fact be constructed. But GOOel's investigations [1] have shown that the strictest finitist methods are
Introduction 3 basically inadequate for carrying out the consistency proof required by Hilbert's programme. So proof theory needs not only the very strict finitist methods of a combinatorial nature but also higher level proof procedures. Thus we arrive at methods, first used by Gentzen [2], using induction which in fact goes beyond the usual complete (mathematical) induction but still has a constructive character. In this book we give a systematic presentation of the most important results which have so far been achieved in the pursuit of Hilbert's programme. The main emphasis is on consistency proofs but other investigations, which are closely re-lated in terms of methodology, are also carried out. We use inductive methods for the consistency proofs but do not admit Tertium non datur as a proof procedure. We need to forgo the constructive standpoint and use classical mathematics as a foundation despite its problems only for the semantic treatment of classical predi-cate calculus (§5) and classical simple type theory (§12). Likewise we first con-sider the necessary systems of ordinals (in §13 and §24) from the standpoint of classical mathematics but then (in §§14, 25 and 26) we define these and treat them constructively. As in the first edition of this book we use the notions of "positive and negative parts" as a basis for formalization in the realm of classical logic. These are a sort of generalization of the notions of "succedent and antecedent formulas" of Gentzen's sequence calculus (Sequenzenkalkul). In intuitionistic logic we use instead the weaker notions of "left and right parts of a formula". In Chapter I we collect together the general basic syntactic notions which are n<teded in the book and used for the formalization of classical propositional calculus. Chapter II treats the constructive syntax (§§3, 4) and the non-constructive semantics (§5) of classical predicate calculus. Intuitionistic predicate calculus is developed in Chapter III but only syntactically (constructively) and related to classical predicate calculus. The Interpolation Theorem proved here (§9) also yields the corresponding theorem for classical predicate calculus. In Chapter IV we first assemble the basic syntactic properties for classical simple type theory in §IO and then introduce partial valuations in §11 which are used to carry out the non-constructive proof, following M. Takahashi [I] and D. Prawitz [1], of Takeuti's Fundamental Conjecture (Eliminability of Cuts). In Chapter V we introduce a notation system for a segment of the ordinals which is used later for the treatment of pure number theory (Chapter VI) and predicative analysis (Chapter VIII). This system of notations is defined in §13 in terms of an ordinary non-constructive approach in the classical theory of ordinal numbers and then defined as a constructive system of ordinal terms in §14. In this section too we constructively prove the necessary properties of functions on ordinal terms of this system (which are needed later) in an elementary way. In Chapters VI and VII we develop the Godel interpretation of pure number theory in a system offunctionals of finite type. Following W. Howard we prove (in §16) by transfinite induction up to 60 that the functionals introduced in §15 are calculable. In §17 we introduce a formal system FT for these functionals in the context of the positive implicational calculus. To this end Chapter VII treats, in
4 Introduction §18, an obvious formal system of pure number theory, and in §19 we carry out the interpretation of this system in the .system FT. In Chapter VIII we are concerned with the predicative limits of analysis and first we develop a formal and a semi-formal system of L l ~ - a n a l y s i s whose languages are that of classical second order arithmetic and which have restricted comprehension axioms as opposed to classical mathematics. In §21 we give de-ductions of formalized transfinite induction in the spirit of S. Feferman in these systems and in subsystems of Ll ~ - a n a l y s i s . In §22 we introduce a semi-formal system for ramified analysis in which the system of L l ~ - a n a l y s i s can be interpreted. This yields the limits for the deducibility of transfinite induction for the formal and semi-formal systems considered and demonstrates the predicativity of these systems. In Chapter IX we prove the consistency of a formal system of lIt-analysis following a proof ofG. Takeuti [4]. For this we need a transfinite induction which goes far beyond those previously introduced. Here we do not use the ordinal dia-grams of Takeuti but a system of notations for ordinal terms based on normal functions ( ) ~ defined and studied by S. Feferman, P. Aczel and J. Bridge and con-structively characterized by W. Buchholz. Using these functions ( ) ~ which are introduced in §24 in the context of the classical theory of ordinals, we build a con-structive system of notations in §25. The necessary properties of this system of notations which are needed for the consistency proof are developed in §§25 and 26. §27 gives the consistency proof for the formal system of lIt-analysis and essentially this corresponds to the proof of Take uti but in a somewhat different way. Similarly we give a consistency prooffor a semi-formal system of lIt-analysis in §28, but this is done using a weaker transfinite induction than in §27. Finally we give construc-tive proofs of well-ordering for the systems of ordinals which we have used and their subsystems in §29.
Part A Pure Logic
Chapter I Fundamentals In mathematical logic sentences are represented by formulas. Those investigations which only depend on the formal structure of logical formulas and fixed formal rules of deduction are said to be syntactic. On the other hand those which depend on model-theoretic interpretations are said to be semantic. Syntactic investigations, which feature predominantly in proof theory, are usually carried out construc-tively whilst the semantic ones can only be carried out with constructive concepts and proof procedures in the simplest part of logic, that is, in the sentential (or propositional) calculus. In § I we start with a semantic characterization of classical sentential calculus and then develop an adequate syntax for it. In §2 we present the basic syntactic concepts which will be used in the subsequent chapters. § 1. CJassical Sentential Calculus 1. Truth Functions Truth values are denoted by t (true) andf(false). An n-place truth function is an assignment of one truth value (t or f) to each n-tuple of truth values. Classical sentential calculus can be presented semantically as the theory of these truth functions. As there are exactly 2" distinct n-tuples of truth values and each n-place truth function assigns just one of two possible values to each n-tuple there are exactly 2(2") distinct n-place truth functions. We use the following connectives as symbols for truth functions. T (verum) and .l. (falsum) denote the O-place truth functions with values T = t and .l. = f The connective. (negation) denotes the one-place truth function with values .(t)=fand '(f)=t. The connectives v (disjunction), 1\ (conjunction) and -the 2-place truth functions with values as follows: (implication) denote vet, t)= v (t,f)= v (I, t)=t, v(f,f)=f, I\(t, t)=t, I\(t,f)= 1\(1, t)= I\(f,f) =1, -(t, t) =-(1, t) =-(f,f) = t, -(t,f) = f
8 I. Fundamentals In the same way we could define arbitrarily many other connectives. But they will not be used in the sequel. 2. Sentential Forms Using connectives and sentential variables, which we denote by v, VI' V2, ••• , we construct sententialforms according to the following inductive definition: SF!. Every sentential variable is a sentential form. SF2. Every O-place connective is a sentential form. SF3. If ¢ is an n-place connective (n ~then ¢(A 1> ••• , An) is also a sentential form. Such an inductive definition, like the ones we use constantly in the sequel, is to be interpreted as follows: a string of symbols has the inductively defined property if, and only if, it can be obtained by a finite number of applications of the defining rules. I) and A I, ... , An are sentential forms Example. -( /\ (VI' v2), v (1.., ,(VI») is a sentential form since the defining rules SFI-SF3 yield the following sentential forms: I. VI and V2 by SFI, 2. 1.. by SF2, 3. ,(vd by SF3 from I, 4. /\ (VI' v2) by SF3 from I, 5. v(1.., ,(VI» by SF3 from 2 and 3, 6. -( /\ (VI' v2), v (1.., ,(VI») by SF3 from 4 and 5. The semantics of the sentential calculus are determined by sentential valua-tions. Such a valuation is an assignment V of a truth value Vv to each sentential variable v. For a given valuation Vevery sentential form A gets a truth value V A according to the following inductive definition. V I. A sentential form which is a sentential variable valone gets the truth value Vv given by the valuation V. V2. VT=t, V1..=! V3. If ¢ is an n-place connective ( n ~ I) and AI' ... , An are sentential forms, then V¢(A I, ... , An) is the truth value which the truth function represented by ¢ assigns to the n-tuple of truth values (V A I, ... , VAn). Example. For a valuation V where VVI =f and VV2 =t we have V - (/\ (VI' v2), v (1.., ,(VI))) =-( /\ (f, t), v (f, ,(f)) =-(f, v (f, t» =-(f, t) = t. :Two sentential forms A and B are said to be semantically equivalent if VA = VB for every sentential valuation V. 3. Complete Systems of Connectives A set M of connectives is said to be a complete system of connectives if to every
1. Classical Sentential Calculus 9 sentential form A there is a semantically equivalent sentential form Ball of whose connectives are in M. Theorem 1.1. The connectives --', /\ and v form a complete system of connectives. Proof Let A be an arbitrary sentential form. We prove by induction on the number of sentential variables in A that there is a sentential form B, semantically equivalent to A, in which the only connectives are --', /\ and v . I. A contains no sentential variables. Then A has the same truth value V A for every valuation V. If VA = t, then A is semantically equivalent to the sentential form v (v, --, (v». If VA =f, then A is semantically equivalent to the sentential form /\ (v, --, (v». 2. A contains the sentential variables VI' ••• , Vn ( n ~ I ) . Let Al (respectively, . A2) be the sentential form obtained from A by replacing Vn by T (respectively, 1-). By the induction hypothesis there are sentential forms B1, B2 semanticallyequi-valent to AI' A2 in which the only connectives are --', /\ and v. But then A is semantically equivalent to the sentential form v (/\ (BI' vn), /\ (B2' --, (vn))). Corollary 1.2. The connectives --, and v form a complete system of connectives. Proof Immediate from Theorem 1.1 since every sentential form /\ (A, B) is semantically equivalent to the sentential form --, (v (--, (A), --, (B»). Corollary 1.3. The connectives --, and -4 form a complete system of connectives. Proof Immediate from corollary 1.2 since every sentential form v (A, B) is semantically equivalent to the sentential form -4(--' (A), B). Corollary 1.4. The connectives 1- and -4 form a complete system of connectives. Proof Immediate from Corollary 1.3 since every sentential form --, (A) is seman-tically equivalent to the sentential form -4(A, 1-). There are many other complete systems of connectives but we shall not go into them as we shall not use them in the sequel. 4. A Formal Language for the Sentential Calculus In formalizing classical sentential calculus we need only consider connectives from a complete system of connectives since semantically equivalent sentential forms have the same logical interpretation. We now define a formal language with con-nectives 1-, --', /\, v and -4. These connectives certainly form a complete system but of course they do not form a minimal complete system of connectives. We assume we are given a countably infinite set of symbols which we call sentential variables. In fact we shall never need to consider these symbols them-selves. We shall only use syntactic symbols v, VI' V2,'" for the given symbols for
10 I. Fundamentals sentential variables. Theformulas of our formal language are given by the following inductive definition. Fl. Every sentential variable is aformula. F2. 1.. is aformula. F3. If A is a formula then IA is aformula. F4. If A and B are formulas then (A 1\ B), (A v B) and (A -formulas. Formulas may be identified with particular sentential forms where IA stands for I (A) and the 2-place connectives are placed between rather than in front of their arguments following ordinary usage. The formulas 1.., lA, (A 1\ B), (A v B) and (A _ B) are to be read "falsum", "not A", "A and B", "A or B" and "A implies B". For any valuation V every formula gets a truth value as defined for sentential forms. Accordingly we have here the following particular defining rules for V2 and V3 (from page 8): B) are also V2. V 1..=f, V3.1. If VA = t (respectively, VA = f), then V,A = f(respectively, V,A = t). V3.2. If VA = t and VB= t, then V(A 1\ B) = t. Otherwise V(A 1\ B) = f V3.3. If VA = tor VB= t, then V(A v B) = t. Otherwise V(A v B) = f V3.4. If VA=for VB=t, then V(A- B)=t. Otherwise V(A-B)=f A formula A is said to be valid if VA = t for every sentential valuation V. Given a formula A we can decide, in an elementary way, whether it is valid or whether there is a valuation under which it gets the value f Indeed there are only finitely many possible combinations of truth values for the sentential variables occurring in A and in order to decide whether A is valid we only have to compute V A for these. Our aim now is to characterize the valid formulas just by their structure and without considering valuations and then to employ such a syntactic charac-terization again for stronger logical systems where the semantics cannot be ex-pressed in as elementary and constructive a way as they can for classical sentential calculus. 5. Positive and Negative Parts of Formulas A formula A which is part of a formula Fmay have the property that the truth value VFis already determined by the truth value VA. We shall call A apositive(negative) part of Fif VA =t (VA =f) implies VF=t. Examples. A is a positive part of the formulas I lA, (A v B) and (B -negative part of the formulas lA, I(B I\A), (A -We establish a connection between the semantics and syntax of classical sen-tential calculus by using the notions of "positive" and "negative parts". We define these notions purely syntactically and without reference to valuations and then prove they have the intended semantic properties. We use certain nominal forms in order to give the syntactic definition of A) and a B).
1. Classical Sentential Calculus 11 positive and negative parts. By an n-place simple nominalform ( n ~ 1) we mean a finite string of symbols in which besides the primitive symbols of our formal language (sentential variables, connectives and round brackets) the nominal symbols *1' ... , *n occur just once. If $ is an n-place simple nominal form ( n ~ 1) and r1, ••• , rn are non-empty finite strings of symbols then $[rl' ... , rn] denotes the result of re...