A PARTIAL LOGIC OF DESCRIPTIONS by PETER J. APOSTOLI Hnrs. B. A. The University of British Columbia, November 1984 A THESIS SUBMITTED IN PATIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF ARTS in THE FACULTY OF GRADUATE STUDIES Department of Philosophy We accept this thesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA November 1986 Q Peter J. Apostoli, 1986 In p r e s e n t i n g t h i s t h e s i s i n p a r t i a l f u l f i l m e n t o f the requirements f o r an advanced degree at the U n i v e r s i t y o f B r i t i s h Columbia, I agree t h a t the L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r r e f e r e n c e and study. I f u r t h e r agree t h a t p e r m i s s i o n f o r e x t e n s i v e copying of t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by the head o f my department or by h i s or her r e p r e s e n t a t i v e s . I t i s understood t h a t copying or p u b l i c a t i o n o f t h i s t h e s i s f o r f i n a n c i a l g a i n s h a l l not be allowed without my w r i t t e n p e r m i s s i o n . Department o f "F^ 1A i I o p I The U n i v e r s i t y of B r i t i s h Columbi 1956 Main Mall Vancouver, Canada V6T 1Y3 Date G c r t . IH U K /ft-n ii Abstract Let a "partial logic" for a first order predicate language L be a formal proof-theory FT for sentences of L together with a model theoretic semantics for FT which can be considered a generalization of classical first-order Tarskian semantics in the following sense: if M is a model for FT then M is a partial function from the set of sentences of L into the set {T, F} of classical truth values such that 1) every atomic sentence of L receives exactly one truth value, and 2) if M agrees with a given Tarskian model TM on the assignment of truth values to the atomic sentences of L, then M agrees with TM everywhere M is defined. In this paper we utilize formal techniques developed by P. C. Gilmore for intensional set theories without excluded middle to present a sound and complete partial logic Pld for the first order predicate calculus with definite descriptions. Pld utilizes truth value gaps to systematically treat symbolic sentences that contain "improper" description terms, and can be seen as an acceptable formalization of the Strawsonian view that the semantic-well-formedness of a grammatically subject-predicate sentence of English presupposes the propriety of any definite description occurring as subject term therein. iii Contents Section 0: Introduction pp. 1 Section 1: The System Pld pp. 14 Section 2: A Soundness Result for Pld pp. 34 Section 3: An Alternative Logical Syntax for Pld pp.49 Section 4: Semantic Completeness for Pld pp. 59 Section 5: Corollaries to Soundness and Completeness pp. 95 Section 6: Some Remarks on the Frege - Strawson Doctrine pp. 97 Bibliography pp. 104 iv Acknowledgements Many thanks are due to the Department of Philosophy for the support I received during my Masters work. I also want to thank the people in the Department of Computer Science (in particular, Paul Gilmore and Akira Kanda) for their generosity. Special thanks are due to Dick Robinson and Howard Jackson for their speed-reading abilities. 1 Section 0: Introduction As is well known, there has been considerable debate among language philosophers concerning the proper treatment of sentences of natural language which contain improper definite descriptions. In particular, there has been heated debate over the question of whether or not grammatically subject-predicate sentences which contain improper definite descriptions as subject terms merit truth values. In contrast, logicians, although differing in their particular logistic methods for treating symbolic sentences containing "improper" description terms, have (historically) been virtually unaminous in their religious belief that all sentences of a formal description calculus should be evaluated. Indeed, Russell and Frege, although on opposte sides of the natural language debate, both offer proof-theoretic treatments of description terms which require (i.e., are sound and complete with respect to) semantics that close truth value gaps for all symbolic sentences. The purpose of this paper is to challenge the assumption that any acceptable description calculus should maintain the law of excluded middle. Utilizing formal techniques originally developed for intensional set theories without excluded middle by P.C. Gilmore in the papers "Combining Unrestricted Abstraction with Universal Quantification" [1] and "Natural Deduction Based Set Theories: A New Resolution of Old Paradoxes" [2], I present a sound and complete "partial logic of descriptions" (abbreviated as 'Pld') which systematically employs truth value gaps in the treatment of certain symbolic sentences containing improper description terms. The semantic treatment such sentences receive in Pld may be seen as a formalization of the Strawsonian [1] view that the truth evaluation of an English subject-predicate sentence which contains a definite description as subject term presupposes the propriety of that description, since the symbolic translation of such a sentence is evaluated relative to a given model of Pld only after the propriety of every description term occurring in the symbolic sentence has been established relative to the given model. By a "partial logic" for a first order predicate language L we intend a formal proof-theory FT 2 for sentences of L together with a model theoretic semantics for FT which can be considered a generalization of classical first-order Tarskian semantics in the fol lowing sense: i f M is a model for FT then M is a partial function from the set of sentences of L into the set {T, F} of classical truth values such that 1) every atomic sentence of L recieves exactly one truth value, and 2) i f M agrees with a given Tarskian model T M on the assignment of truth values to the atomic sentences of L, then M agrees with T M everywhere M is defined. Partial logics are not to be confused with many-valued logics, say, three-valued systems in which the third value is intended to represent a classical-truth-value gap, since models for such systems are total assignment functions. (Intuitively, where the recursive definition of truth for such a three-valued system assigns the third value to a sentence S on the basis of a succeeding computation, we treat such sentences S by computations which fail.) So a partial logic is simply a logical system which allows truth value gaps, and P ld is simply a partial logic for the first order identity calculus with descriptions in which certain symbolic sentences which contain description terms that lack descriptums relative to a given model M do not receive a truth value relative to M . We may characterize virtually al l other proof-theoretic treatments of descriptions (or at least the histortically important ones) as offering totalizing solutions to the problems presented by improper description terms in the sense that they are sound with respect to total models only, that is, models in which excluded middle holds. In this section we give a brief outline of the three historically important proof-theoretic solutions (i.e., those proposed by Hilbert and Bernays [1], Frege [1], [2], and Whitehead and Russell [1]) to the problem posed by improper description terms occurring in symbolic sentences and appraise the relative merits of P ld visa-vis these totalizing solutions. Then in sections 1. - 5. we set out the syntax and semantics for P ld and prove that P ld is both sound and complete. In section 6 we discuss what we cal l the "Frege-Strawson Doctrine" (F-S D), the view that grammatically singular subject-predicate sentences of a natural language that contain improper definite descriptions as subject terms have no truth value, and evaluate to what extent P ld can be said to be a formalization of that doctrine. We wi l l see that P ld treats in a natural way the thorny problem of integrating the F-S D with a general theory of truth for complex symbolic sentences. 3 Any proof-theoretic treatment of descriptions has to treat in some acceptable way the problem that the classically valid inference forms of excluded middle and existential generalization / universal specification are not (in general) intuitively sound in languages containing syntactically well-formed but semantically vacuous singular terms. The failure of existential generalization / universal specification in languages containing syntactically well-formed but semantically vacuous singular terms is self explanatory. The argument that the occurrence of improper description terms in symbolic sentences threatens the validity of excluded middle in formal systems is essentially the same as the argument that vacuous singuar terms occurring as subject terms in grammatically subject-predicate sentences of a natural language threaten the legitimacy of excluded middle for natural languages: Let the "naive" view of the semantics of grammatically singular subject-predicate sentences of a natural language be the view that the utterer of a such a sentence S utters a sentence that is true, respectively, false relative to a context of utterance C just in case the grammatical predicate of S "applies" relative to C to the object "picked out" relative to C by the subject term of S. Note that this account has the same general form as has the account usually given of the truth evaluation relative to a model M of an atomic sentence ,P(*)~' of a formal language (for simplicity, we assume rp(f)l consists of the unary predicate letter 'P' followed by singular term Y, although this restriction is not essential to the point I wish to make): ^ P(f)l is true, respectively, false, relative to M just in case the object M assigns to '( belongs, respectively, does not belong, to the set of objects that M assigns to 'P'. Now, it seems a harmless rephrasing of the naive view to say that the utterer of a grammatically singular subject-predicate sentence S of a natural language utters a sentence that is true, false relative to C just in case the subject term of S "picks out" an object relative to C and the grammatical predicate of S applies, does not apply, relative to C, to that object. In other words, it seems that the naive view of how singular subject-predicate sentence of a natural language come to have truth values (relative to a context of utterance) presupposes (Frege [1], Stawson [1]) that the subject terms of those sentences have referents (relative to that context of utterance). Similarily, we can rephrase the above account of the evaluation of the symbolic sentence ^ P(/)^ 4 relative to M as follows: ^P(0^ is true, false, relative to M just in case M assigns some object to and that object belongs, respectively, does not belong, to the set of objects that M assigns to 'P'. So it appears that the standard method of evaluating the truth of symbolic sentences A relative to a model M presupposes that the singular terms (or at least those of the primitive basis of the language) occurring in A have denotations relative to M. Of course, as Russell points out in "On Denoting" [1], we cannot simply assign an arbitrary truth value (say, False) to sentences which contain improper definite descriptions as subject terms and maintain classical negation without breaching the law of noncontradiction. Now Russell [1], explicitly states that Theory of Definite Description is intended to solve the problem of the "apparent" failure of excluded middle in English posed by improper definite descriptions occurring as subject terms of grammaticaly subject-predicate sentences of English. Indeed, the Russellian Theory of Descriptions does not maintain the validity of existential generalization / universal specification as applied to descriptions. In contrast, Frege, who first articulated the view that (at least subject-predicate) sentences of natural language that contain vacuous singular subject terms do not have truth values, seems concerned with the general problem of the failure of certain intuitively acceptable modes of inference in languages that contain syntactically well formed but semantically vacuous singular terms. Frege [1, pp. 70] writes it is a defect o f languages that expressions are possible with in them, which, in their grammatical form, seemingly determined to designate an object, nevertheless do not fu l f i l l this condit ion in special cases . . . . it is customary in logic texts to warn against the ambiguity o f expressions as a source o f fal l ic ies . . . . it is a least appropriate to issue a warning against apparent names that have no designation ; Although Frege does not explicitly mention the intuitive modes of reasoning he feels that "logically perfect" languages should support, Frege's famous dictum, intended as definitive of the notion of a formal language, that in a log ica l ly perfect language ( logical symbol ism) every expression constructed as a name in a grammatically correct manner out o f already introduced symbols, in fact designate an object . certainly ensures that any reasonable formal semantic theory that satisfies it will maintain both 5 excluded middle and unrestricted generalization / specification as valid forms of inference. The three proof-theoretic treatment of descriptions we are concerned with comparing to Pld -Hibert and Bernay's [1] treatment of descriptive terms in a first-order arithmetic language, Frege's methods [1], [2], and the Whitehead-Russell [1] method presented in P.M.- can best be compared in terms of the above dictum: while the Hilbert - Bernays and the Fregean treatments are based upon different methods of satisfying this same dictum, the Russell's Theory of Descriptions is based upon a rejection of the dictum. For the purposes of the following discussion we introduce the strict-substitution operator [t I x], which, when applied to a formula or term E, yields the result [t I x]E of substituting / for all free occurrences of x in E. Renaming of variables bound in the formula or term is automatically effected so that any free occurrence of a variable in f is a free occurrence in the result of the application. 1) Russell's method: The proof-theoretic treatment of description terms that Russell presents in P.M. is based upon the semantic intuition motivating the Russelian Theory of Descriptions, that the propriety of an English definite description (that is, the condition that there exists a unique object satisfying the defining formula of the definite description) is part of the semantic content or meaning of the sentences in which the description occurs. Accordingly, a grammaticaly subject-predicate sentence S of English containing a definite description D.D as subject term is treated as semantically equivalent to, and an abreviation of, (the material mode equivalent of) the quantificational statement that there exists a unique object x satisfying the defining formula of D.D. and x bears the grammatical predicate of S. In P.M., Russell provides a proof-theoretic formalization of the Theory of Descriptions in terms of the following contextual definiton schema: [(ix)0 ly]F =x (3y)[(Yx)(& B I = J ) A F ] where d> is an arbitrary symbolic formula containing at most free occurrence of the variable x, and F is an arbitrary symbolic formula that contains a free occurrence of y, where y is different from x. This schema may be thought of as a two-way rewrite rule; for any instance I of the schemata, any 6 occurrence (in a symbolic sentence occurring in a derivation) of the symbolic sentence that is the definiendum, respectively, definiens of I may be replaced by the symbolic sentence that is the definiens, respectively, definiendum of L The important point here is that the description operator is not part of the primitve basis of the Russellian language; rather, it is a symbol that is defined only within arbitrary sentential contexts. Let us consider the "Russellian" description calculus obtained from the classical first order identity calculus by the addition of the above contextual definition to the proof theory for the identity calculus. Now, there are two ways in which we could set up a semantics for this Russellian proof theory of descriptions. We could leave the descriptor operator, and hence all description terms, out of the primitive basis of the language, in which case our semantics would simply be the classical semantics for the identity calculus, and no symbolic sentence (of the classical identity calculus with descriptions) that contains description terms would be evaluated relative to any model of our semantics. On the other hand, we could the add description terms to the elementary syntax of our language and add a semantic rule analgous to the Russellian contextual definition to our semantics so that a sentence of the form (3y)[(Yx)(& <-> x = y) A F] is true relative to a given model iff [(\x)&/ y]F is (where these two sentences satisfy the same restrictions as those placed on applications of the Russellian contextual definition above). The important point is that, in either case, this proof-theoretic treatment of description terms requires a semantics in which definite descriptions (i.e., description terms) are not assigned denotations at all. That is, if M is a model of a Russellian proof-theory of descriptions, then a symbolic sentence [(uc)d> / y]F that contains a description term (ix)& is not evaluated on the basis of an assignment of an object from the domain of M to (ur)d>. So a Russellian semantics for formal description calculi represents a rejection of Frege's dictum that every singular term, in particular, every description term, of a formal language should be assigned a denotation (relative to a given model, we would say) since within a Russellian semantics, description terms do not function to denote objects. As mentioned, the main drawback of the Russellian proof-theoretic treatment of descriptions is that existential generalization / universal specification are not in general sound (i.e., validity preserving) when applied to description terms. For suppose ( V y ) F is a classically valid symbolic 7 sentence, for some symbolic formula F containing free occurrence of y. Consider a symbolic formula d> containing at most free occurrence of a variable x such that -i(3^)( V x ) ( & <-> x = y) is classically val id (for example, the formula —,(x =x) w i l l do). Then clearly the symbolic sentence -i(3^)[( V X)(<P «-> x = y) A F ] is classically valid. Then, i f our Russellian description calculus is complete with respect to classical semantics, we are able to derive —i(3^)[(¥x)(d> <-> x = y) A F ] , The above definition, applied "left to right", allows us to re-write this sentence as -i[(ix)<2> /y]F. Then by an application of unrestricted existential generalization applied to the constant term (ix)<P, we may derive (3y)—iF. But since (Yy)F is a classically valid, so is —t(3y)—iF. Hence, (3y)--F is not classically val id. So (3y)—F(y) is derivable but not classically val id, i.e., our Russellian description calculus with unrestricted existential generalization of constant singular terms is not sound. Indeed, this example shows that such calculus (if complete) is not syntactically consistent, since in this example both of (3^,)—iF, —i(3p—iF are derivable. So any sound and complete Russellian calculus of descriptions must restrict the application of the deductive rule existential generalization so that only "provably proper" description terms, that is constant description terms (xx)&such that, for some variable y, the sentence (3y)(Yx)(&<-> x = y) is provable, may be generalized. It is easily shown that a similar restriction must be put on universal specification. One way of restricting existential generalization in this way is simply to require that any application of existential generalization in which the generalized singular term is a description term must be preceded by a subordinate proof of the propriety of the description term. 2) Freee's methods: Frege [1], [2], suggests two formal treatments of descriptions both of which involve satisfying his dictum, that every well-formed singular term of the language have a denotation, by making the arbitrary convention that otherwise improper description terms are assigned some object from the range of the individual variables. There are several ways that this convention can be implemented proof-theoretically, depending on the type of objects that belong to the domain of discourse of the model(s) of the system. In [2], Frege presents a typeless system in which both classes as well as their elements belong to the range of the individual variables, so he is able to make the convention that any constant description term whose descriptive formula is not uniquely satisfied by some object in the range of the individual variables be assigned as descriptum 8 the class of those objects satisfying the defining formula. So, relative to a model M of this type of system, different constant description terms whose defining formulas are not uniquely satisfied by some object from the domain of M may have different descriptums. Frege suggests a slightly simpler treatment in [1]. Here, a single object from the range of the individual variables of the system is chosen as the common descriptum of all description terms whose defining formula is not uniquely satisfied. For example, if the system is a first order arithmetic, zero might be chosen. Alternatively, if the range of the individual variables contains classes of individuals, the null set might be chosen as the common descriptum of all otherwise improper description terms (this is Quine's [1] choice in Mathematical Logic). Now, the literature contains two interesting proof-theoretic implementations of Frege's second method (we ignore the first method, since for our purposes, it is merely a more complicated method of achieving the goal of the second, viz., the assignment of arbitrary denotations to otherwise improper description terms). Carnap [1] suggests a proof-theoretic treatment of descriptions in which a particular individual constant of the language, say a0 , is chosen to denote the common descriptum of all constant description terms whose defining formula is not uniquely satisfied. More precisely, if M is a model for this particular proof-theoretic treatment of descriptions, then M assigns some object o from the domain of M to the individual constant a0 and for any constant description term (ut)<P of the language, ifd> is not uniquely satisfied relative to M by some object in the domain of M, then M assigns o to (uc)<P. In this formal treatment of descriptions a sentence of the form [(ix)& / y]F, whereCP is an arbitrary symbolic formula containing at most free occurrence of x and F is a symbolic formula containing free occurrence of y distinct from x, is treated as logically equivalent to the following sentence (3y)[(Yx)(0 <-> x = y) A F] V (r-(3y)[(Y x)(® <-> x = y)] A [a0/y]F). Then the proof theory for this treatment of descriptions is that of the first order identity calculus together with the following axiom schema (or the corresponding contextual definition): [(\x)0 /y]F <-> (3y)[(Yx)(® 4-> x = y) A F]v (--(3y)[(Yx)(® <-> x = J O ] A [a0/y]F). g and the semantics for this treatment of descriptions is that of the first order identity calculus together with a semantic rule that makes [(\x)0 / y]F semantically equivalent to (3y)[(i<rx)(& <-> x =y) A F] v(-^(3y)[(Yx)(0 ^x=y)]A [a0/y]F). The authors Kalish, Montague and Mar [1] present a natural deduction based treatment of descriptions based on Frege's second method. Here, the term chosen to denote the common descriptum of all otherwise improper constant description terms is the 'absurd' constant description term (ur)-i(;c = x). As in Carnap's treatment, if M is a model for this particular proof-theoretic treatment of descriptions, then M assigns some object o from the domain of M to the the description term (u:)—i(x = J C ) and for any constant description term (ix)0of the language, if<2> is not uniquely satisfied relative to M by some object in the domain of M , then M assigns o to (ix)0. Kalish, Montague and Mar present two inference rules for introducing description terms into their natural deductions derivations. P.D. (Proper Description) allows the symbolic formula [(\x)0 I x]0 to be derived from a formula of the form (By)(Yx)(0 <-» x =.y), where 0 is an arbitrary formula containing no free occurrence of y. I.D. (Improper Description) allows the formula (ix)0 - (uc)—I(JC = x) to be derived from a formula of the form -i(3y)(Yx)(0 <-> x = y), where 0 is an arbitrary symbolic formula containing no free occurrence of y. As mentioned above, the main advantage of the Fregean treatments over the Russellian is that they maintain the soundness of the inference rules existential generalization and universal specification. It is easy to show that they also preserve excluded middle (as does the Russellian). The main disadvantage of the Fregean treatments over the Russellian is that the meanings that certain symbolic sentences containing description terms receive in these treatments diverge from their intuitive meanings. For example, when we consider the following two sentences 1) (Yx)(0^x = b) 2) b = (ix)0 (where b is an individual constant) as translations of English sentences, we expect them to be semantically equivalent - indeed, it is easily verified that they are semantically equivalent within a 10 Russellian semantics. But it is easy to see that there are Fregean models in which 1) is false but 2) is true: let M be any Fregean model such that there is no object o in the domain of M which uniquely satisfiesdA Further, assume that M assigns the "default object" (i.e., the element of the domain of M which has been chosen as the common descriptum in M of all constant description terms whose defining formulas are not uniquely satisfied relative to M by some object in the domain of M) to the individual constant b. Then 2) is true relative to M but 1) is, by hypothesis, false. 3) The method of Hilbert and Bernays: In [1], Hibert and Bernays present an arithmetic calculus (that is, a proof-theory with the natural numbers as the intended model) based upon a proof-theoretic implementation of Frege's dictum (that a formal language must insure that every syntactically well-formed singular term have a denotation) which is an alternative to the Fregean convention of assigning a "default object" to otherwise improper description terms. Rather than defining "term / formula of the language" in a context-free grammar (per the classical approach to defining the elementary syntax of logical languages) this treatment defines the elementary syntax and the notion of proof by simultaneous induction such that a string of the form (ix)&, and hence any "sentence" in which it occurs, is allowed into the language only if there is a proof that there is exactly one natural number satisfying the defining formula <2>. Hence, whereas Frege satisfies by semantic means his dictum that all singular terms defined in the elementary syntax of a logical language have denotations (by assigning a "default object" to otherwise improper description terms), Hilbert and Bernays satisfies Frege's dictum by modifying the elementary syntax of classical arithmetic with descriptions so that a string of the form (ur)<2> is considered well formed only if (there is a proof that) there is exactly one natural number satisfying ® . Hilbert and Bernays' single deductive rule for introducing description terms into derivations provides the original motivation for Gilmore's natural deduction rule for descriptions presented in [2] and (hence) both the proof theoretic and the semantic rules for treating description terms in Pld. We might think of the Hilbert and Bernays' deductive rule for descriptions, and indeed Pld's, as a "one-way" implementation of the Russellian contextual definition that allows us to introduce description terms into arbitrary sentential contexts but not eliminate them from sentential contexts. 11 Roughly speaking, the Hilbert and Bemays deductive rule for description terms (as well as Gilmore's and Pld's deductive rules for descriptions) allows the symbolic sentence that is the definiendum of an instance of the Russellian contextual definition to be concluded from a derivation line consisting of the symbolic sentence which is the definiens of that instance; there is no corresponding rule for introducing description terms into derivations on the basis of a derivation line consisting of the denial (negation) of the symbolic sentence that is the definiens of an instance of the Russellian contextual definition (as there is in the Russellian and Fregean proof theoretic treatments of descriptions). Hence, only provably proper description terms (which are the only description terms in Hilbert and Bernays' language) can be introduced into symbolic sentences in a derivation. If we forget, for the moment, that the language of the Hilbert and Bemays arithmetic calculus is only a proper subset of what we might call "classical arithmetic with descriptions", it would seem that this property of a proof-theory alone, that the only symbolic sentences that can be introduced into a derivations are those in which the only occurring description terms are provably proper, will insure that excluded middle fails for that proof-theory. For surely no sentence of the form ((uc)-1(x = x) = b) v —i((uc)—\(x = x) = b) will be derivable in such a system. Indeed, this sentence of the classical identity calculus with descriptions is not a theorem of Pld. But of course, this sentence is not even in Hilbert and Bemays' language. It is easy to show that excluded middle holds for every sentence of classical arithmetic with descriptions that is in Hilbert and Bernays' language, so their proof-theoretic treatment of descriptions can be classified, along with Frege's and Russell's, as a totalizing treatment in the sense that it is sound only with respect to models that are total Tarskian functions from the set of sentences of the language into {T, F}. One obvious drawback of the Hilbert and Bemays proof-theoretic treatment of descriptions is that this system's language does not have a decidable elementary syntax. Indeed, it is easily seen that the set of well-formed strings of that language is recursively enumerable but not recursive. Carnap [1] points out another drawback of the general approach of satisfying Frege's dictum by restricting the elementary syntax of the classical description calculus. While this approach may be convenient in an arithmetic calculus, he suggests, its extension to general proof-theories in 12 which "factual" symbolic sentences may figure as premises to deductions has the consequence that the set of well formed strings of the language, and hence the formal notion of grammaticality, will depend on "the contingency of facts". We might put Carnap's point here slightly more generally as follows: "The approach of satisfying Frege's dictum by restricting the elementary syntax of the classical description calculus lends itself to an applied system like arithmetic with descriptions since the set of constant description terms of classical description calculus that are "provably proper in arithmetic", and hence are well-formed expressions for the language thus restricted, although undecidable, is at least determinate (at least for a Platonist). However, if this approach is extended to a general description calculus in which we can axiomatize arbitrary extralogical first order theories, the language thus restricted becomes indeterminate since the set of constant "description terms of classical description calculus that are "provably proper" now depends on the particular extralogical theory whose axioms are figuring as premises in derivations of the general calculus". Now it seems to me that the soundness of Hilbert and Bernays proof-theoretic treatment of descriptions in arithmetic illustrates that Frege's dictum places a requirement on the notion of a formal language that is stronger than is necessary to achieve Frege's goal of eliminating the possibility of falacious inferences within a formal language. For the type of fallacious inferences that are due to the occurrence of sentences containing vacuous singular terms in arguments of natural language can be avoided in languages that do not meet the condition that every well formed singular term is assigned a denotation. As the Hilbert-Bernays treatment shows, to avoid making fallacious inferences in a formal language, we need only avoid reasoning over sentences of the language that contain vacuous singular terms. In other words, to avoid fallacious inferences in a formal language with descriptions, we need only exclude improper description terms from occurring in sentences in our derivations, rather than from the language altogether. So Hilbert and Bemay's practice of excluding from their language those sentences that contain classical description terms that are (arithmetically) improper is not necessary to satisfy the goal of Frege's dictum (if not the letter). Of course, any proof-theory of descriptions that uses the Hilbert-Bernays technique (of allowing a description term to be introduced into a sentence in a derivation only after its propriety has been proven) but does not restrict its elementary syntax in 13 the manner of Hilbert and Bernays will not be complete with respect to any classical semantics for that language. For, as we have seen, the classically valid sentence ((uc)— I(J C = J C ) = b) v —i((u:)—\(x = x) = b) will not be derivable in such a system. Now, consider the semantics for such a system obtained from Tarskian first order semantics by adding to the Tarskian definition of 'truth relative to a model' a rule that is the semantic version of our "one-way" deductive rule for description terms, so that the definiendum of an instance I of the Russellian contextual definition is true relative to a model M of this semantics if the definiens of I is true relative to M but not conversely. This semantics is found to be a generalization of Tarskian semantics in which excluded middle holds for all sentences of the classical identity calculus but fails in a model M for (certain) symbolic sentences, and only symbolic sentences, that contain constant description terms that are improper relative to M . Then this semantics together with our Hibert-Bernaysian proof-theory constitutes a sound and complete partial logic of descriptions based upon a decidable elementary syntax. Essentially, we maintain both the semantic completeness of our proof-theory and the decidability of our elementary syntax by making the nonrecursive procedure of determining the propriety of a given description term part of the semantics of our system (where it belongs), rather than polluting our elementary syntax with it, as Hilbert and Bernays would have us do. This is the motivation for Pld. 14 Section 1: The System Pld. 1.1 Elementary syntax The language for Pld has as its primitive basis the sets of symbols given in 1.1.1. - 1.1.9. below: .1. An enumerable set Var of individual variables: V , V, 'w', 'x', 'y', with or without numeric subscripts. An individual variable is a term. An individual variable has an occurrence in itself. An occurence of an individual variable in itself is a free occurrence in itself. .2. An enumerably infinite set Par of individual parameters: 7', 'm', 'n','p', 'q', with or without numeric subscripts. An individual parameter is a term. An individual parameter has an occurrence in itself. .3. A finite set Cnst of individual constants: 'a', 'b\ 'c\ 'd\ 'e', with or without numeric subscripts An individual constant is a term and has an occurrence in itself. .4. A finite set Fun of unary functors: '<£\ 'A', with or without numeric subscripts. .5. For each n, a denumerable set set Pred? of n-ary descriptive predicate constants: 'Qn','/?"', 'Sn', with or without numeric subscripts. .6. A set {'='}containing a single binary logical predicate constant. .7. A set { ' - i ' , ' A ' } of sentential connectives. .8. A set {'()' , V} of variable binding operators. V is called the d e s c r i p t i v e operator. .9. A set {'(', ')' > '•'} of punctuation marks. For the purposes of discussion we will assume as available the connective and quantifier sets 15 of the full predicate calculus on the understanding that expressions over the larger language are defined in terms of the above primitive basis in the usual way. For each set S of symbols given in 1.1.1. - 1.1.5., above, we let the bold-face version of the member symbols be metalinguistic variables ranging over S. Each symbol which is a member of one of the sets given in 1.1.6. -1.1.9. occurs in the metalanguage as a metalinguistic constant denoting itself in the object language. Let r, s, t, with or without numeric subscripts, be metalinguistic variables ranging over terms. Metalinguistic concatenation denotes object language concatenation. Then, .1.0. Elementary formulas are of the formi >"(/ / , . . . , tn) and (tj = t2). A (free) occurrence of a variable in one of tv . . ., tn is a (free) occurrence in Pn(tv . . ., tn). A (free) occurrence of a variable in tt or in t2 is a (free) occurrence in (tt - t2). Elementary formulas are formulas. An elementary formula of the form Pn(tv . . ., tn), t2 = t2 is an atomic formula if the tv t2, . . . ,tn are basic terms. Let 'afm', respectively, 'F', 'G\ 'H', , '*¥', 'E', with or without numeric subscripts, be metalinguistic variables over atomic formulas, respectively, formulas. .1.1. If F and G are formulas, then the following expressions are formulas: —F, (x)(F), (F —> G), (F A G). A (free) occurrence of a variable in F is a (free) occurrence in —>F. A (free) occurrence of a variable in F or G is a (free) occurrence in both of (F —> G), (F A G). A free occurence of a variable other than J C in F is a free occurrence in (x)(F); no other variable has a free occurence in (x)(F). .1.2. If / is a term and £ is a unary functor, then the result fit) of applying fi to t is a term. If F is a formula, then ur.F is a term, and a description term. A (free) occurrence of a term r in / is a (free) occurrence in fit). An occurrence of a term r in F is an occurrence in ur.F . A free occurrence of a variable other than x in F is a free occurrence in ur.F; no other variable has a free occurrence in ur.F. A term in which no variable has a free occurrence is a constant term. .1.3. A term which contains no occurrence of a description term is a basic term. .1.4. Let P : INI —> Par be a bijective enumeration of Par. Let n be any subset of Par. Then 8(TT) is the set of constant basic terms in which the only occurring parameters are from Par u {P(l)}. So 8(Par) is the set of constant basic terms of Pld. 16 .1.4. A sentence is a formula in which no variable has a free occurrence. Let n be any subset of Par. Then E(TT) is the set of sentences in which the only occurring parameters are from %. So TXPaf) is the set of all sentences of Pld. Throughout the remainder of this paper, we will use the symbol '=' to denote the relation of syntactic identity holding between terms, formulas and signed sentences of Pld. In other words, the expression 'Ej = E2' shall mean that the expression denoted by the metalinguistic variable 'Ej'is syntactically the same expression as that denoted by 'E2'. We do this to avoid confusion with the object language symbol for identity '='. Further, we will use both of '=', '=' to denote the relation of set theoretic identity holding between sets of signed sentences; '=' will be used to denote this metatheoretic relation only when there is no danger of confusing it with the object language symbol '='. In particular, will be used to denote the identity relation holding between those sets of signed sentences which are denoted in this text by the display of their member signed sentences. The following expressions, with or without numeric subscripts, will be used as metalinguistic variables over atomic sentences, respectively, sentences: 'asnt', respectively, 'snt', 'A', 'B', 'C, 'D'. The logical syntax and the semantics for Pld is presented in the manner of Gilmore [1], [2] using the notions of signed sentence and sequent of signed sentences. If A is a sentence, then both of ± A are signed sentences. A sequent is any finite set of signed sentences. Semantically, the signature ± indicates, respectively, the assignment of truth or falsehood to a sentence relative to a model. In the logical syntax, the signature ± indicates that the sentence so signed occurs to the right, respectively, left, of the Gentzen arrow. Also used is the simultaneous strict-substitution operator [tv . . ., tnlxv . . ., xn], which, when applied to a formula or term, substitutes ti (l < / < n) for all free occurrences of xt in the formula or term, such that none of the xt occurring free in any of the tv . . ., tn , are substituted for. Renaming of variables bound in the formula or term is automatically effected so that any free occurrence of a variable in /t- is a free occurrence in the result of the application. The substitution operator [tv . . 17 '>tnlxp • • - ' ^ J will be abbrieviated as [£/£], where £ s . . . , tn and x = xv . . ., xn. We will also apply the simultaneous strict-substitution operator [tv . . .,tnlxv . . ., xn] to sequents such that [tp . . . ,tnlx1, . . ., xn]Seq denotes the sequent obtained from the sequent Seq by replacing every signed sentence ±snt in Seq by respectively ±[tv . . . ,t I Xj, . . . , xjsnt. 1.2. Logical syntax We present a set of axioms and first order rules of deduction much as in Gilmore [1], [2]. Rule 1.2.2.6. below is significanly modified over the rule 5.3.2. for descriptions presented in Gilmore [2], where description terms are defined on the basis of set abstraction terms from the first order set theory. 1.2.2.6. represents a weakening of the restriction 5.3.2. places on the "existance" and "uniqueness" premises of an application of that rule such that the "input" sentences to an application of 1.2.2.6. do not have to be themselves derivable sentences, but rather merely positively signed members of a derivable sequent. Indeed, as we demonstrate in section 6, this modification is necessary to the completeness of the set of rules given below relative to the semantics we will define. .1. Let t be in 8(Par). Then the set of axioms is the set of all sequents of the form {-asnt, +asnt} or of the form {+(t = t)}. .2. Let t, r, s be constant, possibly non-basic, terms. The rules of deduction are given by the following schemata: .l.± (thinning) Seq Sequ {±A} .2.± Seq u {±A} Seq u {+-iA} 18 . 3 . ± Seql u { +A } Seq2 u {+B } Seq u {- A , -B } Seql u Seql u {+(A A B)} Seq U {-(A A B)} A.± Seq<u{-A,+B} Seql U [+A] Seql u {-B} Seq u {+(A -» B)} Seql u & ? 2 u {-(A —» B)} .5.± Sequ {+\p/x]F} Seq u {-[t / x]F} Seq u {+(x)F} Seq u {-(x)F} where, for .5.+, p is a parameter which does not occur in the conclusion Seq u {+(x)F}. .6. Seql \j[+[t/x]0} Seql u {+(x)(v)((<P A [V / x]d>) -» x = v)} S«$3 u {±[tI u]F} Seql u Seql u Se^J u {+[ix. <2> / «]F } . where, v different from x. .7. Seql u {+[r / u]F} u {- [« / «]F} u Seql u {-(r = s)} .8. (cut) 5^1 u {+A} 5«^2 u {-A}. Seql u Seql An instance of one of the above rule schemata will be called an application of the rule. For a given application A of one of the above rules, the sequent(s) above, respectively, below, the vinculum are called the premise(s), respectively, conclusion, to A. Let the signed sentential variables (i.e., '±A', '±B', '±[t / x]& ', '±(x)F\ '+(A A B)', etc.) explicitly given in the premises, respectively, conclusion, of a given rule schema R be said to denote the input sentence(s), respectively, output sentence, to a given application of R. 19 We have, then, a three premise rule for introducing sentences containing definite descriptions (i.e., description terms) into derivations. Notice that .6. is unique among the above rules in that it does not have a dual rule treating the case where the input sentences to an application have negative signatures. This asymmetric treatment of descriptions is motivated by the intuition that we cannot, in genaral, validly introduce a sentence containing a description into a derivation on either side of the turnstile (i.i., Gentzen arrow) without first securing the existence of a descriptum for the description to denote. This corresponds to the semantical intuition behind the Frege-Strawson doctrine that a sentence of natural language which is grammatically of subject-predicate form and which contains a vacuous singular subject term cannot have a truth value associated with it. We can say, then, that any description which is introduced into a Pld derivation by 1.2.2.6. has large scope, in the Russellian sense, over the sentence in which it occurs. .3. An axiom from 1.2.1. is a derivation tree. If Z is a derivation tree whose endsequent Seq is the premise of an application A of one of 1.2.2.1.±, 1.2.2.2.±, 1.2.2.3.-, 1.2.2.4.+, 1.2.2.5.±, then the tree obtained from Z by appending the conclusion of A to Seq is a derivation tree. If Z, Z' are derivation trees whose endsequents respectively Seq, Seq' are premises of an application A of one of 1.2.2.3.+, 1.2.2.4.-, 1.2.2.7., 1.2.2.8. then the tree obtained from X and Z 1 by appending the conclusion of A to Seq and Seq' is a derivation tree. If Z, Z', Z" are derivation trees whose endsequents respectively Seq, Seq', Seq" are premises of an application A of 1.2.2.6. then the tree obtained from Z and Z'and Z" by appending the conclusion of A to Seq and Seq' and Seq" is a derivation tree. .4. A sequent Seq of signed sentences is derivable iff it is the endsequent of a derivation tree. A sentence snt is derivable iff the sequent {+snt} is derivable. .5. A sentence snt is grounded iff the sequent. {+snt, -snt) is derivable. Let Grd denote the set of grounded sentences. .6. The depth D(L) of a derivation tree Z is zero if Z ia an axiom; otherwise D(L) = 1 + D(Z') 20 where £' is E's deepest proper subtree. 1.3 Semantics A term model for a formal system T is an interpretation for T whose domain of discourse is the set of constant terms defined in the elementary syntax for T. In this subsection we define a class of term models, called bases, for Pld. .1. Let K Q Par be any set of parameters. A base bse with domain 5(7F) is any set bse of signed atomic sentences from X(7r) which satisfies the following three conditions: 1) For every atomic sentence asnt e E(K), exactly one of ±asnt is a member of bse. 2) For all terms t in 5(7r), +/ = / is in bse. 3) For all terms r, s in 8(7r), if both of +[r / x]afm, -[s I x\afm are in bse, then so is -r=s. For the remainder of this paper, we use simply the term 'base' to mean 'base with domain d(Par)' unless otherwise indicated. .2. Let Set be a set of signed sentences. The semantic successor Se(Set) of Set is the smallest set satisfying the following semantic rules: .1. If respectively ±A is in Set, then respectively +—iA is in Sc(Set). .2. If each of +A, +B, respectively, one of -A, -B, is in Set, then respectively ±(A A B) is in Sc(Set). .3. If one of -A, +B, respectively, each of +A, -B, is in Set, then respectively ±(A —» B) is in Sc(Set). .4. If Set contains +[t / x]F for all tin 8(Par), respectively, -[t I x]F for some / in S(Par), then respectively ±(x)F is in Sc(Set). .5. If each of +[t I x]®, +(x)(v)((<P A [V / x]®) -> x = v), and one of, respectively, ±[t I u]F, is in Set, then respectively ±[\x.® I u]F is in Sc(Set), where / is a constant, possibly non-basic, term. 21 In the semantic rule 1.3.2.5. for descriptions, let '+[t/ x]<P, '+(jc)(v)((d> A [V / x]<P) -> x = v)' be said to denote the signed sentence which is the existence, respectively, uniqueness, presupposition of an instance of 1.3.2.5.. '±[t I u]F' will be said to denote the signed sentence which is the major statement of an instance of 1.3.2.5.. We have then, a rule which is the obvious semantic analog to the derivational rule 1.2.2.7. for descriptions. Note the assymetric treatment descriptions receive semantically: 1.3.2.5. has no dual rule treating the cases where one of the presuppositions of an instance of the rule is false, i.e., of negative signature, in bse. .3. Let Set be a set of signed sentences. We define by transfinite induction on fi a sequence (Set^) as follows: .0. SetQ = Set; .1. Set n + i = &e*n u Sc(SetjJ for successor ordinals ji ; .2. Set^ = KJSetp,0 <P</J- for limit ordinals fl. A. The semantic closure CEibse) of bse is the union set of the bse.. for ordinals fi less than the first nondenumerable ordinal, i.e., Cl(bse) = bseeo . .5. Let bse be a base. A sequent Seq is valid for bse iff \tl p\Seq n Cl(bse) * 0 , where £ is an n-ary vector on Par which contains all of the parameters which occur in signed sentences of Seq and I is any n-ary vector on S(Par). .6. A sequent Seq is valid iff Seq is valid for all bases. A sentence snt is valid iff {+snt} is a valid sequent. Lemma I.3.7.: Sc(Cl(bse)) Q Cl(bse). Proof of I.3.7.: Suppose otherwise, i.e., suppose Sc(Cl(bse)) 3 ClQjse). Then there is a sequence bseQ, . . ., bseE0, Sc(Cl(bse)) of sets of signed sentences each of which properly includes its immediate predecessor. But this sequence is order type E Q + I, and so is of nondenumerable cardnality. Hence, there are nondenumerably many distinct sentences of Pld. But 22 Pld has only denumerably many sentences. Contradiction. • We should note that it is possible to define the semantic closure Cl(bse) of a base bse by finite induction only as bsea. That is, one can show by induction on / , 0 < i < CO, that Sc(bse^) ^> bsew. However, we maintain definition 1.3.4. of Cl(bse) as bseE0 since that definition makes the proof of 1.3.7. much easier than would otherwise be the case. Note that since the semantic rule 1.2.3.4. limits the range of the universal quantifier to the set &(Par) of constant basic terms, and since no description terms occur in any sentence of any base, the bases we are considering all have 8(Par) as their domain of individuals. Hence, description terms play no semantic role in the class of term models defined in 1.3.. Rather, the role that description terms play in Pld is of a purely syntactic nature: descriptions function in the logical syntax (specifically, through the rule of universal specification, .5.-) to abbreviate the results of certain formal deductions and hence to facilitate certain further deductions, deductions which can be achieved without the use of descriptions. Hence, although, Pld is nominalistically interpreted, in the sense that its models are syntactic, description terms do not function as individuals in those models. The fact that description terms do not belong to the domain of individuals in our term models is expressed by lemma 1.3.10. below which "says" that a description term will "bear a range of properties" relative to a given model of Pld only if there is a basic term which bears the same range of properties. This fact proves crucial to the proof (lemma 1.3.9.) that the class of term models we have defined "obey the law of noncontradiction" in the sense that no sentence is assigned both the value true and the value false relative to any given model. Lemma 1.3.8.: Let bse be any base and let r, s be any terms in 8(Par) such that the signed sentence +r = s is in Cl(bse). Then, for all formulas F, if ±[s I x]F is in bse^, so is respectively ±[r / x]F. Proof of 1.3.8.: Suppose +r = s is in Cl(bse). Then, since +r = s is atomic, +r = s is in bse. We show by transfinite induction on jU in definition 1.3.3. that for all fi, if ±[s I x\F is in bse , so is respectively ±[r I x]F. So let ±[s I x]F be any signed sentence in bse . Clearly, we may 23 assume that x occurs free in F, since otherwise the claim holds vacuously. Base step: fi = 0. By clause 1) of definition 1.3.1., since bse contains +r = s, bse does not contain -r = s. Hence, by the contrapositive of clause 3) of 1.3.1., for every atomic formula afm, if ±[5 / x]afm is in bse^, then so is respectively ±[r / x]afm. But bse contains atomic formulas only, so the claim holds. Induction step: Assume that for all f5 < fl, for all formulas G, if ±[s I x]G is in bse^, so is respectively ±[r / x]G. We want to show that respectively ±[r / x]F is in bse . For limit ordinals fi: Since ±[s I x]F is in bse^, and bse^ = ^Jbse^ , 0 < /J < /z, respectively ±[s I x\F is in bse^ for some p < fi. By the hypothesis of induction, then, respectively ±[r / x]F is in bsepQ bse^. Successor ordinals fi: By the hypothesis of induction, we may assume that ±[s I x]F is not in bse^ for any/? < fi, since otherwise respectively ±[r / x]F is in bse^ Q bse^ . Then, since bse^ = bse^_j u Sc(bse^_j), ±[s I x]F is in Sc(bse^_^). There are five main cases: i) ±[s I x]F is in Sc(bse^_j) by virtue of an instance of the semantic rule 1.3.2.1. and is respectively of the form ±[s I x]->G = ±-\[s I x]G for some formula G. Then respectively ±[s / x]G is in bse^_j. So, by the hypothesis of induction, respectively ±[r/x]G is in bse^. Then, by 1.3.2.1., respectively +-.[r / x]G = ±[r / x]->G = ±[r I x]F is in Sc(bse..) Q bse... ii) ±[s I x]F is in Sc^bse^j) by virtue of an instance of the semantic rule 1.3.2.2. and is respectively of the form ±[s I x](G AH) = ±([S I x]G A [S I x]H). Then each of +[s I x]G, +[s I x]H, respectively, one of -[s I x]G, -[s I x]H, is in bse^_t. So, by the hypothesis of induction each of +[r / x]G, +[r I x]H, respectively, one of -[r / x]G, -[r I x]H, is in bse . . By 1.3.2.2., then, respectively ±([r / x]G A [r / x]H) = ±[rl x](G AH) = ±[r/ x]F is in ScibseJ ^ bse . iii) ±[5 / x]F is in Sc(bse^_^) by virtue of an instance of the semantic rule 1.3.2.3.. This case is 24 similar to ii). iv) ±[s I x]F is in Scibse^j) by virtue of an instance of the semantic rule 1.3.2.4. and is respectively of the form ±[s I x](y)G = ±(y)[s I x]G for some formula G. Then bse , contains +[/ /y][s I x]G & +[s I x][t /y]G for all / in 8(Par), respectively, -[t /y][s I x]G = -[s I x][t / y]G for some / in 8(Par). So, by the hypothesis of induction, bse^ contains +[r / x][t /y]G = +[t /y][r I x]G for all / in 8(Par), respectively, -[r / /y]G = -[t /y][r I x]G for some t in 8(Par). Hence, by 1.3.2.4., Sc(bse^) Q bse^ contains respectively ±(y)[r/x]G = ±[r/x](y)G = ±[r/x]F. v) ±[s I x]F is in Sc(bse^_j) by virtue of an instance I of the semantic rule 1.3.2.5. for descriptions and is respectively of the form ±[s I x][iy.<P/ u]G for some constant description term ty.CP and formula G. Since s is a constant term, we may rewrite the sentence [s I x][iy.&/ u]G as [iy.[s I x ] f / u][s I x]G for some formula *¥ such that 0 = [s I x]*P. Then, since ±[vy.[s / x]*F I u][s I x]G is in Sc(bsetl_1) by virtue I, bsefl_1 contains both of the presuppositions +[t/y][s Ix]f, +00(v)(([s / x]*FA [V /y][s I x]f) -> y = v), as well as the major statement respectively ±[t/u][s/ x]G for some constant term t. Since both of /, s are constant terms, the presuppositions may be written as: +[s I x][t /y] % +[s Ix](y)(v)((*FA [V I y] f) —> y = v) and the major statement may be respectively rewritten as ±[s I x][t /u]G. Then, by the hypothesis of induction, bseft_l contains both of +[r/x][t/y]% +[r/xJiyXvXi*?A [VI y] f ) -»y = v), respectively ±[r/ x][t/u]G. Again, these signed sentences may be written as: +[tly\[rlxW, +(y)(v)(([r/x j f A [ V /y][r I J C ] « P ) y = v), respectively ±[t/u][r I x]G. Since bse j contains all of +[t /y][r I x] «P, +0)(v)(([r / x] f A [ V /y][r I x] *¥) -> y = v), respectively ±[t/u\[rIx]G, by 1.3.2.5., Sc(bseu) c toe..contains respectively ±[iy.[rIx]*F/ u][rl x]G= ±[r/ x]F. • Lemma 1.3.9.: Let bse be any base, snt any sentence. Then, for all ordinals ^, not both of ±snt are in bse^. Lemma 1.3.10.: Let bse be any base. Then, for all ordinals /I, for evey constant description term 25 ix.®, there is a basic term t^ $ in b(Par) such that for all formulas F, if ±[ur.<P / K ] F is a signed sentence in bse^, then respectively tf /^^/wJF is in bse^. ^ . ^ i s called a descriptum for ix. ® in 6se. Proof of 1.3.9. and 1.3.10.: We prove 1.3.9., 1.3.10 by simultaneous transfinite induction on fi in definition 1.3.3. showing that all ordinals jj, satisfy both of 1.3.9., 1.3.10.. Let bse be any base. Base step: fi = 0. Since bseQ = bse is a base, by condition 1) of definition 1.3.1., not both of ±snt are in bse0. So 1.3.9. holds. Since bse0 = bse contains signed atomic sentences only, and no atomic sentence contains an occurrence of any description term, 1.3.10. holds vacuously. Induction step: ju > 0. Assume that for all p </!, bse^ satisfies both of 1.3.9., 1.3.10.. That is, assume that a) for all <fi, not both of ±snt are in bse^ , and b) for all /? < fi, for evey constant description term ix.®, there is a basic term t^ ^ in 5(Par) such that for all formulas F, if ±[ur.d> /u]F is a signed sentence in bse^, then respectively ±[1^ ^ /u]F is in bse p. We need to show that bse.. satisfies both of 1.3.9., 1.3.10.. For limit ordinals ji: Since bse^= K^Jbsep,0 <{5<[i, both of 1.3.9., .1.3.10., hold trivially for bse by the hypothesis of induction. For successor ordinals fi: We show first that bse satisfies 1.3.10.. Let ix.® be any description term. We want to show that there is a in h(Par) such that for all formulas F, if ±[ix.®/u]F is a signed sentence in bse^, then respectively ±[txx ^ /u]F is in bse^. Clearly, we may assume that \x.® occurs in a signed sentence ssnt belonging to bse , since otherwise the claim holds vacuously. There are two main cases: a) For no y< fi, constant term variable v, does fose^contain both of the signed sentences +[t I x]®, +(x)(v)((® A [v I x]®) —> x = v). Since \x.® occurs in some signed sentence ssnt belonging to bse and (bse ) is well ordered under Q, there is a least y< \i such that ix.® occurs in some signed sentence ssnt belonging to bse . Since bse0 contains signed atomic sentences 26 only,/* 0. If yis a nonzero limit ordinal, then there is a /? < /such that ssnt e fae^. Hence, yis a successor ordinal. Let t^ # be any term in 8(Par). Now, we show by induction on a that for all a, y< a < jU, for all formulas F, if ±[vc.<P/u]F is in foea, then respectively ±[1^ 0/u]F is in bsea. Clearly, our desired result that for all formulas F, if ±[vc.® /u]F is a signed sentence in bse^, then respectively tit^ 0 /u]F is in bse^ , will follow from this result. So assume that the signed sentence ±[ix.®/u]F is in bsea Base step: a = y. Now, since yis a successor ordinal, by definition 1.3.3., bse^ = bse^ u Sc( bse^_t). Since ix.& does not occur in any signed sentence inbse t it follows that ±[ix.<X>/ u]F is in bse^by virtue of being in Sc{bse^. Since ixd> is a constant term and bse^ does not contain the presuppositions to any instance of semantic rule 1.3.2.5., ±[ix.®/u]F is obtained in Sc(bsey_j) by an instance I of one of the semantic rule 1.3.2.2., 1.3.2.3.. We will assume that I is an instance I of 1.3.2.2., since the other case is similar. Then ±[tx.®/u]F is of the form -(A A [ix.® /u]H) for some sentence A and formula H containing free occurrence of u.,where bse^ contains the the signed sentence -A. Then by an instance of 1.3.2.2., Sc(bse^ contains the signed sentence -(A A [t^^/ulH) = -[t^^/ulF. So the claim holds. Induction step: a > y. Assume c) that that for all f3, y<fi < a, for all formulas F, if ±[ix.d>/ u]F is in bse^, then respectively ±[t^<p /u]F is in bse^. We want to show that for all formulas F , if ±[ix.® /u]F is in bsea, then respectively ±[t^0 /u]F is in bsea. So let F be any formula such that ±[ur.d>/«]F is a signed sentence in bsea We show that respectively ±\t # /u]F is in bsea. For limit ordinals or. Since bsea = K^Jbse^, 0 < < a, the claim holds trivially by hypothesis of induction c). For successor ordinals a: We may assume that for no /? < a is ±[u:.d>/w]F in bsea, since otherwise, by the hypothesis of induction, the claim holds trivially. Then ±[ut.d> /u]F is in Sc(bsea_j). Since a - 1 < n and no for no J3 < fi does bse^ contain the presuppositions to any instance of 1.3.2.5., there are just four cases: i) ±[ix.® /u]F is obtained in Sc(bsea_j) by an application of semantic rule 1.3.2.1. and is respectively of the form ±[ix.<P /u]-~G, for some formula G. Then bsea_t contains repectively 27 + [ix.&/u]G and so, by the hypothesis of induction c), contains +[tlx0/u]G. Hence, by semantic rule 1.3.2.1., respectively ± [t^^/u\-\G = ±[f w < &/u]F is in Sc(bsea_j) Q bsea. ii) ±[ix.0 /u]F is obtained in Sc(bsea_j) by an application of semantic rule 1.3.2.2. and is respectively of the form ±[ix.& /u](G A H), for some formulas G, H. Then bsea_x contains both of +[ix.& /u]G, +[vc.& /u]H, respectively one of -[vc.(P /u]G, -[xx.O /u]H. By hypothesis of induction c), bsea_t contains both of +[tXJC^/u\G, +1^0 u]H, respectively one of -[t^ 0/u]G, -[t^^/ulH. Hence, by semantic rule 1.3.2.2., respectively i f f ^^ /wKG AH) = ±[t^/u]F is in ScQbse^ ) Q bsea . iii) ±[ix.O /u]F is obtained in Sc(bsea_j) by an application of semantic rule 1.3.2.3. and is respectively of the form ±[ix.&/u](G -*H). This case is similar to ii). iv) ±[ur.<P/u]F is obtained in Sc(bsea_j) by an application of semantic rule 1.3.2.4. and is respectively of the form ±[ur.<3>/«](v)G, for some formula G. Then bsea_l contains +[ix.&/ u][s I v]G for all s in 8(Par), respectively, -[ur.d> /u][s I v]G for some s in 8(Par). So, by hypothesis of induction c), bsea_j contains +[txx&/u][s I v]G for all s in 8(Par), respectively, "•Aj:.<&/MHS 1 v ^ f° r s o m e s m 8(Far). Since both of s, # are constant terms, ±[^ ^ / u][s I v]G = ±[s I v][^ 0 /«]G. So bsea_j contains +[s I v ] ^ 0/u]G for all s in 8(Par), respectively, -[s I v][/lJC 0/u]G for s in 8(Par). Hence, by semantic rule 1.3.2.4., respectively ±(v)[tlx<p/u]G = ±[* l x > < p/«](v)G = ± [ ^ 0 / u ] F is in Sc&se^ ) c bsea . In all cases then, respectively ±\txx^/u\F is in bsea . This completes the induction step for case a) . b) For some y< fi, constant term t, variable v, frse^contains both of the signed sentences +[t I x]&, +(jc)(v)((d> A [v /x]<P) - > J C = v). Then, since (bse >is well ordered under Q, there is a least 7< \x such that for some y< /i, constant term variable v, fae7contains both of the signed sentences +[t I x]0, +(x)(v)((® A [V I x]<P) -» x = v) . Since y< /x, by hypothesis of induction b), we may assume that this / belongs to &(Par). So let # be t. Now, we show by 28 induction on a that for all a, y < a < /z, for all formulas F , if ±[ix.d> /u]F is in &.yea, then respectively ± [ ^ 0 / u\F is in bsea. Clearly, our desired result that for all formulas F, if ±[vc.® /u]F is a signed sentence in bse^, then respectively ±[7^ ^ / w ] F is in bse^, will follow from this result. So assume that the signed sentence ±[ix.® /u]F is in bsea Base step: a = y. Since for no /J < y does fae^ contain the pressupositions to any instance of the semantic rule for descriptions 1.3.2.5., it follows by the argument given in case a) above that for all formulas F , if ±[ur.d> /u]F is in bse^, then respectively ± [ 1 ^ ^ / M J F is in bse^. Induction step: a > y. Assume c) that that for all (5, y<fi < a, for all formulas F , if ±[ix.<%> / u]F is in bsep, then respectively ± [ ^ 0 / M ] F is in foe^. We want to show that for all formulas F , if ±[u:.d> / w ] F is in bsea, then respectively i t / ^ 0 /u]F is in foea. So let F be any formula such that ±[\x.®/u]F is a signed sentence in bsea We show that respectively ±[* ^ / « ] F is in bsea. For limit ordinals CC Since foea = KJbsep, G < /J < a, the claim holds trivially by hypothesis of induction c). For successor ordinals a: We may assume that for no f3 < a is ± [ I X . < I > / M ] F in bsea, since otherwise, by the hypothesis of induction, the claim holds trivially. Then ±[ix.®/u]F is in Sc(bsea_j). There are five subcases: subcases in which ± [ u r . d > / « ] F is in Sc(bsea_l) by virtue of an instance I of one of semantic rules 1.3.2.1, 1.3.2.2., 1.3.2.3., 1.3.2.4., are treated as subcases i) - iv) of case a) above. So we consider only the subcase where I is an instance of the semantic rule for descriptions 1.3.2.5. Then there are two sub-subcases: 1) It is not the case that, for some constant term r and variable v, both of the following hold: i) the presuppositions to I are of the form +[r / x]&, + ( J C ) ( V ) ( ( < P A [ V / x]&) —> x = v). ii) the major statement to I is respectively of the form ±[r/u]F. Then F is of the form [iz. f /y]G, for some constant description term iz. f a n d formula G, and the presuppositions, respectively, major statement to I are of the form +[s / z] % +(z)(v)(( ,r Y A [v / z ] f ) -» z = v), respectively, ±[ur.<P/u][s /y]G = ±[s /y][ix.&/u]G, for some constant term s and variable v. So bse^ contains all of +[s I z] % + ( Z ) ( V ) ( C P A [ V / z] *P) -» z = v), respectively ±[u:.d>/u][s /y]G. Then by hypothesis of induction c), bsea-l contains 29 all of +[s I z] *F, +(z)(v)((f A [v / z] f ) -> z = v), respectively ±[1^ 0 /«][s /y]G = ±[s / v ] ^ ^ / M J G . S O , by semantic rule 1.3.2.5., Sc(bsea_j ) Q &,yea contains respectively t f i z - f /ylit^/ujG = ±[/ w ( S/«][iz.y //v]G s 1 ^ / M J F . So the claim holds. 2) The presuppositions to I are of the form +[r/x]&, +(x)(v)((d> A [v / x]&) —> x = v), and the major statement to I is respectively of the form ±[r/u]F, for some constant term r and variable v. So bsea_} contains all of +[r / x]®, +(x)(v)((<P A [v / x]d>) -> x = v), respectively ±[r/u]F. Since a - 1 < fj., by the hypothesis of induction b), we may assume that r is in b(Par). But we established that the signed sentence +[t & I x]& belongs to bse . Since y < a, bsevQ bsea_j. So all of +[^4,/ x]®, +[r I x]®, +(x)(v)((® A [V / x]0) -> x = v), are in bsea_1 . Since +(x)(v)((<P A [v / x]®) —> x = v) is in bsea_t , it is easily verified that by semantic rule 1.3.2.4. there is a < a - 1 such that +(([^.0 / x\® A [S I x]®) ^ ^ = s) is in bsep. Then, it is easily verified that by semantic rule 1.3.2.3. there is a £< /? such that one of -(LX .^ x ]® A [s I x]®), +(^0 = s) is in bse^. Assume that -([t^ 01 x ] ® A [S I x]®) e. bse^. Then it is easily verified that by semantic rule 1.3.2.2. there is a A < £ such that one of -[/ ^ / x]®, -[s/x]d> \s'mbsex. Since X<C,< fi< a- 1, A < a - 1, and hence fae^Qfae^ . So both of +[^0 / x]d>, +[s I x]® and one of -[t^^ I x]<2>, -[s I x~\® is in foea_; . So there is a sentence sn/ such that both of ±snt are in bsea_t. Since a - 1 < fi, this contradicts hypothesis of induction a). So the signed sentence +(^.0 = s) is in bse^ bsea_t. So by lemma 1.3.8., since ±[5 /u]F is in bsea_{ , respectively ±(7^ ^ /uJF is in bsea-l ^ foea. So the claim holds. In all cases, then, respectively ±[/lx_<&/«]F is in &yea This completes the inner induction step of the proof that bse^ satisfies lemma 1.3.10.. Thus, the outer induction step of the proof that for all ordinals fl, bse^ satisfies lemma 1.3.10., is now complete. We now complete the induction step of the proof that bse^ satisfies lemma 1.3.9.: Let snt be any sentence. Assume, contrary to that which is to be shown, that bse contains both of ±snt. Since the sequence (bsej is well ordered under c, there are least P, y, 0 < fi, y< fi, such that +snt e bsep and -snt e bsey . Now, by definition 1.3.3., bsep = bsep KjSc(bsep_1) and bsey = bse^ KjSc(bse^. Since for no £, a such that £< /Jand a< yis +snt e bser, -snt e bseait follows that +snt e Sc(bsep_1) and 30 -snt € Sc(bsey_j). There are two cases: 1) snt contains no occurrence of any description term. Then there are just four subcases: i) snt is of the form — i A for some sentence A. Then +—iA is in Sc(bsep_l) and —>A is in Sc(bsey_}) by virtue of semantic rule 1.3.2.1.. and so -A e bse^ and +A e bse^ . Assume, without loss of generality, that y< p. So bse^j ^ bsep_t and hence both of ±A are in bsep_x . Since P<n, p- I < /i. So there is a p<n such that both of ±A are in bsep . This contradicts hypothesis of induction a). ii) snt is of the form (A A B) for some sentences A, B. Then +(A A B) is in Sc(bsep_1) and -(A A B) is in ScQjse^j) by virtue of semantic rule 1.3.2.2. and so both of +A, +B are in bsep_} and one of -A, -B is in bse^_j. Assume, without loss of generality, that y < p. Then both of +A, +B and one of -A, -B are in bsep_l. Then either both of ±A or both of ±B are in bsep_1. Since P < fi, P — 1 < fi. So there is a P < jj. and a sentence snt such that both of ±snt are in bsep . This contradicts the hypothesis of induction a). iii) snt is of the form (A —> B) for some sentences A, B. This case is similar to case ii) above. iv) snt is of the form (x)F for some formula F. Then +(x)F is in Sc(bsep_l) and -(x)F is in Scibse^j) by virtue of semantic rule 1.3.2.4. and so +[t I x]F is in bsep_j for all terms t e h(Par) and -[r / x]F is in bse^j for some term r e 8(Par). Assume, without loss of generality, that y< p. Then both of +[r / x]F, -[r / x]F are in bsep_t. Since /J</z , /?- l</z . So there is a P < fl and a sentence [r / x]F such that both of ±[r / x]F are in bsep . This contradicts hypothesis of induction a). 2) snt contains an occurrence of some description term and so is of the form [ix.&/u]F for some description term ix.& and formula F containing free occurrence of u.. In case neither +snt e Sc(bsep_^) nor -snt e Scibse^ by virtue of the semantic rule for descriptions 1.3.2.5., this case reduces to case 1) above. So assume, without loss of generality, that +snt e Sc(bsea,) by 31 virtue of an instance B 1.3.2.5.. Then there are two subcases: i) -snt e Scibse^j) by virtue of an instance G of 1.3.2.5.. Since +[ur.&/u]F e Sc(bsep_1) by virtue of B, bsep_t contains the two presuppositions +[s I x]0, +(x)(v)((d> A [V / x]0) -> x = v), as well as the major statement +[s/u]F, to B, for some constant term s and variable v. And since -[ix.0/u]F e Sc(bse^ by virtue G, bse^j contains the existential presupposition +[r / x]0 and the major statement -[r /u]F to G for some constant terms r. Since y - 1 < fi, both of s, r may by hypothesis of induction b) be assumed to belong to 8(Par). Then, since y - 1 < n, it follows from hypothesis of induction a), by an argument similar to the one given in the outer induction step for the proof of lemma 1.3.10., that the signed sentence +(s = r) belongs to bse. So, by lemma 1.3.8., since both of +(s = r), -[r I x]0belong to bse^_}, it follows that the signed sentence -[s I x]0 belongs to bse^j . So both of ±[s I x]& belong to bse^ . This contradicts hypothesis of induction a). ii) -snt e ScQjse^) by virtue of an instance G of some semantic rule other than 1.3.2.5.. Since +[xx.0 /u]F e Sc(bsep_1) by virtue of B, bsep_} contains the two presuppositions +[s I x]0, +(x)(v)((0 A [v / x]0) —» x = v), as well as the major statement +[s /u]F, to B , for some constant term s and variable v. Let us suppose that G is an instance of 1.3.2.2.; the other cases are similar to this one. Then F is of the form (G A H) for some formulas G, H. Since -[lx.0 / u](G AH) = -([ur.d> /u]G A [IX.0 /U]H) e Sc(bse^_j) by virtue of G, bse^{ contains one of the signed sentences -[lx.0 /u]G, -[ix.0 /u]H. Now, since y - 1 < fi, it follows from hypothesese of induction a) and b), by the argument given in the outer induction step for the proof of lemma 1.3.10., that there are £ < y - 1 and/^^e 8(Par)such that bse^ contains the signed sentence +[fu:<&/ x] & and bse^j contains one of the signed sentences -[t^^/ujG, -[t^^/ u]H. Assume, without loss of generality, that y< fi. So bserQbse^ ^ bsep_t and hence all of + ^ix.0 1 xl0> +[* 1 xl0> +(x)(v)((® A [v / x]0) x = v), +[s /u]F = /U]G A [s / u]H), and one of -[t^^/^G, -[t^^/u]H are in bsep_t. Since p-1 < jU and all of +[^$1 x]0, +[s I x]0, +(x)(v)((d> A [v/ x]0) —> x = v) are in bsep_t , it follows from hypothesis of induction a) that the signed sentence + ( ^ 0 = s) belongs to bse. So, by lemma 1.3.8., since 32 +(/u. 4,= s) and one of -[t^^/ujG, -[t^^/ulH both belong to bsep_}, it follows that one of -[s /u]G, -[s /u]H belongs to bsep_{. Now, formulas G, H are respectively of the form hz.*¥ I x]G\ \vy.S I x]H'. for some formulas G', H' containing no occurrences of any constant description terms, where the iz. *F = \z1.xFl, . . ., izn.H/n , iv.E = vyl.El, . . ., ivm .Smare all of the constant description terms occurring in G, H. So bsep_j contains +[s/u]F = +([s /u]G A [S/U]H) = +([s /u)hz.*F/ x\G' A\S /u\\ iv.S I J C W ) and one of -\s /u\\\z. *¥l x\G'. -\s/ii\\\y.EI x\H'. Since P- 1 < jU, by hypothesis of induction b), there are t^= t l z I v l , . . ., V « . f l , . ^ s ^ £ i ' • • W a » in 8(Par) such that bsep_1 contains +([5 / M ] ^ y / x]G' A [5 /u][^z j /x j / / ' ) and one of -[5 / "][4Z xpl i ]G ' , -[5 / « ] [ I l z S / £ W - Now, since neither of G \ / / ' contain an occurrence of any constant description term, ([s/u]^ w l x]G' A [S/u][tu ~Ix}Hr) contains no occurrence of any constant description term. Since bse^ contains +([s /u]|j l z y / x\G' A [S/u][tlz ~ 1'x\H"), there is a least £< j8- 1 such that bse^ contains +([s /u][j l z.y/ x\G' A [S /u\\t^zEl X^H"). S o +([S / »][4Z yl *JG' A [s/u][tlzE/x]H") is in ScQjse^). Moreover, since ([s /«][4 Z ^ *]G' A [5 / M ] [ j l z g / 1 x ] / / ' ) contains no occurrence of any constant description term, +([s /u][tlzT/ x]G' A [S / u][£lz-/x]H') is in Sc(bse^_}) by virtue of semantic rule 1 . 3 . 2 . 2 . . So bse^_t contains both of +[s /m][4z y/ i]G' , +[5 /MJIJ^g/*]//'. Since bse^_t ^ foe^, it follows that bsep_1 contains both of +[s/u\{t^l x]G', +[s /wJIX^/*] / / ' and one of -[s / u ] [ ^ / i]G' , -[s / M ] ^ / * ] / / ' . So there is a P < jj. and a sentence 5/1/ such that both of ±snt are in bsep . This contradicts hypothesis of induction a). In all cases then, the assumption that both of ±snt are in bse leads to a contradiction. This completes the induction step of the proof that for all ordinals fi, bse satisfies lemma 1 . 3 . 9 . . Thus, the proofs of lemmata 1 . 3 . 9 . and 1 . 3 . 1 0 . are now complteted. • Lemma 1 . 3 . 1 1 . : Let bse be any base and let ix.d> be any constant description term such that for some constant term rand variable v, Cl(bse) contains both of the signed sentences +[r/x]&, +(*)0)((<P A [v / x]&) —> x = v). Let t #e 8(Par) be a descriptum of ix.® in bse . Then, 33 for all formulas F, if ±[f ^ / u]F is a signed sentence in Cl(bse), then so is respectively ±[u\d> lu]F. Proof of 1.3.11.: Let bse, ix.0 and t^ 0 be as above. Assume that, for some formula F, ±[^$,1 u]F is a signed sentence in Cl(bse). We want to show that respectively ±[ix.0/ u]F is in in Cl(bse). Since Cl(bse) = KJbse^ ,0</i<e.0, respectively ±[7^ ^ / j>]F is in toe^ for some £< G 0. Since Cl(bse) contains both of the signed sentences +[r/x]0, +(x)(v)((d> A [ V / x]<P) -> x = v), there are P,y<e0such that +[r / x]<Z>e toe^and +(x)(v)((d> A [V / x]d>) -> * = v) e foe^ . Assume, without loss of generality, that P <y. Then bse^Q toe^and so bse^ contains both of the signed sentences +[r / x]0, +(x)(v)((d> A [V / x]0) —> a: = v). So, by an instance of 1.3.2.5. whose major statement is +[r/ x]<P, Sc(bseJ Q bse^j contains the signed sentence +[xx.0 I x]0. Then by lemma 1.3.10., bse^{ contains the signed sentence +[^4, I x]0. There are two cases: i) £< y. Then bsey+1 contains both of +[1^ ^ / x]&, +(x)(v)((<3> A [V / X]&) -> x = v), as well as respectively tU^ 0 /y]F. Hence, by 1.3.2.5., Sc(bsey+1) Q Cl(bse) contains respectively ±[ur. 0/ y]F. ii) £ > y. Then bse^ contains both of +[/ lx -<p /x]0 , +(x)(v)((0 A [ V / x]0) -» x = v), as well as respectively ± 1 ^ ^/,y]F. Hence, by 1.3.2.5., Sc(bse^ Q Cl(bse) contains respectively ±[ix.0/y]F. • The significance of lemma 1.3.10. is that it guarantees that for every base bse and every constant description term t, there is a basic terms representing or "covering" t in bse. This fact is crucial to the soundness proof of the next section. 34 Section 2: A Soundness Result for Pld. We say that Pld is semantically sound iff every derivable sequent is valid. In this section we show that Pld is (semantically) sound. Lemma 2.0.: Let bse be any base, s any constant term, uc.d> any constant description term, and F any formula containing free occurrence of the variable u. Then, for all ordinals /i, ifbse contains both of the signed sentences respectively ±[s I u]F, +[ur.d>/ u]F, then, for some constant term t and variable v, bse^ contains both of the signed sentences +[/ / x]d>, + ( A T ) ( V ) ( ( < P A [ V / x]<P) —> x = v). Proof of 2.0.: Let bse be any base, s any constant term, ix.& any constant description term, and F any formula containing free occurrence of the variable u. Assume that bse^ contains both of respectively ±[s I u]F, +[ixd>/ u]F, and, contrary to that which is to be shown, for no constant term t and variable v does bse contain both of the signed sentences +[/ / x]<J>, +(x)(v)((& A [v / x]0) —» x = v). By definition 1.3.3., bse^ = ^Jbsep , 0 < p < fl, so, since +[ur.d> / u]F belongs to bse^, there is a p < fl such that +[ix.&/ u]F e bsep. Now, since ix.& occurs in the signed sentence +[ur.d>/ u]F e bsep and (bse^) is well ordered under Q, there is a least£< P such that ix.0 occurs in some signed sentence ssnt in bse^. We now establish the following claim: Claim: Let F be any formula containing free occurrence of a variable u ands be any constant term such that bse contains both of the signed sentences respectively ±[s I u]F, +[uc.d> / u]F. Then, there is j3-</x such that for no y< p does ur.d> occur in any signed sentence in bsey and for some sentence A and formula G containing free occurrence of u, one of the following two conditions holds: i) there is a sentence of the form (A A [s I u]G), ([s / u]G A A) such that bsep contains the signed sentence -(A A [IX.<P/ u]G), -([s / u]G A A) as well as the signed sentence +(A A [s I u]G), 35 +([s I u\G A A ) ii) there is a sentence of the form ( A — »[s I u]G), ([s I u]G —> A ) such that bsep contains the signed sentence + ( A —> [tx.<P/ u]G), +([ix.CP/ u]G —> A ) as well as the signed sentence - ( A -> [s I u]G), -([s I u]G - » A ) . Proof of claim: Let F be any formula containing free occurrence of u ands be any constant term such that bse contains both of the signed sentences respectively ±[s I u]F, +[ix.®/ u]F. We show by induction on / i for fx > £ that there is/? < i i such that for noy<P does ix.d> occur in any signed sentence in bsey and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. Base step: fi = C • Clearly, fi is a successor ordinal. So bse = bse , u Scibse ,). Since + [ix.® I u]F e bse^ and for no < fi = £ does +[ur.d> / u]F occur in foe^, it follows that +[ix.® / u]F e Sc(bse^_j) by virtue of an instance I of some semantic rule. Since u\d> is a constant term and for no p < fl = £ does ur. ® occur in any signed sentence in bsep, it follows that I is not an instance of either of the semantic rules 1.3.2.1., 1.3.2.4.. By assumption, for no constant term / and variable v does bse ^>bse ,, and hence bse , , contain both of the signed sentences +[t I x]®, +(JC)(V)((<2> A [ V / x] d>) —> x• = v), so I is not an instance of the semantic rule for descriptions 1.3.2.5.. Then there are just two cases: a) l i s an instance of the semantic rule 1.3.2.2.-.. Then, for some sentence A containing no occurrence of ix.d>and some formula G containing free occurrence of u, +[tx.<P/ u]F is of the form of one of - ( A A [ix.d> / u]G), -([tx.® / u]G A A ) , where bse , contains - A . Then ±[s I u]F is of the form + ( A A [S I u]G), +([s / u]G A A). So /x is such for no p < fi does ix.<J> occur in any signed sentence in bsep and bse^ contains - ( A A [ I X . < P / u]G), -([ix.® / u]G A A ) as well as - ( A A [ I X . < P / u]G), -([ix.®/u]G A A ) . So condition i) holds. b) l i s an instance of the semantic rule 1.3.2.3.+.. Then, for some sentence A containing no occurrence of ix.<Pand some formula G containing free occurrence of u, +[\x.®/ u]F is of the 36 form of one of +(A —> [ut.d> / w]G), +([\x.&I u]G —> A), where bsejX_l contains -A, +A. Then ±[5 / u]F is of the form -(A -> [s / w]G), -([s / u]G —> A). So fx is such for no P < fx does u\d> occur in any signed sentence in bsep and bse^ contains +(A -> [ix.d> / u]G), +([ur.d>/ «]G -> A) as well as -(A -> [s / u]G), -([s I u]G -> A). So condition ii) holds. In both cases, then, one of conditions i), ii) holds. Induction step: fx > £ . Assume that for all 7, £ < y< fx, for all formulas H containing free occurrence of u and all constant terms t such that bsey contains both of the signed sentences respectively ±[t / u]H, +[vc.&/u]H there is p < 7 such that for no y< does ix.&occur in any signed sentence in bse^ and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. For limit ordinals 11: The claim holds trivially by the hypothesis of induction. For successor ordinals fi: Now, bse^ contains both of respectively ±[s / u]F, +[ix.& I u]F. Since by assumption s is a constant term, by lemma 1.3.10, we may assume that s is in 8(Par). Let u . f b e any constant description term occurring in Fand let F' be the result of uniformly replacing every occurrence of u . f i n F by a descriptum t^yfor U - f in bse whose existance is guaranteed by lemma 1.3.10. By lemma 1.3.10, bse contains both of respectively ±[s I u]F\ +[ix.&I u]F'. Since bse^ = KJbsep ,0<P<fi, and (bsej is well ordered under there are least 7, < Li such that ± [s I u]F' e bseyan& respectively + [ur. 01 u]F' e bsep. Clearly, p is a successor ordinal, and so bsep = bsep_} u Sc(bsep_1). So +[uc.d> / u]F' e Sc(bsep_1) by virtue of an instance G of some semantic rule. Since F' contains no occurrence of any constant description term, and for no constant term t and variable v does bse^ d bsep_} , and therefore bsep_1 .contain both of the signed sentences +[tI x]0, +(x)(v)((d> A [v / x]<P) -> x = v), it follows that G is not an application of the rule for descriptions 1.3.2.5.. So there are just four cases: 1) G is an instance of 1.3.2.1.. Then F' is of the form —>H for some formula H and so +[ut.d>/ 37 u]F' = +[vc.&/«]—iH. So bsep_j contains respectively ±[ix.&/u]H. Now, foe^contains respectively ±[5 / u]F' = ±[s I u\—H. Since [s I u]—H is not atomic, 0. Clearly, then, yis a successor ordinal, and so bse^= bse^_x u Sc(bse^_j). Since for no K"<y does foe ^ contain ±[s I u]—iH, it follows that ±[s I u]—iH e Sc(bse^_j) by virtue of an instance B of some semantic rule. Since ±[s I u]F' = ±[s I u]—H contains no occurrence of any constant description term, it follows that B is not an application of the rule for descriptions 1.3.2.5.. Then B is an instance of 1.3.2.1.. So bse^j contains respectively +[s I u]H. Assume, without loss of generality, that P >y. Then bse^j Qbsep_t and so bsep_1 contains both of respectively ±[vc.&/u]H, +[s I u]H. Clearly, since u has free occurrence in F' = —H, it follows that u has free occurrence in H. Since <fi, P - I <ii, so by the hypothesis of induction, there is T] < P~ 1 such that for no y < 77 does uc.d> occur in any signed sentence in toeyand for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. Since p <f±, 77 <fi. Hence, there is a 77 < /! such that for no y< T] does ix. <P occur in any signed sentence in frse^and for some sentence A and formula G containing free occurrence of «, one of conditions i), ii) hold. So the claim holds. 1) G is an instance of 1.3.2.2.. Then F' is of the form (G AH) for some formulas G, H and so + [ur.d> / u]F' = +[vc.&I M ] ( G AH) = +([\x.&I u]G A [\X.&I u\H). So bse^ contains one of -[ix.01 M ] G , -[ur.d> / u]H respectively both of +[ix.01 u]G, +[ix.&I u]H. Now, foe^contains respectively ±[s I u]F' = ±([s / u]G A [S I u]H). Since ([s I u]G A [S I u]H) is not atomic, P * 0. Clearly, then, P is a successor ordinal, and so bsep = bsep_} u Sc(bsep_I). So ±([s / « ] G A [s I u]H) e Sc(bsep_j) by virtue of an instance B of some semantic rule. Since ±[s I u]F' = ±([s I u]G A [s I u\H) contains no occurrence of any constant description term, it follows that B is not an application of the rule for descriptions 1.3.2.5.. Then B is an instance of 1.3.2.1.. So bsep_j contains both of +[s I u]G, +[s I u]H respectively one of -[s I u]G, -[s I u]H. Assume, without loss of generality, that P>y. Then bsep^ contains both of +[s I u]G, +[s I u]H and one of -[tx.d> / u]G, -[ix.&/ u]H respectively one of -[s I u]G, -[s I u]H and both of +[ix.&/ u]G, +[ix. &/ u]H. Now, we show that there is a formula K containing free 38 occurrence of u such that bsep_} contains both of ±[t I u]K, +[\x.® / u]K; clearly, this result follows if both of G, H contain free occurrence of u. So assume that it is not the case that both of G, H contain free occurrence of u. Since u has free occurrence in F' £ (G AH), U has free occurrence in one G, H. So assume, without loss of generality, that G contains free occurrence of u but H does not. In this case, [s I u]H £[ix.® I u]H. It follows that bsep_t does not contain -[tx.® / u]H = -[s I u]H, for suppose it does: Then, contrary to lemma 1.3.9., bsep_t contains both of +[s I u]H, -[s I u]H. Since bsep_j does not contain-[ix.® / u]H £ -[s I u]H, it follows that bsep_j contains both of +[s I u]G, -[ix.® I u]G respectively both of -[s I u]G, +[vc.® I u]G. So there is a formula K containing free occurrence of u such that bsep_l contains both of ±[t/u]K, +[ix.® / u]K. Since fi<fi, - 1 <fi, so by the hypothesis of induction, there is a 77 < p- 1 such that for no y< r/ does ur. ® occur in any signed sentence in bse^and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. Since P<LL, f] < ju. Hence, there is a 77 < fi such that for no y< r\ does xx.® occur in any signed sentence in bse^and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. So the claim holds. 3) G is an instance of 1.3.2.3.. This case is similar to case 2) above 4) G is an instance of 1.3.2.4.. Then F' is of the form (z)H for some formula H and variable z and so +[ix.®/u]F' = +[ix.® I u](z)H = +(z)[ix.® I u]H. So bse t contains -[t/ z][ve.® I u]H for some t e 8(Par) respectively +[/ / z][ix.® I u]H for all t e h(Par) Now, bsep contains respectively ±[s I u]F' = ±[s I u](z)H = ±(z)[s I u]H. Since (z)[s I u]H is not atomic, P * 0. Clearly, then, P is a successor ordinal, and so bsep = bsep_1 u Sc{bsep_1). So ±(z)[s I u]H e Sc(bsep_j) by virtue of an instance B of some semantic rule. Since ±[s I u]F' £ ±(z)[s I u]H contains no occurrence of any constant description term, it follows that B is not an application of the rule for descriptions 1.3.2.5.. Then B is an instance of 1.3.2.4.. So bsep_l contains +[t I z][s I u]H for all t e d(Par) respectively -[t I z][s I u]H for some / e 8(Par). Clearly, since u has free occurrence in F' £ (z)H, u has free occurrence in H. Assume, without loss of generality, that P>y. Then bse»_I contains -[/ /z][ix.® I u]H for some / e 8(Par) and +[t I 39 z][s I u]H for all t e b(Par) respectively +[/ / z][ix.0/ u]H for all t e b(Par) and -[t I z][s I u]H for some / e &(Par). Clearly, then, since [/ / z\[ix.0I u]H = [ix.0/ u][t I z]H and [/ / z][s I u]H = [s I u][t I z]H, it follows that [/ / z]H is a formula containing free occurrence of u such that bsep_t contains both of ±[f / u][t I z]H, +[\x.0l u] [t I z]H . Since J3 </!, /3 - 1 <ju, so by the hypothesis of induction, there is a 77 < /3 - 1 such that for no y< 77 does ix.0 occur in any signed sentence in bse^and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. Since <pi, 77 < /!. Hence, there is a 77 < fi such that for no y< 77 does xx.0occur in any signed sentence in bse^and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) hold. So the claim holds. In all cases then, there is a (3 < fi such that for no y< ft does vc.O occur in any signed sentence in bse^ and for some sentence A and formula G containing free occurrence of u, one of the following two conditions holds. This completes the induction step of the proof of the claim. We now return to the main proof of lemma 2.O.. Since bse^ contains both of respectively ±[s I u]F, +[ix.0/ u]F, by the claim, there is a P < fi such that for no y< f5 does ix.0 occur in any signed sentence in bse^ and for some sentence A and formula G containing free occurrence of u, one of conditions i), ii) holds. Assume, without loss of generality, that condition i) holds. Then, there is a sentence of the form (A A [S I u]G), ([s I u]G A A) such that bsep contains the signed sentence -(A A [IX.0/ U]G), -([IX.0/ U]G A A) as well as the signed sentence +(A A [S I «]G), +([s I u]G A A). Since by assumption s is a constant term, by lemma 1.3.10, we may assume that s is in 8(Par). Let iz-fbe any constant description term occurring in A or in G, and let respectively A ' , G ' be the result of uniformly replacing every occurrence of tz- f in respectively A' , G ' by a descriptum <lz,«j/for iz.*Fin bse whose existance is guaranteed by lemma 1.3.10. By lemma 1.3.10, bsep contains both of -(A' A [ix.01 u]G'), -([ix.01 u]G' A A') as well as the signed sentence +(A' A [S I u]G'), +([s I u]G' A A') . Clearly, is a successor ordinal, and so bsep = bsep_1 u Sc(bsep_j). Since for no y< (3 does xx.0occur in any signed sentence in bsey, it follows that -(A' A [\X.0I u]G'), -([\x.01 u]G' A A') does not belong to foe„ , . So -(A' A [IX.0 I u]G'), -([ix.01 u]G' A 40 A') belongs to Sc(bsep_j) by virtue of an instance B of some semantic rule. Since neither A nor G contains an occurrence of any constant description term, and for no constant term t and variable v does bse^> bse^_1 , and therefore bsep_l , contain both of the signed sentences +[t/x]&, +(x)(v)((<2> A [v / x]<P) —> x = v), it follows that B is not an instance of the semantic rule for descriptions 1.3.2.5.. Hence, B is an instance of 1.3.2.2., and so bsep_t contains -A ' . Since bsep contains the signed sentence +(A' A [S I u]G'), +([s I u]G' A A'), there is a least y</3 such that bsey contains the signed sentence +(A* A [S I u]G'), +([s I u]G' A A ' ) . Clearly, yis a successor ordinal, and so bsey= bse^ u Scibse^). Since +(A' A [S I u]G'), +([s I u]G' A A') does not belong to bsey_l, +(A' A [s I u]G'), +([s I u]G' A A') belongs to Sc(bsep_j) by virtue of an instance G of some semantic rule. Now, +(A' A [s / u]G'), +([s I u\G' A A ' ) contains no occurremce of any constant description term, B is not an instance of 1.3.2.5.. Hence, G is an instance of 1.3.2.2., and so bsey_l contains both of +A', +[s / u]G'. Assume, without loss of generality, that y>/3. Hence, bsep_{ Qbsey_}. So bse^j contains both of ±A\ This contradicts lemma 1.3.9.. Thus lemma 2.0 is established. • Theorem 2.1.: Let Seq be any sequent. If Seq is derivable, then Seq is valid. Proof of 2.1: Let Seq be any derivable sequent. Let £ = Pj , . . . , pn be an n-ary vector on farcontaining all of the parameters which occur in some member signed sentence of Seq. We need to show that for all bases bse and all n-ary vectors t = t1, . . ., tn on hiPar), [£ / p\Seq n Cl(bse) * 0 , from which it follows by definition 1.3.5. and 1.3.6. that Seq is valid. So let bse be any base and t any n-ary vector on Par. Since Seq is derivable, by definition 1.2.4., there is a derivation tree FI such that Seq is the endsequent of II. We show by strong induction on the depth D(Jl) that [t I pJSeq n Cl(bse) * 0 . Base step: 0(TI) = 0. Then by 1.2.6. Seq is an axiom and so by 1.2.1. there are two cases: i) Seq is of the form {-asnt, +asnt) for some atomic asnt. Since the I are all members of hiPar), \ilp}asnt is an atomic sentence. So by condition 1) of 1.3.1., one of ±\tlp\asnt belong to bse. Hence {-\tlp\asnt, +[tlp\asnt) = [tlg]{-asnt, +asnt] = [tlp^Seq n Cl(bse) 41 0 . ii) Seq is of the form [+(t = t)} for some / e b(Par). Clearly, [II u\t e 5(Par), so by condition 2) of 1.3.1., the signed atomic sentence +([tI &}t = [tly^t) belongs to bse. So {+([tI U\t= [tlu\t)} s [ | /£]{+(/= 0} = [LIalSeq n Cl(bse) * 0 . In both cases, then, [£ / j^Seq n Cl(bse) * 0 . Induction step: Assume valid all sequents which are derivable as endsequents of derivation trees £ such that D(L) < B(YI). We show that [/ I g]Seq n Cl(bse) * 0 by considering eight cases corresponding to the eight deductive rules given in 1.2.2. applications of which Seq may be the conclusion in II: i) Seq is the conclusion of an application A of the thinning rule 1.2.2.1.±. Then Seq is respectively of the form Seq' u {±snt} for some sequent Seq' and sentence snt, where Seq' is the premise to A . Then Seq' is the endsequent of IPs deepest proper subtree E. Since D(L) < B(Tl), by the hypothesis of induction, Seq' is valid. So, by definition 1.3.6., [t/g]Seq' n Clibse) * 0 . Trivially, then, ([£/j^Seq' U [t/&\{±snt}) & [tl &\(Seq' u {±snt}) n Cl(bse) * 0 . So n C/(foe) * 0 . ii) Seq is the conclusion of an application A of 1.2.2.2.±. Then Seq is respectively of the form Seq'u {+-nA} for some sequent Seq' and sentence A, where respectively Seq'u {±A} is the premise to A . Then Seq' u {±A} is the endsequent of Li's deepest proper subtree E. Since D(L) <£J(IT), by the hypothesis of induction, Seq'u {±A} is valid. So, by definition 1.3.6., U I £]( Seq' u { ±A}) = ([t I u\Seq' u [t I Q\ {±A}) n Clibse) * 0 . There are two cases: a) [iI£\Seq' nCl(bse) * 0 . Trivially, then, respectively ([tI fi\Seq' u U.IB\{ +-.A}) = [tl U\(Seq' u {+-iA}) n Cl(bse) * 0 . So [f / fiJSkg n C/(foe) * 0 . b) [t/E}Seq' n C7(fae) = 0 . Then, since respectively (ut/£]&9' u [£/£]{±A}) n <C7(fae) * 0 , it follows that respectively ±[£/^JA e Cl(bse). So, by semantic rule 1.3.2.2.±, 42 respectively £]-.A e Sc(Cl(bse)). By lemma 1.3.7., Sc(Cl(bse)) Q Clibse), so +(i/£]-iA e Clibse)). Hence, respectively ([£/£]S<etf'u {+li/£]-"A}) s [l / j2](Se#'u {+-iA}) n C/(fae) ?t 0 . So U / n CT(tae) * 0 . iii) Seq is the conclusion of an application A of 1.2.2.3.±.. We separate the two cases: 111.1) Seq is the conclusion of an application A of 1.2.2.3.+.. Then Seq is of the form Seq' u {+(A A B)} for some sequent Seq' and sentences A , B. Then there are sequents Seql,Seq2 such that Seq' = Seql u Seq2 and Seql u {+A}, Seq2 u {+B} are the premises to A . Then both of Seql u {+A}, Seq2 u {+B} are endsequents of proper subtrees respectively £ y , Z 2 of IT Since D(Lj), D(L2) < D(Yl), by the hypothesis of induction, both of Seql u {+A}, Seq2 u {+B} are valid. So, by definition 1.3.6., \ilg](Seql u {+A}) = (\tl ]£Seq2 u {+[£ /U\A}) n Clibse) * 0 and [tl's\(Seq2 u {+B}) = (&I]&Seq2 u {+U//i]B}) n C/(toe) * 0 . There are two cases: iii.l.a) (\t/u\Seql u U/u\Seq2) n Cl(bse) * 0 . Since S ^ ' = u Se^2, it follows that [t/u\Seq' = ([tl^Seql u \t/n]Seq2). So [£//2]&^' n C/(toe) * 0 . Trivially, then, ([*/ /iJSe^'u [£//2]{ +(A A B)}) s [tl£(Seq'KJ {+(A A B)}) n Cl(bse) * 0 . So WBiSeq n C/(fo<?) * 0 . iii.Lb) ([t/B\Seql u K / ^ ) n C / ( k ) =0 . Then, since ([f/jd&tfi u {+[£//z]A}) n C/(foe) * 0 and ([f/£]&??2 u {+[£/^]B}) n C/(toe) * 0., it follows that both of +[/ /£]A, +[//£]B e CT(foe). So, by semantic rule 1.3.2.3.+, +([|//z]A A [ / / # ) S +{tf £](A A B) e £c(C/(6se)). By lemma 1.3.7., Sc(Cl(bse)) c Cl(bse), so +[r/£](A A B) G Cl(bse)). Hence, / u {+U / £](A A B)} = [t / g](Seq' U {+(A A B)}) n C/(iwe) * 0 . So [/ / UlSeq n C/(6se) * 0 . 111.2) Se^ is the conclusion of an application A of 1.2.2.3.-.. Then Seq is of the form Seq' u {-(A A B)} for some sequent Seq' and sentences A , B, where Seq' u {-A , -B)} is the premise to A. Then Seq' u {-A, -B)} is endsequent of ITs deepest proper subtree E. Since 43 D(Z) <D(H), by the hypothesis of induction, Seq' u { - A , -B)} is valid. So, by definition 1.3.6., UlBMSeq'yj { - A , - B ) } ) £ ([H ulSeq' u [tlp}{-\ , - B ) } ) n Cl(bse) * 0 . There are two cases: iii.2.a) (UIPlSeq'n Cl(bse)* 0 . Trivially, then, ([£I$Seq' u [ £ / £ ] { - ( A A B ) } ) £ [ ( . / pl(Seq' u { - ( A A B ) } ) n Cl(bse) * 0 . So [tlp^Seq n C/(fee) * 0 . iii.2.b) (\i/B}Seq'nCl(bse) = 0 . Then, since (\i/B\Seq' u [ * / £ ] { - A , - B ) } ) n C7(foe) * 0 , it follows that [t/pj{-A , - B ) } ) n Cl(bse) * 0 and hence that one of A , - | i / £ ] B belongs toC/(foe). So, by semantic rule 1.3.2.2.-, -([L/pJA A & / £ ] B ) £ -[L/p2(A A B ) e Sc(Cl(bse)). By lemma 1.3.7., Sc(Cl(bse)) Q Clibse), so - [ / V E R A A B) e Cl(bse)). Hence, [ £ / £ ] S ^ ' u { - [ | / £ ] ( A A B ) } £ [//^](Segp u { - ( A A B ) } ) n Cl(bse) * 0 . S o [ f / £ J & ? # n C/(foe) * 0 . iv) Ste^ is the conclusion of an application of respectively 1.2.2.4.+.. This case is similar to case iii) above. v) Seq is the conclusion of an application A of 1.2.2.5.1.. We separate the two cses: v.l) Seq is the conclusion of an application A of 1.2.2.5.+.. Then Seq is of the form Seq' u [+(x)F] for some sequent Seq' and formula F, where for some q e Par not occurring in any signed sentence of Seq' u { + ( x ) F } , Seq' u [+[q I x]F] is the premise to A . Then Seq' u {+[q I x]F} is endsequent of ITs deepest proper subtree E . Since D(Z) < D(Yl), by the hypothesis of induction, Seq' u {+[q I x]F} is valid. Now, we want to show that Seq' u { + ( x ) F } is valid, that is, we want to show that for all n-ary vectors t on 8(Par), [tlu\(Seq' u {+(x)F}) n Cl(bse) * 0 , wheren is an n-ary vector on Par containing all of the parameters which occur in some member of Seq' u { +(x)F }. Let g_ = ql , . . ., q{= q , . . . , qm be an m-ary vector on Par containing all of the parameters which occur in the members of Seq'KJ {+[qi I x]F] such that q is the fth term of q. Clearly g_ contains all of the parameters which occur in some member of Seq' u { + ( J C ) F } . L e t s ^ s , , . . ., sif . . ., sm be any m-ary vector on, 44 and let r be any term in, b(Par). Let \r / sJis_= s2 , . . ., r , . . ., sm be the m-ary vector which is obtained from s. be replacing the i'th term s{ in £ by r. Since Seq' u {+[q./ x]F} is valid, it follows that [§_l &(Seq' u {+[c7(./ x]F}) = ([s_/ g_]Seq' u Ls_/o] {+[?,•/ x ] F } ) n Cl(bse) * 0 . There are two cases: v.l.a) [s I a\Seq'n Cl(bse) * 0 . Trivially, then, ([s / Q\Seq' v [§_/ Q]{ +(X)F}) = [§_/ 0] (Seq' u {+(x)F}) n Cl(bse) * 0 . So [s / &]&^ n C/(fc re) * 0 . v.l.b) [ j /4 ]%' r iC/ ( foe) = 0 . Since ^ does not occur in any member of &e<g', it follows that [slq\Seq' = [lr / -^Is / So, [Ir / / g]Seq° n Cl(bse) = 0 . But since Se^' u { + [ ^ . / J C ] F } is valid, it follows that [Ir / sjis/g](Seq' u {+[?,./ x ] F } ) £ ([Ir / s.ls / q\Seq' u [Ir / s^ ls / fl] {+[«7(. / x]F}) n O(toe) * 0 . So [Ir / / fl] {+[?,. / x ] F } n Cl(bse) * 0, in other words, +[\r / st\s / g][q(/ x]F e Cl(bse). Now, since all of the terms in \r I s^s are constant terms, [Ir / sfls / Q\[qi I x]F s [r / x][Ir / sJis I q\F. Since qt does not occur in F , [r / *][lr / sjs I Q\F = [r / x][s / fl]F. So +[r / x][s I q\F e Cl(bse). Since r is an arbitrary term in 8(Par), for all r e b(Par), +[r I x][s I g}F e Cl(bse). Hence, by semantic rule 1.3.2.4.+., +(x)[s I g\F = +[£ / £](jc)F e Sc(Cl(bse)). By lemma 1.3.7., Sc(Cl(bse)) Q Cl(bse), so +[s / £ ] ( x ) F e Cl(bse)). Hence, [$/ o J W u {+[£/ aJW^} = [*/ gl(Seq' u { + ( x ) F }) n C/(tae) * 0 . So [t I $Seq n C/(6se) * 0 . v.2) is the conclusion of an application A of 1.2.2.5.-. Then Seq is of the form Seq' u {-(x)F) for some sequent Seq' and formula F , where for some constant term t, Seq' u {-[t I x]F) is the premise to A. Then Seq'^j {-[tl x]F} is endsequent of ITs deepest proper subtree E . Since D(Z) <D(Yl), by the hypothesis of induction, Seq' u {-[t/x]F} is valid. So \tl Ui(Seq' u {-[t/x]F}) = (\lljfiSeq' u [t I ${-[t I x]F}) n C/(toe) * 0 . There are two main cases: v.2.a) [t I BlSeq' n Cl(bse) * 0 . Trivially, then, (UI p}Seq' u [£ /£] {-(x)F }) = [£/ £K&?tf' u {-(x)F}) n C/(tae) * 0 . So fj / n C/(6re) * 0 . 45 v.2.b) [L/plSeq'r>Cl(bse) = 0. Since (U/p]Seq' u [t/pl{-[t/x]F}) n Cl(bse) * 0 , it follows that [£/z\[-[t / x]F}) n Cl(bse) * 0. So -[L/ pj[t / x]F = -[[£/£]* / x][i/pJF e Cl(bse)). There are two subcases: v.2.b.a) [ / /£ ] / e 5(Par). Then, by semantic rule 1.3.2.4.-., -(*)[*/pJF = -[t/pJ(x)F e Sc(Cl(bse)). By lemma 1.3.7., Sc(Cl{bse)) Q Cl(bse), so - [ * / £ ] ( x ) F e Cl(bse)). Hence, [1 u { - U / f i ] ( J c ) F } £ u { - ( x ) F }) n C/(fae) * 0 . So n CJ(foe) * 0 . v. 2.b.P) 8(7°^). Then is a constant description term, so by lemma 1.3.9., there is a descriptum r^t^t G h(Par) for in bse such that -[ r^t/^t/ x][t/pJF e Cl(bse)). So this subcase reduces to v.2.b.a) above. vi) Seq is the conclusion of an application A of 1.2.2.6.. Then Seq. is respectively of the form Seql KJ Seql u SeqS u {±[ix.<P I u]F) for some sequents Seql, Seql,Seq3, description term ix.® and formula F , where for some constant term /, the premises to A are Seql u {+[/ / x\®},Seqlu {+(x)(v)((<P A [ V / x]<P) -> x = v)} and respectively SeqS u { ± { / / K ] F } . Since these premises to A are endsequents of proper subtrees of I i , by the hypothesis of induction, they are all valid. So [tl pl(Seql u {+[t fx]®}) = ([£/pJSeql u [/7 £]{+[/ / x]®}) n Cl(bse) * 0 and [tlpl(Seql u {+(x)(v)((<P A [v /x]d>) -» x = v)}) = ([tlpJSeql u \tl pJi {+(x)(v)((4> A [v / x]CP) -> x = v)}) n Clibse) * 0 and respectively [/ / £](Se^i u {±[/ / "] F}) = / jr]&4? u [1 / £] {± [/ / u]F}) n C/(foe) * 0 . There are two main cases: vi. a) [L/pJSeql u U.I tt\Seq2 U n Cl(bse) * 0 . Trivially, then, [t/pJSeql u U/pJSeql u \i/pJSeqS u {±[ix.CP / M ] F } = \t/pJ(Seql Seql KJ SeqS u {±[ix.c2>/ u ] F } ) n C/(fo<?) * 0 . So [f / ^ f o g n C/(foe) * 0 . vi.b) (U/pJSeql u [1/pJSeql u [ f / f i ] S « « 5 ) n C / ( M = 0 . So, [*/£]{+[*/x]d>} n Clibse) * 0 and [i / { + ( J C ) ( V ) ( ( C P A [v / x] CP) -> x = v)}) n Clibse) * 0 and respectively [i / £]{ + [*/a]F}) n Clibse)* 0. So all of +[*/p][tIx]® = +[[i/pjt/x]Wpj®, 46 pl(x)(v)((& A [v / x]&) - » JC = v) = +(x)(v)(([L I p]& A [v / x][tI pl<$) -» x = v), respectively ±[il pl[tI u]F} = ±[\tI pitI u][L/pJF belong to Cl(bse)). Then, since [tI pit is a constant term, by semantic rule 1.3.2.5., respectively ±[\x.\ilpl&Iu][tlplF = ±[ll pl[\x.&I u]F e Sc(Cl(bse)). B y lemma 1.3.7., Sc(Cl(bse)) Q Cl(bse), so respectively ±[tl pl[xx.® I u\F e Cl(bse)). Hence, [ / / £ ]%! u u u [//fi] {+[u.d»/«]F} £ [|/ pi (Seql u &?2 u Se$3 u {± [ix. 01 u]F}) n C/(&re) * 0 . So U / ^ C/(fae) * 0 . vi i) is the conclusion of an application A of 1.2.2.7.. Then Se^ is respectively of the form Se^l U Seql u {-(r= s)} for some sequents Seql, Seql, and constant terms r, s, where for some formula F, the premises to A are Seql U {+[r / «]F), Se^2 u {-[5 / w]F}. In case w does not occur free in F, [r I u]F = [s I u]F. Then, by the arguement given in case x below, ([t I plSeql u [tlplSeql) n Cl(bse) * 0 , and hence ([tlpJSeql u [£/plSeql v[tlpl{-(r = s)}) = UI pi (Seql u Seql u {-(r = s)}) n Cl(bse) * 0 . So [t I p]Seq n C7(tae) * 0 . So assume that u has free occurrence in F . Since the premises to A are endsequents of proper subtrees of FI, by the hypothesis of induction, they are all valid. So [tl pl(Seql u {+[rl u]F}) = ([tl plSeql u [XIPli+irl u]F}) n Cl(bse) ± 0 and [tl pl(Seql u {-[slu]F}) = ([tl plSeql u [i I pi {-[S I «]F}) n Cl(bse) * 0 . There are two main subcases: vii.a) (ft / plSeql u [f / £]Seg2) n C7(tae) * 0 . Trivial ly, then, ([/ /plSeql u [/ / £j&?^2 u Wpl{-(r = s)})= [ilpl(Seqf u {-(r = «;)}) n C7(Jwe) * 0 . So U.IB$eq n C/(toe) * 0 . vii.b) ([£ / plSeql u [1 / £]Setf2) n C/(toe) = 0 . Since ([£ / u [t I p] {+[r I u]F}) n Cl(bse) * 0 and ([f / £]&?#2 u / p] {-[s I u]F}) n C/(foe) * 0 , it follows that [* / pi {+[r I u]F} n C/(foe) * 0 and [* /£l {-[s I u]F} n C/(toe) * 0 and hence that both +[t Ip][r I u]F = +[[t/plr/u][tlp]F, -[ilp\[s I u]F = -[[LIpis I u] tlp]F belong toCl(bse). B y definition 1.3.3., Cl(bse) = ^ Jbse^ , 0 <fj. < e0, so, since both of +[[t/plrl u\[i Ip]F, -[[A'pls I u\[il plF belong to Cl(bse), there are /3, y < e 0 such that +[[1 / £]r / u] [£ I plF e bsep and -[[£ I pis I u]UIPlF e bsey . Assume, without loss of generality, that y . Then bsey Qbsep and so both of +[[LIplrl u][ilplF, -[[Upis I u\[ilplF belong to bseB . There are two main 47 sub-subcases: vii.b.i) both of [£ I plr, \1I pis are basic terms. Then, since [t I plr, fi / p]s are constant terms, [tl plr, [tl pise B(Par). Then, by the contrapositive of lemma 1.3.8., since both of +[[tl plrl u\[tlplF, -[[if I pis I u][tlp_]F belong to bsep, the signed sentence +i[tl plr = [/j/£]s) does not belong to Clibse), thus, +([t/ plr = [{Ipis) £ bse. So, by condition 1) of definition 1.3.1., -{{tlplr= [t/pjs) = -\tlp\ir = s) e bse Q Clibse). Hence, [tlplSeq' u {-[tl pl(r = s)} = [Hpl(Seq' u {-(r = s)}) n Cl(bse) * 0 . So [t'p2Seq n Clibse) # 0 . vii.b.ii) not both of [IIplr, [1/pis are basic terms, i.e., at least one of [tl plr, [tlpis is a constant description term. Assume without loss of generality that [£ I pis is a constant description term ur.<P. Then there are two sub-sub-subcases: vii.b.ii. 1) [tIp]re8iPar), i.e., [1/plr is a basic term. Since -[ix.®l u][£lplF belongs to bsep , by lemma 1.3.10., there is a descriptum 8(Par) for ur.d>in bse such that -[t^^l u\[tl plF belongs to bsep. Since both of +[[tl plrl u][tlplF, -[t^^ I u][i/plF belong to bsep, by the same argument as that given in b.i) above, the signed sentence -([£ / plr = / t f $ ) belongs to bse Q Cl(bse). Now, since u occurs free in F, u occurs free in [tlplF. So, since both of +[[t I plr I u\[tl PlF, -[ix.®/ «][// plF belong to bsep, by lemma 2.O., for some constant term / and variable v, bsepQ Clibse) contains both of the signed sentences +[t I x\®, +(x)(v)((d> A [v I x]®)-*x = v). Then, by lemma 1.2.11, since all of -([t I plr = ), +[t I x]®, +(x)(v)((d> A [v / x]®) —> x = v) belong to Clibse) so does the signed sentence -([/ /p l r = ix.®) £ -([£/ Plr =[1/pis) £ -[t'pl(r = s). Hence, WiflSeq'U {-[tlplir = s)\ £ [tlpliSeq'KJ {-(r = s)}) n Clibse) * 0 . So [jf / plSeq n Clibse) * 0 . vii.b.ii.2) [t I plr g 8(/5ar), i.e., [t I plr is a constant description term, say iz. for some formula f . Since +[tz.f/ u\[tl plF belongs to bsep, by lemma 1.3.10., there is a descriptum ' u . f e &iPar) for \z.*F in bse such that +[t^l u\[tlp\F belongs to bsep. By the argument given in b.ii. 1) above, there is a descriptum t # e b"iPar) for ix. ® in bse such that -[/ * / 48 u\[LIu\F belongs to bsep. Since both of +[/u ^ / u][i/g]F, - [ /^^ / u][tlp]F belong to bsep , by the same argument as that given in vii.b.i) above, the signed sentence -(£ u ^ = t^ ^ ) belongs to bse Q Cl(bse). By the argument of vii.b.ii.l) above, it follows that -if^= ix.O) belongs to bse Q Clibse). So, since both of +[iz. f / «][£/j>]> -[vc.& / u][L/ g]F belong to bsep, by lemma 2.O., for some constant term t and variable v, bsepQ Cl(bse) contains both of the signed sentences +[t I zW, +(Z)(V)(("FA [V / z] f ) -> z = v). Then, by lemma 1.2.11, since all of -(t^ = ix.®), +[t I zW, +(z)(v)((fA [v / z]f) -> z = v) belong to Clibse) so does the signed sentence -(iz. f = ur.d>) s -([£/g]r = /JZ]S) = -\tln\(r = s). Hence, [j£ / U\Seq' u { - [ £ / ^ ] ( r = s)} = U./jt](Seq' u {-(r = s)}) n Clibse) * 0 . So n CT(foe) ?t 0 . viii) Ste^ is the conclusion of an application A of the cut rule 1.2.2.8.. Then, trivially by lemma 1.3.9., UtBHSeq n Cl(bse) * 0 . In all cases, then, [t / g]Seq n Clibse) * 0 . Hence, theorem 2.1. and the soundness of Pld is established. • . Corollary to Soundness ("Syntactic Consistency"): For no sentence snt are both of {+snt}, {-snt} derivable sequents. Proof: Assume there is a sentence snt such that both of [+snt], {-snt} are derivable. Let bse be any base, £ any n-axy vector on Par containing all of the parameters occurring in snt and t any n-axy vector on h(Par) and. By soundness theorem 2.1., both of {+snt}, {-snt} are valid, so by definitions 1.3.5. and 1.3.6., [tl£}{+snt} n Cl(bse) * 0 and U.In\{-snt} n Cl(bse) * 0 . So both of ±\i I B]snt belong to Clibse). Since Cl(bse) = KJbse^ ,0<fi<E0 , there are fi, y< < E Q such that +[//g]snt e bsepand -U.Iu\snt e bsey . Assume, without loss of generality, that p<y. Then bse^Qbsepand so both of ±[£In]sntbelong to bsep . This contradicts lemma 1.3.9.. • 49 Section 3: An Alternative Logical Syntax for Pld. For the purposes of the semantic completeness proof of section 4, we present a set of deductive rules which is equivalent to the set presented in 1.2.2.; section 4 establishes the semantic completeness of the new theory Pld2. The logical syntax of Pld2 is obtained from the set of deductive rules of 1.2.2. by replacing the three premise description rule 1.2.2.6., .6. Seql u {+[r / x]® } Seql u {+(x)(v)((® A [ V / x]®) -> x = v)} Seq3 u {±[t / u]F} Seql (j Seql u Seql u {±[ix.® / u]F} by the following two binary rules 1.2.2.6.+ and 1.2.2.6.-: .6.+. Seql u {+[*/ x](® A F)} Seql u {+(x)(v)((<P A [ V / x]®) -> x = v)} Seql u Seql u {+[ix.® I x\F } .6.-. Seql KJ {+[t Ix](® A —IF)} Seql u {+(x)(v)((CP A [ V /x]<P) -> x = v)} Seql u Seql u {-[ ix.® I x]F) A Pld2 derivation tree is defined in the obvious way. We say that a sequent Seq is 2-derivable iff it is the endsequent of a Pld2 derivation tree. We need to show that a sequent Seq is 2-derivable iff it is derivable. The claim that every derivable sequent is 2-derivable is trivial. However, the proof that Pld is semantically complete requires the converse claim, that every 2-derivable sequent is derivable, which we now establish. We first prove a couple of simple lemmata concerning the "old" notion of derivability: Lemma 3.1.: Let Seq be any sequent, A any sentence. If Seq u {H—A} is derivable, then so is Seq u {- A } . Proof of 3.1.: The proof of 3.1. is by induction on the depth B(U) of an arbitrary derivation tree 50 FI of Seq u {+—iA} in the manner of the proof of lemma 3.2. below. Lemma 3.2.: Let Seq be any sequent, A , B any sentences. If Seq u {+(A A B)} is derivable, then there are sequents Seql, Seql such that Seql u Seql = Seq and both of Seql u {+A}, Seql u {+B} are derivable. Proof of 3.2.: Assume that Seq u {+(A A B)} is derivable, say, as endsequent of a derivation tree II. We show by induction on the depth D(Tl) of FI that there are sequents Seql, Seql such that Seql u Seql = Seq and both of Seql u {+A}, Seql u (+B} are derivable. Clearly, we may omit the basis step, since by assumption IT contains nonatomic sentences and so is not an axiom. So assume the claim holds for all sequents which are derivable as endsequents of derivation trees £ such that D(L) < D(Yl). We show the claim holds for Seq u {+(A A B)} by case analysis. Since the proof is trivial and somewhat tedious, we consider only three cases: 1) Seq u {+(A A B)} = Seq' u {+(x)F , +(A A B)} is the conclusion of an application A in FI of the quantifier rule 1.2.2.5+. Then the premise to A is Seq' u {+[p I x\F , +(A A B)} where p is a parameter that does not occur in Seq u {+(A A B )} . Now, Seq' u {+[p I x]F , +(A A B)} is the endsequent of the deepest proper subtree X of IL Since D(L) < D(Yl), by the hypothesis of induction, there are Seq'l and Seql such that Seql u Seql = Seq' U [+[p I x]F) and both of Seq'l u {+A},Seq2 u {+B} are derivable. So {+[p /x]F] belongs to one of Seq'l, Seql. Without loss of generality, assume that {+[p I x]F}e Seq'l. There are two cases: i) [+\P 1 x]F)i Seq'l. Since p does not occur in Seq u {+(A A B)} = Seq' u {+(x)F , +(A A B)},p does not occur in (Seq'l- {+\p Ix]F}) u {+(x)F ,+A). So the following is a legitimate application of rule 1.2.2.5+.: (Seq'l- {+{p/x]F}) u {+[p/x]F , +A} (Seq'l- {+[p/x]F}) u [+(x)F , +A) Since Seq'l u {+A} = (Seq'l- {+{p /x]F}) u {+[p /x]F , +A} is derivable, it follows that 51 (Seq'l- [+[p /x]F}) u {+(x)F , +A} is derivable. Hence, both of {Seql- [+[p f x]F}) u { +(x)F , +A}, Seq'l u { + B } are derivable. Since Seq'l u &?^'2 £ S ^ ' u { +[/> / x]F } and {+[/>/x]F}g Seq'l, {Seq'l- {+[/>/x]F}) u {+(x)F} u Seql = Seq'KJ {+(X)F}. So, the claim holds. ii) {+[p / x]F}e Seq'l. Since p does not occur in u {+(A A B)},p does not occur in {Seq'l— [+\p I x]F}) KJ {+(X)F , + B } . S O the following is a legitimate application of rule 1.2.2.5+.: {Seql- {+[p/x]F}) u {+[p / x]F , + B } {Seql- {+[/>/x]F}) u [+{x)F , + B } Since Seq'l u { + B } = {Seq'l- {+\p / x]F}) u {+[p/ x]F , + B } is derivable, it follows that {Seql- {+[p I x]F}) u {+{x)F ,+B} is derivable. By case a), we know that {Seq'l- {+[p I x]F}) u {+(x)F , +A} is derivable. Since Seq'l u &e '^2 £ £<ef' u {+[p / x]F}, {Seq'l-{+[>/x]F})u {+(x)F} <u {Seq'l- {+[p/x]F})u {+(x)F} = Seq' u {+(x)F}. So the claim holds. QED CASE 1). 2) Stetf u {+(A A B ) } = Seq' u {+(C A D) , +(A A B ) } is the conclusion of an application A in FI of rule 1.2.2.3+., for some sentences C, D and sequent Seq'. Then A is of the following form: Seq'l u { +C } Seql u { + D } Seq'Kj {+(C A D ) ,+(A A B ) } where Seq'l u Seql = Seq' u {+(A A B ) } . There are three cases: i) {+(A A B ) } e Seq'l and {+(A A B ) } g Seq'l. Then Seq'l = {Seq'l - {+(A A B ) } ) U {+(A A B ) } . Since {Seq'l - {+(A A B ) } ) u {+(A A B ) , +C} is derivable as endsequent of a proper subtree of II, by the hypothesis of induction, there are SeqS and Seq4 so that SeqS u Seq4 = {Seq'l - {+(A A B ) } ) u {+C} and both of SeqS u {+A},Seq4 u { + B } are 5 2 derivable. Assume, without loss of generality, that +C e SeqS. There are two cases: a) +C e Seq4. The following is a legitimate application of 1.2.2.3.: (SeqS - {+C}) u {+C} u {+A} Seql u { + D } Seql u (SeqS - {+C}) u {+(C A D ) } U {+A} Since both of Seql u { + D } , S * ? f 5 u {+A} s (5*g3 - {+C}) u {+C} u {+A} are derivable, it follows that Seql u (Se^J - {+C}) u {+(C A D ) } U {+A} is derivable. Further, we know that Seq4 u { + B } is derivable. Now, since Seq'l u Seql = Seq'^J {+(A A B ) } and SeqS u Seq4 = (Seq'l - {+(A A B ) } ) u {+C}, it follows from the facts that {+(A A B ) } e= Seq'l and +C e Seq4 that Seq'l u (SeqS - {+C}) u (+(C A D ) } u Seq4 = Seq' u {+(C A D ) } . So the claim holds. b) +C G Seq4. The following is a legitimate application of 1.2.2.3.: (Seq4 - {+C}) u {+C} u { + B } fe?2u{+D) u (5ef^ - {+C}) u {+(C A D ) } u { + B } Since both of Seql u { + D } , S ^ 4 u { + B } £ - {+C}) u {+C} u { + B } are derivable, it follows that Seql u - {+C}) u {+(C A D ) } U ( + B } is derivable. Further, by case a) we know that Seq'l u (SeqS - {+C}) u {+(C A D ) } U {+A} is derivable. Now, since Seq'l u Seq'l = Seq'u {+(A A B ) } and SeqS u Seq4 = (Ste^'l -{+(A A B ) } ) u {+C}, it follows from the fact that {+(A A B ) } g Seq'l that 5"e^ 2 u (Seq4 - {+C})u {+(C A D ) } U Seq'l u (SeqS - {+C}) u {+(C A D ) } = Seq' u {+(C A D ) } . So the claim holds. ii) {+(A A B ) } € Seq'l and {+(A A B ) } e Seql. This case is similar to case i) above. iii) (+(A A B ) } e Seq'l and {+(A A B ) } e Seq'l. Then, by similar argument to case i), there are SeqS and Seq4 so that SeqS u Seq4 = (Seq'l - {+(A A B ) } ) U {+C} and both of SeqS u {+A}, Seq4 u { + B } are derivable and there are SeqS and Seq6 so that SeqS u 53 Seq6 = (Seq'l - {+(A A B ) } ) u {+D} and both of SeqS u {+A},Seq6<u {+B} are derivable. The following is a legitimate application of 1.2.2.3.: (SeqS - {+C}) u {+A , +C} (SeqS - {+D}) u {+A , +D} (SeqS - {+C}) u (SeqS - {+D}) u {+(C A D) , +A} In case +C e SeqS, SeqS u {+A} £ (&$3 - {+C}) u {+A , +C}. In case +C e SeqS, since 5e^3 u {+A} is derivable, (SeqS - {+C}) u {+A , +C} is derivable by an application of thinning. So in both cases, (SeqS - {+C}) U {+A , +C} is derivable. By similar reasoning, {SeqS - {+D} u {+A , +D} is derivable. Hence, (SeqS - {+C}) u (SeqS - { + D } ) u (+(C A D) , +A} is derivable. A similar argument establishes that (Seq4 - {+C}) u (Seq6 -{+D}) u {+(C A D) , +B} is derivable also. Since SeqS u Seq4 = (Seq'l - (+(A A B )} ) u {+C} and SeqS u Seq6 = (Seq7 - [+(A A B ) ) ) U {+D} , it follows from the fact that Seq'l u Seq'l = Seq' u {+(A A B)} that (SeqS - {+C}) u (SeqS - { + D } ) u {+(C A D)} u (Seq4 - {+C}) u (SeqS - { + D } ) u {+(C A D)} = Seq' u {+(C A D ) } . S O the claim holds. QED CASE 2). 3) Seq u {+(A A B ) } = Seq' u [±[ix.® I u]F , +(A A B ) } is the conclusion of an application A in IT of rule 1.2.2.6., for some description term ix.<& and formula F. Then A is respectively of the following form: Seql u [+[t/x]®} Seql u {+(x)(v)((® A [v /x]®) x = v)} SeqS u {±[t/u]F} Seq'Kj {±[uc.<P/a]F , +(A A B)} where Seql yj Seql SeqS = Seq' <u {+(A A B )} . There are four main cases: i) +(A A B ) G Seql and +(A A B ) e Seql u SeqS. Then, since Seql u {+[// x]d>} = (Seql - {+(A A B ) } ) u {+(A A B ) , +[t/ x]<P] is derivable as the endsequent of a proper subtree of IT, by the hypothesis of induction, there are Seq4, SeqS such that Seq4 u SeqS = (Seql - [+(A A B )} ) u {+[t/x]®} and both of Seq4 u {+A},SeqS u {+B} are derivable. 54 Assume without loss of generality that +[t I x]d>e Seq4. There are two cases: a) +[t I x]0 £ SeqS. The following is a legitimate application of 1.2.2.6.: (Seq4 - {+[f/*]<£}) u {+A , +[t/ x]&) Seql u [+(x)(v)((® A [V / X]®) -> x = v)} Seq3 u [±[t/u]F] (Seq4 - { + [tI x]0}) u Seql u SeqS u [±[ix.® / u]F ,+A) Since all of Seq4 u { +A } = (Seq4 - [+[t / x]0}) u { + A , +[//x]<2>}, Seql u {+(x)(v)((<P A [v / x]d>) -> x = v)}, SeqS u {±[f / M ] F } are derivable, it follows that (Seq4 -{+[ / / x]<P}) u Se«?2 u Seg3 u {±[u\<?> / u ] F , +A} is derivable. So both of (Seq4 -{+[t I x] O}) u Seql u S ^ J u {± [ix. <2> / M ] F , +A}, SeqS u { + B } are derivable. Now, since Seql u S«^2 u Segi £ Seq' u {+(A A B ) } and Seq4 u Se^5 £ (Se^l - {+(A A B ) } ) ^ {+[tl x]0], it follows by the facts that +(A A B ) € Seql u SeqS and +[t/ x]0 € SeqS that (Seq4 - {+[f / x]0)) u 5e*y2 u SeqS u {±[ix.<2> / M ] F } u 5e«5 s 5e*f' u {±[xx.0/u]F). S O the claim holds. b) +[t/x]0<= SeqS. Then SeqS u { + B } s (Ste$J - {+[//*]<£}) u {+[f/x]<3> , + B } . The following is a legitimate application of 1.2.2.6.: (SeqS - [+[tIx]®}) u {+B , +[t / x]&) Seql u {+(x)(v)((* A [V /X]<P) -> x = v)} Setfi u (±[// H]/?} (S«?5 - [ + [t / x]&)) KJ Seql v Seq3 u {±[uc.«£/u]F ,+B} Since all of SeqS u { + B } = (SeqS - {+[// x]0}) u { + B ,+[//x]<J>},Se$2 u {+(x)(v)((0 A [v / x]<2>) -> x = v)} , Se^J u {±[t I u]F}, are derivable, it follows that (SeqS - {+[t/ x]0}) u Seql u S«^5 u {±[u\<£ / « ] F , + B } is derivable. But by case a), we know that (Seq4 - {+[t I x]0)) u Seql u u {±[ix.«3> / w ] F , +A} is also derivable. Now, since Seql u Seql u SeqS = Seq'u {+(A A B ) } and Seq4 u SeqS = (Seql - {+(A A B ) } ) U {+[t/ x]0], it follows by the fact that +(A A B ) e Se^2 u Se^J that (SeqS - {+[f/x]d>}) u Se#2 u SeqS u {±[ix.tf> / u]F} u ( S * ^ - {+[f / x]<£}) u Se#2 u Seg3 u {±[ix.tf> / u]F , +A} = Seq' u {±[ix.01 u]F}. So the claim holds. 55 ii) +(A A B ) e Seql and +(A A B ) e Seql and +(A A B ) eSeqS. By case i), there are Seq4, SeqS such that Seq4 u SeqS = (Seql - {+(A A B ) ) ) U { + [ / / X ] < P } and both of Seq4 u {+A}, SeqS u {+B} are derivable. By a similar argunent, since +(A A B) G Seql, we know that there are Seq6, Seq7 such that Seq6 u Seq7 = (Seql - {+(A A B ) } ) u {+(x)(v)((® A [v /x]<P) -> x = v)} and both of Seq6 u {+A},5e#7 u {+B} are derivable. Let Seq6* = (5e$tf - {+(x)(v)((CP A [ V / x]®) -> x = v)}) U {+(x)(v)((<P A [v/x]d>) -> x = v)}. The following is a legitimate application of 1.2.2.6.: (S««4 - {+[//*]<£}) u {+A , +[t/x]<P] Seq6* u {+A} Seq3 u {±[f/ - {+[tlx]0}) u - {+0c)(v)((ef>A [v/*]<*>) -» x= v)} )vSeq3 u {±[ur.d>/«]F , +A} In case +[//x]d>G Seq4,Seq4 u {+A} £ - {+[//x]<2>}) u {+A ,+[f/x]d>}; in case +[r/x]<P£ Se?4, (Seq4 - [+[t /x]®}) u {+A /x]d>} is derivable from Seq4 u {+A} by an application of thinning. In both cases, then, (Seq4 - {+[t /x]d>}) u {+A ,+[/ /x]®} is derivable. A similar argument establishes that SeqS* u {+A} is derivable. Since SeqS u {±[/ / u]F] is derivable, it follows that (Seq4 - {+[t /x]®}) KJ (Seq6 - {+(x)(v)((® A [ V /X]®) —> x = v)}) u SeqS u {±[ ix.® I u]F , +A} is derivable. A similar argument establishes that (SeqS - {+[tI x]®}) u (Seq7 - {+(x)(v)((® A [ V / x]®) -> x = v )} ) u SeqS u {±[ ix.® I u]F , +B} is derivable as well. Now, since Seql u Seql KjSeqS = Seq' u {+(A A B)} and Seq4 u SeqS £ (Seql - {+(A A B ) } ) U {+[*/ x]<2>} and Se e^f u Seq7 = (Seql - {+(A A B ) } ) u {+(x)(v)((® A [v / x] ®) -> x = v)}, it follows by the fact that +(A A B) G Ste^i that - {+[t/ x]®}) u - {+(x)(v)((d> A [v/x]0) -> x = v)}) u Se^J u {±[tx.<2> / u]F] u (Se^5 - / x]d>}) u (Se^7 - {+(x)(v)((<P A [ V / x]®) -> x = v )}) u SeqS u {±[ IX.<2>/M]F} S Se^'u {±[ix.CP/M]F}. S O the claim holds. iii) +(A A B ) e Seql and +(A A B) e Seql and +(A A B) G SeqS. This case is similar to case ii) above. iv) +(A A B ) e Seql and +(A A B) G Seql and +(A A B ) eSeqS. This case is similar to case ii) above. QED CASE 3). 56 This completes our case analysis. By the principle of induction, lemma 3.2. is established. • We may now establish the desired result that every 2-derivable sequent is derivable: Lemma 3.3.: Let Seq be any sequent. If Seq is 2-derivable, then Seq is derivable. Proof of 3.3.: Assume that Seq is 2-derivable, say, as endsequent of a Pld2 derivation tree IT. We show by induction on the depth D(Yl) of Tl that Seq is derivable. Base step: D(Tl) = 0, i.e., Tl is an axiom. Then i i is derivable. Induction step: Assume derivable every sequent that is 2-derivable as endsequent of a Pld2 derivation tree £ such that D(Z) < B>(Tl). Clearly, if Seq is the conclusion of an application of one of .1.2.2.1.+, 1.2.2.2.1, 1.2.2.3.1, 1.2.2.4.1, 1.2.2.5.1, 1.2.2.7.1, 1.2.2.8.1, then by the hypothesis of induction, Seq is derivable. So assume that Seq is the conclusion of an application A of either 1.2.2.6.+ or 1.2.2.6.-. We consider these two cases: i) Seq is the conclusion of an application A in II of 1.2.2.6.+. Then, Seq = Seql u Seql u [+[xx.® I x]F) for some sequents Seql, Seql, term t, formula F, and description term ix.® and A is of the following form: Seql u {+[//x](® A F)} Seql u {+(x)(v)((<P A [ V /x\®) -> x = v)} Seql u Seql u {+[ur.®/x]F} Since Seql u {+[// x](® A F)} and Seql u {+(x)(v)((® A [ V / x]®) -> x = v)} are 2-derivable as endsequents of proper subtrees of IT, by the hypothesis of induction, both of Seql u {+[t/ x](® A F)}, Seql u {+(x)(v)((® A [V I x\®) -> x = v)} are derivable. Since Seql u [+[t/x](®A F)} £ Seql u {+([*/x]® A [t/x]F)} is derivable, by lemma 3.2., there are sequents Seq3, Seq4 such that SeqS u Seq4 = Seql and both of SeqS u {+[// x]®}, Seq4 {+[t I x]F] are derivable. The following is a legitimate application of 1.2.2.6.: 57 SeqS u {+[t I x ]0 } Seq2 u {+(x)(v)((«3> A [ V / x]0) -> x = v)} Seq4 u {+[t I x]F} SeqS u Seql u Seq4 u {+[ix. <2> / x]F} So it follows that SeqS u S<e#2 u Seq4 u {+[tx.d> / x ] F} = Seql u S«^2 u {+[ix.d> / x]F} = Seq is derivable. So the claim holds. ii) Seq is the conclusion of an application A in IT of 1.2.2.6.-. Then, Seq = Seql u Seql u {-[tx.d>/x]F} for some sequents Seql, Seql, term /, formula F, and description term ix.0 and A is of the following form: Seql u [+[t I x](0 A -iF)} &?f2 u {+(x)(v)((4> A [ V / x]d>) -» x = v)} Seql U Seql u {-[ix.CP/x]F} Since Seql KJ { +[t I x](d> A - , F )} and,5^2 u {+(x)(v)((d> A [ V / x]<2>) -» x = v)} are 2-derivable as endsequents of proper subtrees of II, by the hypothesis of induction, both of Seql u {+[t/ X](0A -iF)}, Seql u {+(x)(v)((<£ A [v/x]d>) -> x = v)} are derivable. Since Seql u { + [ / / X ](< P A - T F ) } = £e«yl u {+([t/X)0A [ / / X ] - , F ) } is derivable, by lemma 3.2., there are sequents Seq3,Seq4 such that Se^J u Seq4 = Seql and both of SeqS u {+([// x]d>},Se^ u {+([*/x]-.F)} are derivable. Since Seq4 u {+([*/x]-iF)} is derivable, by lemma 3.1., Seq4 u {-([f / x ]F )} is derivable. The following is a legitimate application of 1.2.2.6.: SeqS u {+[tI x]0 } Seql u {+(x)(v)((d> A [v /x]d>) x = v)} Seq4 u {-[/ / x ] F } SeqS u 5 ^ 2 u Seq4 u {-[ix.CP / x]F} So it follows that SeqS KJ Seql u Seg^ u {- [ix. 01 x ]F } = Seql u £ ^ 2 u {-[tx. <P / x]F } = Ste<? is derivable. So the claim holds. In both cases, Seq is derivable. So by the principle of induction, lemma 3.3. is established. • 58 3.4.: A derivation tree II is a strict derivation tree iff II contains no applications of the cut rule 1.2.2.8.± and no applications A of the description rule 1.2.2.6. such that A has a nonelementary output sentence. A sequent Seq is strictly derivable iff it is derivable as endsequent of a strict derivation tree. A Pld2 derivation tree IT is a strict Pld2 derivation tree iff n contains no applications of the cut rule 1.2.2.8.± and no applications A of either of the description rules 1.2.2.6.+, 1.2.2.6.-, such that A has a nonelementary output sentence. A sequent Seq is strictly 2-derivable iff it is 2-derivable as endsequent of a strict Pld2 derivation tree. Lemma 3.5.: Let Seq be any sequent. If Seq is strictly 2-derivable, then Seq is strictly derivable. Proof of 3.5.: The proof of lemma 3.5. is obtained from the proof of lemma 3.3. by uniformly substituting the expression "strict derivation tree" for "derivation tree", "strict Pld2 derivation tree" for "Pld2 derivation tree", "strictly derivable" for "derivable", "strictly 2-derivable" for "2-derivable", and "afm" for "F" throughout that proof. This concludes section 3. We are now prepared to establish the semantic completeness of Pld by establishing the semantic completeness of Pld2. 59 Section 4: Semantic Completeness for Pld. We say that Pld is semantically complete iff every valid sequent is derivable. In this section we show that Pld is semantically complete. 4.1 Preliminaries. For the purposes of the completeness proof, we generalize the notion of 2-derivability (strict 2-derivability) defined in section 3 so that we may consider the 2-derivability (strict 2-derivability) of arbitrary sets of signed sentences. A possibly infinite set Set of signed sentences is said to be 2-derivable (strictly 2-derivable) iff there is a sequent Seq Q Set such that Seq is 2-derivable (strictly 2-derivable). In other words, a set of signed sentences is 2-derivable (strictly 2-derivable) iff some finite subset of it is 2-derivable (strictly 2-derivable). Observe that a sequent is 2-derivable (strictly 2-derivable) in the extended sense defined here iff it is 2-derivable (stricdy 2-derivable) in the sense of section 3. Let bijective numerations P: IN -> Par, T: IN -» 8(Par), SS: IN -» {±snt: snt e E(Par)}, of the set of respectively parameters, constant basic terms, signed sentences, of Pld be given. Let led: {±snt: snt e T^Par)} —> IN be the functional inverse of SS, i.e., Ind(SS(/)) = /; i will be called the index of the signed sentence SS(i'). If Set is a set of signed sentences, let ^ (Set) be the set of parameters which occur in at least one member of Set. Then, .1. Let Set be a set of signed sentences and ±snt any member of Set. Then, Set is downward closed iff the following conditions hold: 1) For no atomic sentence asnt does Set contain both of tasnt. 2) For no / in b(Par) does Set contain the signed sentence +(r = /) 3) For no r, s in d(Par) does Set contain both of +(r = s), -(s = r). 60 4) For no r, s in 5(P<zr) and atomic formula afm does Set contain all of -(r = s), -[rl v]afm, +[s I v]afm. 5) If ±snt is respectively of the form ±-iA for some sentence A, then Set contains respectively +A. 6) If ±snt is respectively of the form ±(A A B) for some sentences A, B, then Set contains one of +A, +B, respectively, both of -A, -B. 7) If ±snt is respectively of the form ±(A —> B) for some sentences A , B, then Set contains both of -A, +B, respectively, one of +A, -B. 8) If ±snt is respectively of the form ±(x)F for some formula F, then Set contains +[p I x]F for some p in ^(Set), respectively, -[/ / x]F for every/in 5(SP(Sef)). 9) If ±snt is a signed nonatomic elementary sentence of the form +[xx.0 lu\afm for some constant description term xx.0 and atomic formula afm, then Set satisfies one of the following conditions: i) Set contains the signed sentence +(x)(v)((& A [ V / x]&) —> x = v) for some variable v. ii) Set contains the signed sentence +[/ / x](& A [X I u]afm) for every t e ^(^(Set)). 10) If ±snt is a signed nonatomic elementary sentence of the form -[xx.0lu\afm for some constant description term xx.0 and atomic formula afm, then Set satisfies one of the following conditions: i) Set contains the signed sentence +(x)(v)((0 A [ V / x]0) — » x = v) for some variable v*x. ii) Set contains the signed sentence +[t I x\(0 A —i[x/ u]afm) for every f e ^(^(Set)). 4.2. Statement and Proof of the Completeness Theorem. Theorem 4.2.1.: Let Seq be a sequent of signed sentences. If Seq is valid, then Seq is derivable. 61 We establish 4.2.1. by proving the much stronger result that if Seq is valid then Seq is stricdy derivable. This stronger result follows by lemma 3.5. from the following theorem, which we now prove: Theorem 4.2.2: Let Seq be any sequent. If Seq is valid then Seq is strictly 2-derivable. Proof of 4.2.2.: We will show that any sequent that is not strictly 2-derivable is not valid, that is, is invalidated by some base, by establishing the following two lemmata: Lemma 4.2.3.: Let Seq be any sequent. If Seq is not strictly 2-derivable, then Seq has a downward closed extension Set^. Lemma 4.2.4.: Every downward closed set Set of signed sentences determines a base bseSet such that Set n Cl(bseSet) = 0 . Note that the significance of the notion of downward closed is revealed by lemmas 4.2.3. and 4.2.4.: every downward closed sequent is invalidated by some base. Clearly, our desired result that any sequent which is not strictly 2-derivable is invalidated by some base is an immediate consequence of lemmas 4.2.3. and 4.2.4.. Proof of 4.2.3.: We establish lemma 4.2.3. by defining a process which constructs downward closed extensions for arbitrary sequents which are not stricdy 2-derivable. We say that a signed sentence ±snt is reducible iff snt is neither elementary nor, for some formula F, of the form (x)F. Let S 5= INI and Set be a set of signed sentences. Let ±snt be a signed nonatomic sentence in Set such that Ind(±snt) e S and for all j < i, if j e S, then SS(/) &Set. In other words, let ±snt be the first signed nonatomic sentence in Set whose index is not in S. Then Set' is said to be an S-reduction of Set iff ±snt is reducible and Set' is obtained from Set by adding new signed sentences to Set' according to the following rules: 1) If ±snt is respectively of the form ± - A for some sentence A, then respectively +A is added to Set; 62 2) If +snt is of the form +(A A B) for some sentences A, B, then one of +A, +B is added to Set; 3) If ±snt is of the form -(A A B) for some sentences A, B, then both of -A, -B are added to Set; 4) If ±snt is of the form +(A —» B) for some sentences A, B, then both of -A, +B are added to Set; 5) If ±snt is of the form -(A —> B) for some sentences A, B, then one of +A, -B is added to Set.; 4.2.3.1: A reduction sequence (Set;) of a sequent Seq with respect to an enumeration SS is a sequence of sets Set;Of signed sentences defined by simultaneous recursion with sequences (S-), (Dl,-) of index sets S-, D l - as follows: Let ±snt;be the first signed nonatomic sentence in Set; whose index is not in S •. Let R(i) Q S • be the set of indices in S • of signed sentences ssnt such that ssnt is either of the form -(x)F for some formula F or of the form ±[xx.®/ u]afm for some description term u:. CP and atomic formula afm. Then, 0) Set0 = Seq. S0 = 0. D l - = 0 . 1) If ±snt; is reducible, then Seti+1 is a S; -reduction of Set;. Si+1 = S-u [lnd(±snt;)}. D1- + 7 = D1-. 2) If ±snt; is of the form +(x)F for some formula F, then Seti+1 is obtained from Set; by adding to Set; the new signed sentence +[p I x]F, where p is the first parameter that does not occur in any signed sentence of Set;. In other words, Seti+1 = Set; u {+\p I x]F}. Si+J = (S; u {Ind(±sfi4)}) - R(i). D1 i + ] = D1 -. 3) If ±snt; is of the form -(x)F for some formula F, then Seti+1 is obtained from Set; by adding to Set; all signed sentences of the form -[/ / x]F, where t is in ^ (^(Set;)). In other words, Seti+1 =Set;(J {+[t/x]F : f e 8(^(Set;))}. Si+] = S,-u {lnd(±snt;)}. Dli+1 = D1-. 4) If ±snt is a signed nonatomic elementary sentence of the form +[\x.® / u]afm for some description term ur.CP and atomic formula afm, then Seti+1, Si+1, D l i + 7 are obtained from Set;, S;, Dl; by one of the following rules: 63 a) If IndCisn/j) g DI,., then Seti+1 is obtained from Setfiy adding to Set; the new signed sentence +(x)(v)((d> A [ V / x]<P) -> x = v) for some variable v * x. In other words, Seti+1 = Setk u {+(x)(v)((<P A [v /x]d>) -> x = v)}. Si+1 = S ( u {indClsii/,.)}. D l f + y = DI,.. b) Sef l+y is obtained from Seti by adding to Stef; all signed sentences of the form +[/ / x](<P A [ X / u]afm), where t e 809s(Sef,-)). In other words, S«f i + y = Stef,- u {+[/ / x](d> A [x / H]fl/ffl):<e8(^(S^))}. Si+] = S ,u {lnd(±«if.)}. D l l + y = D l , . u {lnd(±«!/,.)}. 5) If ±snt is a signed nonatomic elementary sentence of the form -[ix.d> / u]afm for some description term \x.& and atomic formula afm, then Seti+I , Si+1 , D l i + y are obtained from Set;, Si, Dli by one of the following rules: a) If Ind(±s/ir;) £ DI; then Seti+1 is obtained from Set [by adding to Seti the signed sentence +(x)(v)((d> A [v / x] 0) —7 x — v) for some variable v*x. In other words, Seti+l = Seti u (+WW((d>A[v/x]d>)-»x = v)}. S. + y = S,.u {IndClsnf,.)}. D l ; + y = D l t . . b) Sef^y is obtained from Set;by adding to Seft- all signed sentences of the form +[t I x](<2> A -.[x / u]afm), where * e 8($s(Set;)). In other words, Seti+1 = Set; u {+[// x](d> A - I [ X / u]afm): t e 8(^(5«r,-))}. S / + y = S - u {lnd(±sn )^J. D l i + y = D l , u {Imd(± snf.)}. 6) If there is no such signed sentence ±snti, that is, if Seti contains no signed nonatomic sentence whose index is not in St-, then Seti+1 = Seti. Si+I = S;. D l f + y = D l ; . Observe that definition 4.2.3.1. is well-defined in the sense that the "new" parameter p required by clause 2) will always exist, since for all i, ^(Set^) is finite, as we now show: Since Seq is a finite set of signed sentences, ^°(Set0) is finite. If (Set;) is finite, so is &*(Seti+]), since the only clause of 4.2.3.1. which adds new parameters to any S°(Set;) (i.e., 2) adds only finitely many such parameters (just one, in fact). We observe that 4.2.3.1. is well-defined also in the sense that clauses 1) - 6) inclusive of that definition are mutually exclusive as well as collectively exhaustive. It is important to note that rules a), b) of clauses 4) and 5) of 4.2.3.1. are not to be thought of as mutually exclusive and exhaustive and therefore determinate subcases of 4). Rather, they are alternative possible ways in which a Seti+1 may be obtained from Seti in a reduction sequence (Set;). 64 We will see that for arbitrary sequents Seq that are not strictly 2-derivable there exists an infinite reduction sequence (Set;) the union set of which proves to be the downward closed extension of Seq whose existence is claimed in lemma 4.2.3.. The significant observation here is that any reduction sequence (Set) has the property that for each Set; in (Set}}, if Set; is valid in a base bse with domain 5(^(Set;)), then Seti+] is valid in bse. Hence, if a base bse invalidates any Set ;in any reduction sequent (Set}) of a sequent Seq, it follows by induction that bse invalidates Seq. Indeed, the claim that the union set of a reduction sequent (Set;) is downward closed implies that (Set) has the property observed above and that there are Set; in (Set) and bse such that bse invalidates Set;. Lemma 4.2.3.2: Let Seq be any sequent. If Seq is not strictly 2-derivable, then Seq has an infinite reduction sequence (Set) such that no Set; in (Set) is strictly 2-derivable. Proof of 4.2.3.2.: Assume Seq is not strictly 2-derivable. We show by induction on / that for every i, there is a Set; such that Set; is not strictly 2-derivable. Base step: i = 0. By assumption Set0 - Seq is not strictly 2-derivable. Induction step: i > 0. Assume Set; is not strictly 2-derivable. We show that there is a Set; j which is not stricdy 2-derivable by exhaustive case analysis. There are two main cases: 1) There is no signed nonatomic sentence ±snt; such that ±snt; e Set; and Md(±snt) <& S,-. In this case, by clause 6) of definition 4.2.3.1., Seti+1 = Set;. By the hypothesis of induction, Seti+I is not strictly 2-derivable, so the claim holds. 2) There is a signed nonatomic sentence ±snt; such that ±snt;G Set;&n& lnd(±snt) g S(-. There are nine subcases: i) ±snt; is respectively of the form ±—iA for some sentence A . Then by clause 1) of 4.2.3.1. Seti+1 exists and is a S-reduction of Set- of type 1). In this case, Seti+1 = Set; u { + A } , respectively. We show that if Seti+] is strictly 2-derivable, then so is Set;, from which it follows 65 by the hypothesis of induction that Seti+] is not strictly 2-derivable. Assume that Seti+] is strictly 2-derivable. Then some finite subset Seq' of Seti+1 is strictly 2-derivable. In case Seq' Q Set;, Set;is strictly 2-derivable by virtue of its strictly 2-derivable finite subset Seq'. In case Seq'<£ Set;, respectively +A e Seq'. The following is a legitimate application of rule 1.2.2.2..: (Seq' - {+A}) U {+A} (Seq' - {+A}) u { ± - i A } So, since Seq'= (Seq' - {+A}) u {+A} is strictly 2-derivable, so is (Seq' - {+A}) u {±->A}. Since Seq' c Seti+1 = Set; u {+ A } , (Seq' - {+A}) u {±-iA} c Set; u {±-.A} = Set;. Since Ster-has a finite subset (Seq' - {±A}) u {±—iA} which is strictly 2-derivable, Set; is stricdy 2-derivable. So the claim holds. ii) ±snt; is of the form +(A A B) for some sentences A, B. In this case (since +(A A B) G Set), Set; = Set; u {+(A A B)}. Then by clause 1) of 4.2.3.1., two Seti+l exist as St-reductions of Set; of type 2): Set; u {+A } and Set; u {+B}. We show that if both Seti+1 are strictly 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that at least one of the Seti+J is not strictly 2-derivable. So assume that both of Set; u {+A}, Set; u {+B} are strictly 2-derivable. Then there are finite Seql ?= Set; u {+A}, Seql Q Set; u {+B} such that both of Seql, Seql are strictly 2-derivable. In case either of Seql, Seql are subsets of Set; , then clearly Set; has a finite subset which is strictly 2-derivable, and so is strictly 2-derivable. So assume neither of Seql, Seql are subsets of Set;. Then +A eSeql and +B eSeql. The following is a legitimate application of rule 1.2.2.3.+.: (Seql - {+A}) u {+A} (Seql - {+B}) u {+B} (Seql - {+A}) u (Seql - {+B}) u {+(A A B)} Since both of Seql = (Seql - {+A}) u [+A},Seql = (Seql - {+B}) u {+B} are strictly 2-derivable, it follows that (Seql - {+-A}) u (Seql - {+B}) u {+(A A B)} is strictly 66 2-derivable. Now, since Seql Q Set; u {+A} and Seql Q Set; u {+B}, it follows that (Seql - {+A}) u (Seql - {+B}) u {+(A A B)} C Set;u {+(A A B)} = Set;. Since Set; has a strictly 2-derivable finite subset (Seql - {+A}) u (Seql - {+B}) u {+(A A B)}, Set; is strictly 2-derivable. So the claim holds. iii) ±snt; is of the form -(A A B) for some sentences A, B. Then, by clause 1) of 4.2.3.1., Seti+I exists and is an S-reduction of Set; of type 3). In this case, Set; = Set; u {-(A A B)} and Seti+1 = Set; u {-A , -B}. We show that if Seti+1 is stricdy 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that Seti+1 is not strictly 2-derivable. So assume that Set; u {-A, -B}, is strictly 2-derivable. Then there is finite Seq' Q Set; u {-A , -B} such that Seq' is strictly 2-derivable. In case Seq' ^ Set;, Set; is strictly 2-derivable by virtue of its strictly 2-derivable finite subset Seq'. In case Seq' $ Set;, one of -A, -B e Set;. Without loss of generality, assume that -A e Set;. There are two cases: a) -B e Seq'. Then Seq's (Seq' - {-A , -B}) u {-A , -B}. Consider the following legitimate application of rule 1.2.2.3.-: (Seq'- { - A , - B } ) u {-A,-B} (Seq' - {-A , -B}) u {-(A A B)} Since (Seq' - {-A , - B } ) u {- A , -B} = Seq' is strictly 2-derivable, it follows that (Seq' -{-A , -B}) u {-(A A B)} is stricdy 2-derivable. b) -B e Seq'. Then Seq' = (Seq' - {-A , -B}) u {-A}. The the following is a legitimate application of the thinning rule followed by a legitimate application of rule 1.2.2.3.-: { - A , - B } ) u {-A} (Seq' - {-A , -B}) U {-A , - B } (Seq' - {-A , -B }) u {-(A A B)} 67 Since (Seq'- {-A , -B}) u {-A} = Seq' is strictly 2-derivable, it follows that (Seq' - {-A , -B}) u {-(A A B)} is strictly 2-derivable. In both cases, then, (Seq' - {-A , -B}) u {-(A A B)} is strictly 2-derivable. Since Seq' ^ Seti+] = Set; u {-A , -B}, it follows that (Seq' - {-A , - B}) u {-(A A B)} c Set; u {-(A A B)} =Set;. Hence, Set ;has a strictly 2-derivable finite subset and so Set ;is strictly 2-derivable. So the claim holds. iv) ±snt; is the form +(A —> B) for some sentences A, B. This case is similar to subcase iii). v) ±snt; is of the form -(A —> B) for some sentences A, B. This case is similar to subcase ii). vi) ±snt; is of the form +(x)F for some formula F. In this case, Set; = Set; u {+(x)F}. Then, by clause 2) of 4.2.3.1., Seti+l exists and Seqi+I = Set;U {+[p Ix]F} where p is the first parameter that does not occur in any member of Set;. We show that if Seti+J is strictly 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that Seti+] is not strictly 2-derivable. So assume that Seqi+1 = Set;(J {+[p I x]F) is strictly 2-derivable. Then there is finite Seq' Q Set; u {+{p I x]F] such that Seq' is strictly 2-derivable. In case Seq' Q Set; , Set;is strictly 2-derivable by virtue of its strictly 2-derivable finite subset Seq'. In case Seq'<£ Set;, +[p I x]F e Seq'. Since p does not occur in any member of Set;, the following is a legitimate application of rule 1.2.2.5.+: (Seq' - {+\p/x]F}) u {+{p /x]F} (Seq' - {+[p I x]F }) u {+(x)F} Since Seq' = (Seq' - {+[p Ix]F}) u {+[>/ x]F] is strictly 2-derivable, it follows that (Seq' - {+lP I x]F }) u {+(x)F} is strictly 2-derivable. Since Seq' Q Seqi+1 = Set;u {+[p I x]F), it follows that (Seq' - {+[p /x]F }) u [+(x)F] Q Set;Vj {+(x)F} = Set;. Hence, Set; has a strictly 2-derivable finite subset and so Set; is strictly 2-derivable. vii) ±snt; is of the form -(x)F for some fomula F. In this case, Set- = Set; u {-(x)F). Then, 68 by clause 3) of 4.2.3.1., Seti+1 exists and Seqi+1 = Set;U {-[t/ x]F :te b(^°(Set;))}. We show that if Seti+1 is strictly 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that Seti+1 is not strictly 2-derivable. So assume that Seqi+1 = Set; u [-[t I x]F : t e biS3(Set;))} is strictly 2-derivable. Then there is finite Seq' Q Set;Kj {-[t I x]F : t <= ^(^(Set;))} such that Seq' is strictly 2-derivable. In case Seq' Q Set; ,Set;is strictly 2-derivable by virtue of its strictly 2-derivable finite subset Seq'. In case Seq' $ Set; there is a nonempty finite set {-[/, / x]F , . . . , -[tn/x]F} ^{-[t/x]F :te b(^(Set;))} such that {-[tj/x]F, . . . , - [*„ /x ]F} QSeq' where the / x]F , . . .,-[/„/ x]F are all the signed sentences in {-[/ / x]F : t e ^(^(Set;))} which are members of Seq'. The following is a finite sequence of legitimate applications of rule 1.2.2.5.-: (Seq'-i-Vj/xW , • . .,-[t„/x]F}) u {-[tj/xW, . • - ,-[tn/x]F} (Seq' - {-[tj 1 x]F , . . . .,-[tn/x]F}) u {-[t2/x]F, . . .,-[tn/x]F} u {-(x)F} (Seq' - {-[tj/x]F , . . • .,-[tn/x]F}) v {-[t3/x]F , . • .,-[tn/x]F} u {-(x)F} (Seq'- {-[tj / x]F , . . . , -[/„ / x]F}) u { -[tn I x]F} u -(x)F} ( W " { - [ ^ / x ] F , . . . , - [ r „ / x ] F } ) u {-(x)F} Since Se^' = (Se^p - {-[^ / x]F , . . . , -[tn I x]F}) u {-[tj I x]F , . . . , / x]F} is strictly 2-derivable, it follows that (Seq' - {-[tj / x]F , . . . , -[tnl x]F}) u {-(x)F} is strictly 2-derivable. Since Seq' Q Seqi+1 = Set; u {-[r /x]F : r e 8(^(5^.))} and the -[tj I x]F , . . . , -[tnlx]F are a// the signed sentences in {-[t/x]F : te 8(^(Set;))} which are members of Seq' it follows that (Seq' - {-[t11 x]F , . . . , - [ / „ / x ]F} ) u {-(x)F} c 5^. u {+(x)F} £ S^r,-. Hence, Set; has a stricdy 2-derivable finite subset and so Set; is strictly 2-derivable. So the claim holds. viii) ±snt; is a signed elementary sentence of the form +[ix.d>/ u]afm for some description term ix. <P and atomic formula afm. In this case, Set; = Set; u {+[ix. d> / u]afm}, for some set of 69 signed sentences Set. Then by rules a), b) of clause 4) of 4.2.3.1., two Seti+1 exist: a) Set; u {+(x)(v)((® A [v / x]0) -> x = v)} and b) Set; u {+[* / x](d> A [X I u]afm) U e ^(^(Set;))}. We show that if both Seti+] are strictly 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that at least one of the Seti+I is not strictly 2-derivable. So assume that both of Seti+1a), Seti+Jb) are strictly 2-derivable. Then there are finite Seql ^ Seti+Ja), Seql Q Seti+1b) such that both of Seql, Seql, are strictly 2-derivable. In case one of Seql, Seql, is a subset of Set; , then clearly Set; is strictly 2-derivable. So assume neither of Seql, Seql, are subsets of Set;. Then +(x)(v)((& A [v / x]d>) —> x = v) e Seql and there is nonempty finite set {+[tj I x](& A [X I u]afm), . . ., +[t„ I x](® A [x I u]afm)} Q{+[t/ x](® A [X I u]afm) :t e 8($o(Set;))} such that / x](® A [x I u]afm), . . . , +[tn I x](d> A [X I u]afm)} Q Seql where the / x](<2> A [X I u]afm), . . . , + [*„ . / A [x/ u]afm) are the only signed sentences in {+[*/x](d> A [x/ u]afm) U e 8(38(Set;))} which are members of Se^2. Let Seql* = Seql - [+(x)(v)((® A [v / x]&) -> x = v)}, and let Seql* = Seql - {+[tt I x](<2> A [x / u]afm), . . . , +[r„ / x](d> A [x / u]afm)}. Then the following is a finite sequence of legitimate applications of 1.2.2.6.+: Seq2* u {+[f|/x](<J> A [X / u]afm) +[tn I x](0 A [x/«i]a/«)} S e ^ i Seq2*yjSeql*KJ {+[t2 I x](<P A [ x / « ] a / m ) + ! > „ / * ] ( * A [X / u]afm)} U { + [ i x . # / u]afm} Seql Seq2*<uSeql* u { / x](<£ A [X / u)afm) +['„/x](<& A [X / «i]o/m)} u {+[tx.<£ / u]afm] Seql Seq2* \J Seql* u {+[fn / x ] (<£ A [x / u]afm)} u {+[ ix.# / u]afm) Seql Seq2* U S e ^ i * u (+[u.* / u]afm] Since both of Seql, Seql = Seql* U {+[^/x](d> A [ X I u]afm), . . . ,+[/„/x](d> A [ X / u]afm)} are strictly 2-derivable, it follows that Seql* u Seql* u {+[tx.d>/ u]afm} is strictly 2-derivable. Now, since Seql c s^ f. u {+(x)(v)((d> A [v/x]d» -» x = v)} and Seql Q Set;U {+[t/x](d> A [x/«]a/m) :te8(^(Set;))}, it follows by the facts that Seql* = 70 Seql - {+(x)(v)((d> A [ V / x ] C P ) - > x = v)} and Seql* = Seql - / x](<2> A [ X / u]afm), . . .,+[tn/x](® A [x/u]afm)}, where the +[t1lx](® A[x/u]afm), . . .,+[/„ / x ] ( C P A [x I u]afm) are the only members of {+[t / x ] ( C P A[X / u]afm) U e ^(^(Set;))} which belong to Seql, that Seql* u Seql* Q Set; . Hence, Seql* u Seql* u {+[tx.CP / «]a/w} c Sg/4.u {+[uc.d>/«]a/wi} £ 5er(-. Hence, Set; has a strictly 2-derivable finite subset and so Set; is stricdy 2-derivable. So the claim holds. ix) ±snt; is a signed elementary sentence of the form -fur.CP / u]afm for some description term ur.CP and atomic formula afm. In this case, Set; = Set; u {-[ix.CP / u]afm}. Then by rules a), b) of clause 5) of 4.2.3.1., two Seti+1 exist: a) Set; u (+(x)(v)((CP A [ V / X ] C P ) -» x = v)} and b) Set; u {+[t I x](® A - > [ X / u]afm) :t e ^ (^(Set;))}. We show that if both are stricdy 2-derivable, then so is Set;, from which it follows by the hypothesis of induction that at least one of the Seti+1 is not strictly 2-derivable. So assume that both of Set;+jSL), Set;+jb) are strictly 2-derivable. Then there are finite Seql Q Seti+1&), Seql Q Seti+Ib) such that both of Seql, Seql, are strictly 2-derivable. In case one of Seql, Seql, is a subset of Set; then clearly Set; is strictly 2-derivable. So assume neither of Seql, Seql, axe subsets of Set; . Then +(x)(v)((CP A [v / x ]CP) —> x = v) e Seql and there is a nonempty finite set / x ] ( C P A - n[x / u]afm), . . . , +[tn I x](d> A -,[x / u]afm)} s {+[t / x](® A - . [ X / u]afm) :t eS(^(Set;))} such that {+[^/x ] ( C P A - , [ X / u]afm), . . .,+[r„ / x ] ( C P A - . [ X / u\afm)} c Seql, where the +[r2 / x ] ( C P A - ! [ X / u]afm), . . . , +[tn I x ] ( C P A - > [ X / u]afm) are the only signed sentences in {+[r/x ] (CP A -\x I u]afm) :t e 8Q?*(Set;))} which are members of Seql. Let Seql* = Seql - {+(x)(v)((<Z> A [ V / x ] C P ) -> x = v)}, and let Seql* = Seql -{+[tj Ix](CP A -.[x / u]afm), . . . , +[tn I x ] ( C P A - > [ X / u]afm)}. Then the following is a finite sequence of legitimate applications of 1.2.2.6.-: Seq2* u {+[tj I x](<t> A -,[X I u]afm), . . . , +[tn I x](& A - , [ X / u]afm)) Seql Seq2*vSeql*Kj{+[t2 I A -,[X I u]afm), . . ., A -,[X I u]afm))u{-[ix.* / u]afm] Seql Seq2*vSeql* u {+[ f j /x ] (<& A -.[JC / u]afm),. . *](<P A -,[X I u]afm)} u {-[ix.<& / u]afm] Seql 71 Seq2* U Seql* u {+[*„ I A -,[X I u]afm)} u {-[i*.<& / u]afm) Seql Seq2* U U {-[IJC.<& I u]afm] Since both of Se^i, Seql = Seql* u {+[tj / x](® A-^[x I u\afm), . . . ,+[/„/x](d> A - , [x / a]a//n)} are strictly 2-derivable, it follows that Seql* u Seql* u {-[tx.d>/ u]a/m} is strictly 2-derivable. Now, since Seql Q Set; u {+(x)(v)((d> A [ V / x]<P) -» x = v)} and Se^2 c Set; u {+[// x](<£ A ->[x / u]afm) U e b(^(Set;))}, it follows by the facts that Seg/* = Seql - {+(x)(v)((d> A [ V / x]®) -> x = v)} and Se$2* £ Seql - {+[*, / x](d> A - , [ * / u]afm), . . . , +[fB / x](® A -.[x / «]a/m)}, where the +[tt / x](d> A - . [ X / u]afm), . . ., +['„ / x](<P A —i[x / u]afm) are the only members of {+[/ / x](d> A —i[x / u]afm) :t (Set;))} which belong to Seql, that Seql* u Seql* Q Set; . Hence, Seql* u Seql* u {-[ix.d> / u]afm} <± Set; u {-[ix.<P / } s S ^ . . Hence, Set; has a strictly 2-derivable finite subset and so Set; is strictly 2-derivable. So the claim holds. This concludes our case analysis. By the principle of induction, lemma 4.2.3.2. is established. • Lemma 4.2.3.3.: Let (Set) be any infinite reduction sequence of sequent Seq, and let (S() be the sequence of index sets defined with (Set;) in 4.2.3.1.. Then, for any Set;in (Set;) and any signed nonatomic sentence tsnteSet; such that Imd(±snt) <£ S;, there is ay > i such that ±snt is the first signed nonatomic sentence in Setj such that Md(±snt) £ Sj . Proof of 4.2.3.3: Let Set; be any term of (Set;) and let ±snt be any signed nonatomic sentence in Set; such that Ind(±snt) g S,-. Then for all j < i, ±snt e Setj. We show by induction on the number N(i, Md(±snt)) of signed sentences ssnt of the form +(x)F such that Ind(ssnt) < Imd(±snt) and Ind(ssnt) e. S(- that there is a j such that ±snt is the first signed nonatomic sentence in Setj such that Md(±snt) e Sy . Base step: N(/, Jnd(±snt)) = 0. Suppose the claim does not hold, that is, suppose that for all j > i, there is a signed nonatomic sentence ssnt e Setj such that Ind(ssnt) <Ind(±snt) and Md(ssnt) £ S;. For any i, let ssnt;be the first signed nonatomic sentence in Set;Such that 72 Ind(ssnt;) € S(-. Then, for all j > i, Ind(ssntp < Md(±snt). So there is an infinite sequence of natural numbers Ind(ssnt), Ind(ssnti+1),. . . , Ind(ssntj ), . . . such that for all j > i, lnd(ssntp < lnd(±snt) and Ind(ssntj+1) e S;- and Ind(ssntj+J) e Sj+1 . We now show by induction on j that for all j > i, SjQ S- + i : For j = i, since Ind(ssntp < Ind(± snt) and Ind(ssntp e S • and N(i, Md(±snt)) = 0, it follows that ssntj is not, for some formula F, of the form +(x)F. Hence S-+l- is obtained from S^ -in (S,) by a clause of 4.2.3.1. other than clause 2). Since clause 2) is the only clause of 4.2.3.1. that deletes indices from an S; in (S,), it follows that S • c Sj+1. For j > i, assume that for all k, i < k< j, Sk Q Sk+1. Since N(i, Imd(±snt)) = 0, it follows that N(j, Ind(±snt)) = 0. So, sntj is not of the form +(x)F, and so, since S y + / is obtained from Sj by a clause of 4.2.3.1. other than 2), Sj Q Sj+1. QED. We now continue with the main proof of the base step: Since for all j > i, Jnd(ssntj+1) & Sj and Md(ssntj+I) e Sj+1, it follows by the fact that for all j > i, Sj Q Sj+1 that for all j > i, for all k < j, Ind(ssntj) * Md(ssntj ). So each Ind(ssntj ) in the sequence led(ssnf-), Ind(ssnti+1),. . . , Ind(ssntj ), . . . is distinct. Hence, there are infinitely many natural numbers n such that n < Ind(±snt). But for any given natural number there are only finitely many natural numbers less than it. Contradiction. So the claim holds. Induction step: N(i, Md(±snt)) > 0. Assume as the hypothesis of induction that for all Set; in (Set) and any signed nonatomic sentence ssnt G Set- such that Ind(ssnt) e S f , if N(i, Md(ssnt)) < N(i, Md(±snt)), then there is a j > i such that ssnt is the first signed nonatomic sentence in Setj such that lnd(ssnt) £ Sj . We show that there is a j > i such that ±snt is the first signed nonatomic sentence in Set- such that Ind(ssnt) € Sj. For suppose the opposite. Suppose, that is, that for all j>i , there is a signed nonatomic sentence ssnt e Setj such that lnd(ssnt) < Jnd(±snt) and Md(ssnt) g S •. For any /, let ssnt; be the first signed nonatomic sentence in Set;Such that Ind(ssnt;) e S; . Then, for all j > i, Ind(ssntp < Ind(±snt). Now, for all j > i, Sj+1 is obtained from Sj in (S) by adding a Md(ssntj) to S^ (per one of clauses 1), 2), 3), 4), 5) of 4.2.3.1.). So there is an infinite sequence of natural numbers lnd(ssnt), Ind(ssnti+1),. . . , Ind(ssntj ), . . . such that for all j > i, Ind(ssntp < Ind(±snt) and 73 Ixad(ssntj+1) <£ Sj and Ind(ssntj+J) e Sj+1. In case for all j>i, ssntj is not, for some formula F, of the form +(x)F, it follows that for all j > i, Sj ^ Sy + y . In this case, then, for all j > i, for all k < j, Ind(ssntk) * Ind(ssntj ). Hence, each Ind(ssntj) in the sequence lnd(ssnti), Ind(ssnti+1),. . ., Ind(ssnf •), . . . is distinct, which contradicts the fact that there are only finitely many distinct natural numbers n such that n < Ind(±snt). So let v > i be a number such that ssntv is the signed sentence in the sequence Ind(ssnt-), Md(ssnti+1),. . ., Md(ssntj), . . . of the form +(x)F such that for no j, i <j < v, is ssntj of the form, for some formula G, +(x)G. It follows that for all j, i <j < v, Sy- c s . + 7 , and so S T -C S v . Hence, N(/, Ind(±siiO) ^ N(v, lnd(±snt)). Now we know that Ind(ssntv) < Ind(±snt) and Ind(ssntv ) g S v . By clause 2) of 4.2.3.1., S v + / = ( S v - R(v)) u [lmd(ssntv)}. Since R(v) contains no indices of signed sentences of the form +(x)F, it follows that N(v + 1, Md(±snt)) = N(v, Md(±snt)) - 1. Hence, N(v + 2, Md(±snt)) < N(/, Md(±snt)). So by the hypothesis of induction, there is ay > v + 7 such that ±snt is the first signed nonatomic sentence in Setv+] such that Md(ssnt) g S v + / . Since v + 1 > i, it follows that there is ay > / such that ±snt is the first signed nonatomic sentence in Setj such that Ind(ssnt ) g Sy. So the claim holds. This completes the proof of lemma 4.2.3.3. • Lemma 4.2.3.4: Let Seq be any sequent which is not strictly 2-derivable. Let (Set) be one of the infinite reduction sequences of Seq whose existence is asserted by lemma 4.2.3.2. and let Seta be the union set of (Set), i.e., Set^ = KJSet; ,0 < / < Co. Then, Set^ is downward closed. Proof of 4.2.3.4.: We show that Set^ satisfies all of conditions 1) - 10) inclusive of definition 4.1.1.. Let ±snt be any member of Set^. Then, 1) For no atomic sentence asnt does Set^ contain both of tasnt. Proof: Suppose that Set^ contain both of tasnt for some atomic sentence asnt. Since Set^ = KJSet; ,0 < i < co, there are i,j < co such that +asnt e Set; and -asnt e Setj. Asssume, 74 without loss of generality, that i>j. Then both of tasnt e Set;and so [+asnt, -asnt) Set;. Since {+asnt, -asnt] is an axiom, it is strictly 2-derivable. Since Set;has a strictly 2-derivable finite subset, by definition Set; is strictly 2-derivable. This contradicts the claim of lemma 4.2.3.2. that no Set; in (Set) is strictly 2-derivable. So Set^ satisfies condition 1) of 4.1.1.. • 2) For no t in 8(Par) does Set^ contain the signed sentence +(t = t). Proof: Suppose that Set^ contains the signed sentence +(/ = /) for some basic constant term t in b(Par). Since Seta = KJSet; ,0 < / < co, there is / < co such that +(/ = t) e Set; . Since {+(t =t)} is an axiom, it is strictly 2-derivable. Since Set; has a strictly 2-derivable finite subset, by definition Set; is strictly 2-derivable. This contradicts the claim of lemma 4.2.3.2. that no Setim (Set) is strictly 2-derivable. So Set^ satisfies condition 2) of 4.1.1.. • 3) For no r, s in $(Par) does Set contain both of +(r = s), -(s = r). Proof: Suppose there are r, s in §(Par) such that Set^ contains both of +(r = s), -(s = r). Since Set^ = VJSet; ,0 < i < co, there is i,j < co such that +(r = s) e Set; and -(s = r) e . Assume without loss of generality that i > j. Then +(r = s), -(s = r) e Ser,-. Since the sequents {+(s = s)}, {-(r = s) , +(r = s)} are both axioms, the following is a legitimate Pld2 strict derivation of the sequent {+(r = s), -(s = r)}: {+(s = s)} [+(r = s),-(r = s)} {+(r = s),-(s = r)} Thus {+(r = s), -(s = r)} is a strictly 2-derivable sequent. But by lemma 4.2.3.2. no Set;, Set; in (Set) is stricdy 2-derivable. So [+(r = s), -(s = r)} is not a subset of Set; for any i . So SetQ) satisfies condition 3) of 4.1.1.. • 4) For no r, s in b(Par) and atomic formula afm does Set contain all of -(r = s), -[r / v\afm, +[s I v]afm. Proof: Suppose that for some r, s in 6(Par) and atomic formula afm, Set contain all of -(r = s), 75 -[r / v]afm, +[s I v]afm. Since Set^ = ^ Set; , 0 < i < co, there are & < co such that -(r = s) e Ster,-, -[r/ v]a//n e , and +[s/ v]afm e Sef^ . Assume, without loss of generality, that i>j> k. Then all of -(r = s), -[r/ v]afm, +[s I v]afm e Se^and so {-(r = s), -[r / v]a/m , +[s I v]afm} Q Set; . We show that {-(r = s), -[r / v]a/m , +[s / v]afm} is a strictly 2-derivable sequent. The following is a legitimate application of the identity rule 1.2.2.7.: {-[r / v\afm , +[r / v\afm} {-[s I v]afm , +[s I v]afm} {-(r = s), -[r I v]afm , +[s I v]afm} Since both of {-[r I v]afm , +[r / v]afm], {-[s I v]afm , +[s I v]afm} are axioms, it follows that {-(r = s), -[r / v\afm , +[s I v]afm} is a strictly 2-derivable sequent. Since Set- has a strictly 2-derivable finite subset, by definition Set; is strictly 2-derivable. This contradicts the claim of lemma 4.2.3.2. that no Set; in (Set) is strictly 2-derivable. So Setm satisfies condition 4) of 4.1.1.. • Since ±snt e Set^ = {JSeti ,0<i< co, and (Set) is well-ordered under Q, it follows that ±snt e Setifor some least /, 0 < i < CO. We now show that Set^ satisfies conditons 5) - 10) of definition 4.1.1.: 5) If ±snt is respectively of the form ±—iA, for some sentence A, then Set^ contains respectively Proof: Assume that ±snt is respectively of the form ±-iA. Since for ally < /, ±—iA eSetj, it follows by definition 4.2.3.1. of (Set) that respectively Ind(±-iA) g S(. . Since ±-iA eSet; and Irad(±-iA) <£ S{. , by lemma 4.2.3.3., there is a j > i such that ±-iA is the first signed sentence in Setj such that respectively Ind(±—iA) ^ S^ . Hence, by clause 1) of 4.2.3.1., Setj+I is an S{. -reduction of Setj of type 1) and so Setj+1 = Setju {+A}, respectively. Since Setj+1 Q Set^, it follows that respectively +A e Set^. So Set^ satisfies condition 5) of 4.1.1. • 6) If ±snt is respectively of the form ±(A A B), for some sentences A, B, then Set^ contains one of +A, +B, respectively, both of -A, -B. 76 Proof: Assume that ±snt is respectively of the form ±(A A B). Since for all j < i, ±(A A B) eSetj, it follows by definition 4.2.3.1. of (Set) that respectively Ind(±(A A B)) g S,. . Since ±(A A B) GSet;and Ind(±(A A B)) e S ; , by lemma 4.2.3.3., there is ay >i such that ±(A A B) is the first signed sentence in Setj such that respectively Ind(±(A A B)) g Sj. Hence, by clause 1) of 4.2.3.1., Setj+J is an S; -reduction of Setj of type 2) and so Setj+1 contains one of, respectively, both of, A , B. Since Setj+1Q Set^, it follows that Set& contains one of, respectively, both of, A, B. So Set^ satisfies condition 6) of 4.1.1.. • 7) If ±snt is respectively of the form ±(A —> B), for some sentences A, B, then Set^ contains both of -A, +B, respectively, one of +A, -B. Proof: This case is similar to condition 6) above. • 8) If, for some formula F, ±snt is respectively of the form ±(x)F, then Set^ contains +[p I x]F for some p in ^(Set^), respectively, -[t I x]F for every t in SQ^3 (Set ($))-. Proof: There are two cases: i) ±snt is of the form +(x)F. Since for ally < i, +(x)F <£Setj, it follows by definition 4.2.3.1. of (Set) that Ind(+(x)F) e Si . Since +(x)F eSftf-and Imd(+(x)F) e S- , by lemma 4.2.3.3., there is a j > i such that +(x)F is the first signed sentence in Setj such that Imd(+(x)F) g S • . Hence, by clause 2) of 4.2.3.1., Setj+1 = Set-^J {+[p I x]F}, where p is in 3s(Setp Q ^(Set^). Since Setj+J ^ Set^, it follows that +\p I x]F e Set^. So Set^ satisfies condition 8). ii) ±snt is of the form -(x)F. We want to show that -[t I x]F e Set^ for every tin ^(^(Set^)). So let s be any term in ^(^(Set^)). Since the sequence (j? 3(Set)) is well ordered under Q, there is a least i such that s e 8(^(Set); let that least i be V. It follows that ^(Set^j) Q S^iSet;') but ^(Set;.) $ ^(Set^j). Since for all i , clause 2) is the only clause of 4.2.3.1. that adds new parameters to a.^(Set), it follows that Setv is obtained from Setri in (Set) by clause 2). Hence, S r = 0 . There are two subcases: 77 a) /' < i. Since for all j < i, -(x)F eSetj, it follows by definition 4.2.3.1. of (Set) that Ind(-(jc)F) e= S- . Then, since -(x)F eSVf-and Md(-(x)F) e S- , by lemma 4.2.3.3., there is a j > i such that -(x)F is the first signed sentence in Setj such that Ind(+(x)F) e Sj . Then, by clause 3) of 4.2.3.1., Setj+1 = Setj u {+[t I x]F : / g 8(&*(Setp)}. Since j> i > i', 9s(Set;.) c $o(Setp, and so S(^(Setr)) Q 8(9>(Setp). Hence, -[s I x]F e Setj+J Q Setfjy. So Set^ satisfies condition 8). b) i < i'. Since Set; Q Set;., -(x)F eSetr . Then by lemma 4.2.3.3., since Ind(-(x)F) g S r , there is ay > V such that -(x)F is the first signed sentence in Setj such that Ied(+(x)F) g Sy . Then, by clause 3) of 4.2.3.1., Setj+J = Setj u [+[t / x]F : t e b(^(Setp) }. Since j> V, 9>(Setr) Q &(Setp, and so 8(^(Setr)) Q 8(^(Setp). Hence, -[s I x]F e Sef y. + / c Sto^. So Set^ satisfies condition 8). In all cases, then, Set^ satisfies condition 8). • 9) If ±snt is a signed nonatomic elementary sentence of the form +[ix.<P I u\afm for some constant description term uc.<3> and atomic formula afm, then Set^ satisfies one of the following conditions: i) Set^ contains the signed sentence +(x)(v)((® A [ V / x]&) —> x = v) for some variable v. ii) Seta contains the signed sentence +[/ I x](® A [x I u]afm) for every te ^(^(Set)). Proof: Assume that ±snt is of the form +[ix.&/ u]afm. Since for all j < i, +[ix.&/ u]afm eSetj, it follows by definition 4.2.3.1. of (Seq) that Ind(+[ix.d> / u]afm) <2 S ; . Since +[ix. 01 u]afm e Set; and Ind(+[ur. <P I u]afm) £ S; , by lemma 4.2.3.3., there is a j > i such that +[vx.&/ u]afm is the first signed sentence in Setj such that Md(+[ix.0/ u]afm) e Sy- . Let j' be the least such y, i.e., let y" be such that +[ix.&/ u]afm is the first signed sentence in Setj. such that Ind(+[uc.d>/ u]afm) g S-. and for all k <y", it is not the case that +[ix.&/ u]afm is the first signed sentence in Setk such that Ind(+[ur. <P / u]afm) <£ S^ . We observe that by definiton 4.2.3.1., for all / and signed sentences ssnt, Md(ssnt) eDl t only if there is ay < i such 78 that ssnt is the first signed sentence in Setj such that lnd(ssnt) £ Sj. Hence, Ind(+[xx.® / u]afm) g Dly. . Hence, by clause 4) of 4.2.3.1., there are two cases: i) Setj.+1 is obtained from Setj. by rule a) of clause 4). Then, Setj.+1 = Setj. u [+(x)(v)((® A [v /x]®) —> x - v)} for some variable v. Since Setj.+1 c Set^, it follows that +(JC)(V)((CP A [ V / x]®) —> JC = v) e Set^. So Set^ satisfies i) of condition 9). ii) Setj.+1 is obtained from Setj. by rule b) of clause 4). Then, D l > 7 = Dly.u {lmd(+[u:.d>/ u]afm)}. We want to show that +[// x](® A [X I u]afm) e Seta for every* in ^(^(Set^)). So let s be any term in ^(^(Set^)). Since the sequence (^(Set)) is well ordered under there is a least i such that s e ^(^(Set)); let that least / be i". It follows that ^(Set^j) Q ^(SetJ but ^(Set;) $ ^(Set^j). Since for all i, clause 2) is the only clause of 4.2.3.1. that adds new parameters to a ^(Set), it follows that Setr is obtained from Setr j in (Set) by clause 2). Hence, S = 0 . There are two subcases: a) j" +1 > V. We have that +[ix.® / u]afm is the first signed sentence in Setj. such that Ind(+[xx.® / u]afm) g Sj. and that Setj.+1 is obtained from by rule b) of clause 4). Hence, Sety+l = Setj.KJ {+[t I x](® A [X I u]afm) :t e ^(^(Setj))}. Clearly, since f>i' and s e 8(^a(Seti.)), s e 5(^(Setj.)). So +[s / x](® A [ X / w]a/m) e $ety+1 c S e ^ . So satisfies ii) of condition 9). b) /' > f +1 . Since f > i, it follows that i' > i, so we know that +[uc.<2> / u]afm e Setr . Since S f = 0 , Ind(+[xx.® / u]afm) g S r , so by lemma 4.2.3.3. there is a y > i' such that +[u\d>/ u]afm is the first signed sentence in Setj such that Ind(+[u\d>/ u]afm) g Sj . Now, since Imd(+[u\d>/ u]afm) e D l y , + y and j > i'> j' +1, it follows by definition 4.2.3.1. that Ind(+[ix.®/ u]afm) e Dly . Hence, Setj+1 is not obtained from Setjby rule a) of clause 4) of 4.2.3.1., but rather is obtained from Setjby rule b) of clause 4). Hence, Setj+I = Setju {+[t/ x](® A [x I u]afm) :t e 8(&(Setj))}. Clearly, since j > V and s e 8(^(Setr)), s e ^(^(Setj)). So +[s I x](® A [X I u]afm) e £ Seta. So Sef^ satisfies ii) of condition 9). 79 In all cases, then, Set^ satisfies condition 9) of 4.1.1.. • 10) If ±snt is a signed nonatomic elementary sentence of the form -[ix.® I u]afm for some constant description term ix.<P and atomic formula afm, then Set^ satisfies one of the following conditions: i) SetfQ contains the signed sentence +(x)(v)((® A [v / x]<P) —> x = v) for some variable v. 11) Set^ contains the signed sentence +[tl x](® A ->[X I u]afm) for every t e SQ^iSet)). Proof: The proof of 10) is similar to the proof of 9) above. • This completes the proof of lemma 4.2.3.4.. Lemma 4.2.3. is established by lemmas 4.2.3.2. and 4.2.3.4. as follows: Let Seq be any sequent which is not strictly 2-derivable. By 4.2.3.2., Seq has an infinite reduction sequence (Set) such that Seq = Set0 and no Set; in (Set) is strictly 2-derivable. Then by 4.2.3.4., Set^ = ^ USet; ,0<i< CO, is downward closed. Since Seq Q Seta, it follows that Seq has a downward closed extension Set^. We now restate and prove lemma 4.2.4.: Lemma 4.2.4.: Every downward closed set Set of signed sentences determines a base bse(Set) such that Set n Cl(bse(Set)) = 0 . Proof of 4.2.4.: Let Set be a downward closed set of signed sentences. Let F be any formula. We recursively define a downward closed extension Set* of Set as follows: 0) Set0 = Set; 1) Seti+J is obtained from Set; by adding to Seti a ^ s i g n e d sentences of the form ±{p / x]F such that respectively ±[P(1) / x]F is in Set; , where p is the first (relative to the enumeration P) parameter that does not occur in any member of Set;. In other words Seti+1 =Set;U {±fP(0/x]F: ± [P( l ) /x ]Fe Sett and P(i) e Par - &(Set) and for all 80 j<i, P(/)e S°(Set.)}. 2) Set* = U Set; ,0<i < co. Lemma 4.2.4.1.: Let Set be a downward closed set of signed sentences, and let Set* be as defined above. Then Set* is downward closed. Proof of 4.2.4.1.: We show by induction on / in the recursive definition of Set* that every Set; is downward closed. Let ±snt be any member of Set*. Then, Base step: / = 0. By assumption, SetQ = Set is downward closed. So the claim holds. Induction step: / > 0. Assume that for all j < i, Setj is downward closed. We show that Set; satisfies all of conditions 1) -10) inclusive of definition 4.1.1: 1) For no atomic sentence asnt does Set; contain both of ±asnt. Proof: Assume that Set; contains both of tasnt for some atomic sentence asnt. Now, asnt can be written as [p I x]afm for some atomic formula afm containing no occurrence of p, where p is the first parameter in Par - ^(Set; j). Clearly, then, since both of ±[p I x]afm are in Set; and afm contains no occurrence of p, it follows by clause 1) of the recursive definition of Set* that Set;j contains both of ±[P(1) / x]afm. This contradicts the hypothesis of induction. 2) For no / in 8 (^(Set})) does Set; contain the signed sentence +(/ = t). Proof: Assume that Set; contains the signed sentence +(t = t) for some t in hi^iSet;)). Now the signed sentence +(t = t) can be written as +[p I x](s = s) for some basic term s containing no occurrence of p, where p is the first parameter in Par - ^(Set^ j). Since +[p I x\(s = s) e Set; and s contains no occurrence of p, it follows by clause 1) of the recursive definition of Set* that +[P(1) / x](s = s) e Set;_j . But clearly, the signed sentence +[P(1) / x](s = s) is of the form +(r = r) for some r in 8 (^(Set;)). So for some r in 8 (^(Set;)), Set{1 contains the signed sentence +(r = r ) . This contradicts the hypothesis of induction. 81 3) For no r, s in 8(^ s(Ser i)) does Set; contain both of +(r = s), -(s = r) . Proof: The proof that Set; satisfies condition 3) is similar to the proof above that Set; satisfies condition 1). 4) For no r, s in ^(^(Set;)) atomic formula afm , does Set; contain all of -(r = s), -[r / v]afm, +[s I v]afm. Proof: Assume that for some r, s in 8( v? 8(Sef J)) and atomic formula afm, Set; contains all of -(r = s), -[r I v]afm, +[s I v]afm. Now -(r = s), -[r I v]afm, +[s I v]afm can be respectively writtten as -[p I x\{tl = t2), -[p I x] [[p I x]tj I v]afm', +{p I x][[p I x]t2 I v]afm' for some basic terms t1 , t2 and atomic formula afm' such that none of t1,t2 , afm' contain an occurrence of p, where p is the first parameter in Par — ^(Set;^). Since all of -[p I x](tt = t2) , -[p I x][[p I x]tj I v]afm', +[p I x][\p I x]tjI v]afm' are in Set;, and none of tt, t2, afm' contain an occurrence of p, it follows all of -[P(l) / x\(f1 = t2) = -(DP(1) / x]tj = [P(l) / x]t2), - [ P ( l ) / J f][[P(l) / x]tj I v]afm', +[P(1) / x ] [ [ P ( l ) / x]tt I v]afm' are in Setu . This contradicts the hypothesis of induction. 5) If ±snt is respectively of the form ±—iA, then Set; contains respectively +A. Proof: Assume that ±snt is respectively of the form ±-iA. Now —iA is of the form [p I xY-J7 for some formula F containing no occurrence of p, where p is the first parameter in Par — ^{Set; j). Since respectively ±[p I x]—>F is in Set; and F contains no occurrence of p, it follows that the signed sentence respectively ±[P(1) / x]—iF is in Set; L . Set; } is downward closed by the hypothesis of induction, so by condition 5) of 4.1.1., Set;^ contains respectively +[P(1) / x]F. Then by clause 1) of the recursive definition of Set*, Set; contains respectively +{p I x]F = +A. So the claim holds. 6) If ±snt is respectively of the form ±(A A B) , then Set contains one of +A, +B, respectively, both of -A, -B . 82 Proof: Assume that ±snt is respectively of the form ±(A A B) for some signed sentences A, B. Now A, B are respectively of the form [p I x]F, [p I x\G, for some formulas F, G containing no occurrence of p, where p is the first parameter in Par - ^(Set;^). Since respectively ±(A A B) = ±([p I x]F A [p I x]G) is in Set; and neither F nor G contains an occurrence of p, it follows by clause 1) of the recursive definition of Set* that Set;j contains respectively ±([P(1) / x]F A [P(l) / x]G). By the hypothesis of induction, Set; y is downward closed, so by condition 6) of 4.1.1., Set;_} contains one of +[P(1) / x]F, +[P(1) / x]G, respectively, both of -[P(l) / x]F, -[P(l) / x]G. Then by clause 1) of the recursive definition of Set*, Set; contains one of +[p I x]F, +\p I x]G, respectively, both of -[p I x]F, -[p I x]G. So Set; contains one of +A, +B, respectively, both of -A, -B. So the claim holds. 7) If ±snt is respectively of the form ±(A —> B), then Set; contains both of -A, +B, respectively, one of +A, -B. Proof: The proof that Set; satisfies condition 7) is similar to the proof above that Set; satisfies condition 6). 8) If ±snt is respectively of the form ±(x)F, then Set; contains +[p I x]F for some p in ^(Set;), respectively, -[/ / x]F for every / in ^(^(Set;)). Proof: Assume that ±snt is respectively of the form ±(x)F, for some formula F. Now, F is of the form [p I y]G, for some formula G containing no occurrence of p, where p is the first parameter in Par - ^(Set;:i). We treate the two cases seperately: i) ±snt is of the form +(x)F. Since +(x)F = +(x)[p Iy]G = +\p Iy](x)G is in Set; and G contains no occurrence of p, it follows by clause 1) of the recursive definition of Set* that Set;^ contains +[P(1) / y](x)G = +(x)[P(l) / y]G. By the hypothesis of induction, Sethis downward closed, so by condition 7) of 4.1.1., Set^j contains +[q / x]\P(l) Iy]G = +[P(1) / y\[q I x]G for some q in ^(Set;^). Then by clause 1) of the recursive definition of Set*, Set; contains +[p I y][q I x]G = +[q I x]\p I y]G = +[q I x]F for some q in ^(Set;^) Q 5s(Set) . So the claim holds. 83 ii) ±snt is of the form -(x)F. Since -(x)F = -(x)[p I y]G = -\p /y](x)G is in SW(-and G contains no occurrence of p, it follows by clause 1) of the recursive definition of Set* that Set; j contains -[P(l) /y](x)G = +(x)[P(l) I y]G. By the hypothesis of induction, Set; j is downward closed, so by condition 8) of 4.1.1., Set;; contains -[tlx][P(l) /y]G . Let r be any term in b'i&'iSet;)). Now, r is of the form [p I y]s for some variable y and term s such that s contains no occurrence of p. Then [P(l) / y]s is a term in b^iSet;^)). So Set;_j contains -[[P(l) / y]s I x][P(l) / y]G. Hence, by clause 1) of the recursive definition of Set*, since neither G nor s contain an occurrence of p , Set; contains -[[p Iy]s I x][p Iy]G = -[[p Iy]s I x]F = -[rl x]F, which is what we want to show. In both cases, then, the claim holds. 9) If ±snt is a signed nonatomic elementary sentence of the form +[\x.& / u]afm for some constant description term xx.O and atomic formula afm, then Set; satisfies one of the following conditions: i) Set; contains the signed sentence +(x)(v)((<P A [ V / x]<P) —> x = v) for some variable v. ii) Set; contains the signed sentence +[t I x](0 A [X I u]afm) for every t e bi^iSet;)). Proof: Assume that ±snt is a signed nonatomic elementary sentence of the form +[ix.&/ u]afm for some constant description term ur.d> and atomic formula afm. Now, the formulas d>, afm are respectively of the form [p Iy] f , [p Iy]afm' for some variable y and formulas f , afm' such that *F and afm' contain no occurrence of p, where p is the first parameter in f a r -<F(Set;_j). Since +[u\<P / u]afm = +[ix.[p Iy]*¥I u] [p Iy]afm' = +[p 'yftix.*FI u]afm' is in Set; and neither d>nor afm contain an occurrence of p, it follows by clause 1) of the recursive definition of Set* that Set^j contains +[P(1)/yftix.Y/u]afm' = +[u:.[P(l) Iy]*FI «][P(1) I y]afm'. By the hypothesis of induction, Set^j is downward closed, so by condition 9) of 4.1.1., there are two cases: i) Set;_j contains the signed sentence +(x)(v)(([P(l) /y]*F A [ V /x] [P(l) / v]1?) x = v). 84 Now, the signed sentence +(x)(v)(([P(l) I y] f A [v / x] [P(l) /y] tF)^>x = v) may be written as +[P(1) / J'](x)(v)((y /A [v / x] *F) —> x = v). So by clause 1) of the recursive definition of Set*, since *¥ contains no occurrence of p,Set; contains +[p / / K x X v X C fA [VIX\*V) -» x = v) s +(x)(v)((|> / # A [ V / X ] | > / ^ ) - ) I = V ) S +(x)(v)((<P A [v / x]<P) -> x = v). So the claim holds. ii) For every te Si^iSet;^)), Set;_t contains the signed sentence +[t/x]([P(l) / y]*F A [P(l) /y]afm'). Now let r be any term in bi^^Set;)). Now, r is of the form [p Iy]s for some term s such that s contains no occurrence of p. Then [P(l) / y]s is a term in bi^iSet; j)). So Ser- 7 contains the signed sentence +[[P(1) / y]s / x]([F(l) I y\*¥ A [P(l) /y]afm') = + [P(l) /^] [s/ X I C F A afm'). Since none of s.f, a//n' contain an occurrence of p, by clause 1) of the recursive definition of Set*, Sett contains +[p / y] [s I x ] ( f A o/m') £ / y]s I x]([p / y] V A \p I y]afm') = +[rl x](4> A afm), which is what we want to show. In both cases, then, Set; satisfies condition 9). 10) If ±snt is a signed nonatomic elementary sentence of the form -[ix.& /u]afm for some constant description term ix.& and atomic formula afm; then Set; satisfies one of the following conditions: i) Set; contains the signed sentence +(x)(v)((d> A [ V / x]&) —» x = v) for some variable v. 11) Set; contains the signed sentence +[t I x](d> A —>[X I u]afm) for every / e ^(^(Set;)). Proof: The proof that Set; satisfies condition 10) is similar to the proof above that Set; satisfies condition 9). That Set* is downward closed follows immediately from the facts that, by definition, Set* = Set; ,0<i < co and that for all i, 0 < / < co, Set; is downward closed. This completes the proof of lemma 4.2.4.1. • Lemma 4.2.4.2.: Let Set be a downward closed set of signed sentences, and let Set* be as defined above. Let ±snt be any signed sentence in Set*. Then, if ±snt is of the form -(x)F for 85 some formula F containing free occurrence of x, then ^(Set*) = Par. Proof of 4.2.4.2.: Let ±snt be any signed sentence in Set* such that ±snt is of the form -(x)F for some formula F containing free occurrence of x. Since by lemma 4.2.4.1. Set* is downward closed, by condition 8) of definition 4.1.1., Set* contains the signed sentence -[// x]F for every / in b($8(Set*). Since by definition 1.1.1.4., P(l) e §($8(Set*), it follows that Set* contains the signed sentence -[P(l) / x]F. Then it is easily verified by induction on / in the definition of Set* that Set* contains the signed sentence -[P(0 / x]F for every i < co. Since F contains free occurrence of x, it follows that $°(Set*) = Par. • Lemma 4.2.4.3.: Let Set be a downward closed set of signed sentences, and let Set* be as defined above. Let ±snt be any signed sentence in Set*. Then, if ±snt is of the form ±[ix.®/ u]afm for some constant description term ix.® and atomic formula afm containing free occurence of u, and for no variable v does Set* contain the signed sentence +(x)(v)((® A [v / x]®) -> x = v), then 9s(Set*) = Par. Proof of 4.2.4.3.: Let ±snt be any signed sentence in Set* of the form ±[ix.® I u]afm for some constant description term ix.® and atomic formula afm containing free occurence of u such that for no variable v does Set* contain the signed sentence +(x)(v)((® A [ V / x]®) —» x = v). Since, by lemma 4.2.4.1., Set* is downward closed and i) of condition 9), respectively, 10) of 4.1.1. is not satisfied, by ii) of condition 9), respectively, 10) of 4.1.1., Set* contains the signed sentence +[t I x](® A [X I u]afm), respectively +[t I x](® A —i[x / u]afm), for every / in 8(^(Se*). Since, by definition 1.1.1.4., P(l) e ^(^(Set), it follows that Set* contains the signed sentence +[P(1) / x](® A [X I u]afm), respectively, +[P(1) / x](® A - I [ X / u]afm). Then it is easily verified by induction on i in the definition of Set* that Set* contains the signed sentence +[P(0 / x](® A [xl u]afm), respectively, +[P(0 / x](® A —\x I u\afm) for every / < CO. Since afm contains free occurrence of u, it follows that $°(Sei*) = Par. • Now, let Set be a downward closed set of signed sentences, and let Set* be as defined above. Let B l be the set of atomic sentences +asnt such that respectively tasnt is in Set*. We extend B1 to a base bse(Set) with domain ^(^(Set*)) by the following operations: 86 a) Let t be any term in 8(Par). Then B2 is obtained from B l by adding to B l all signed atomic sentences of the form +(t = t). b) Let r, s be any terms in b(Par) such that neither of ±(r =s) is a member of B2. Then B3 is obtained from B2 by adding -(r =s) to B2. c) Let asnt be any atomic sentence such that neither of tasnt is in B3, and let r , j e S(Par). Then B4 = bse(Set) is obtained from B3 by adding to B3 one and only one of tasnt with the following proviso: if asnt is of the form [r / x]afm for some atomic formula afm and +(r = s) e B3, then if +[r /x]afm is added to B3, then so is +[s I x]afm. Lemma 4.2.4.4.: Let Set be a downward closed set of signed sentences, and let bse(Set) be as defined above. Then bse{Set) is a base with domain 8(Par). Proof of 4.2.4.4.: We show that bse(Set) satisfies all of conditions 1), 2), 3) of definition 1.3.1. : 1) For every atomic sentence asnt, exactly one of tasnt is in bse(Set). Proof: By operation c) above, bseiSei) contains at least one of tasnt for every atomic sentence asnt. To show that bseiSet) contains at most one of tasnt for every atomic sentence asnt, we show that B1 has this property and that operations a), b), c) preserve the property. Since by hypothesis Set* is downward, by condition 1) of definition 4.1.1.1., Set* contains at most one of tasnt for every atomic sentence asnt. It follows by the definition of B1 that B1 contains at most one of tasnt for every atomic sentence asnt. Now we show that operation a) preserves this property: Assume that B2 contains both of tasnt for some atomic sentence asnt. In case asnt is of the form (t = /), since operation a) adds to B l signed sentences with positive signature only, B1 contains the signed sentence -(/ = Then by the definition of B l , Set* contains the signed sentence +(t = t). But since Set* is downward closed, by condition 2) of 4.1.1., Set* contains no such signed sentence. Contradiction. In case asnt is not of the form (/ = /) for some t e b"(SP(Set*)), since operation a) adds to B l signed sentences of this form only, B l contains both of tasnt. Now we show that operation b) preserves the desired property: Assume that B3 87 contains both of tasnt for some atomic sentence asnt and that for no atomic sentence asnt does B2 contain both of tasnt. Then we know that at least one of tasnt is added to B2 by operation b) and since the only type of signed sentence operation b) adds to B2 are identity statements of negative signature, it follows that asnt is of the form (r = s) for some r , j e 8(Par) and that by operation b) adds the signed sentence -(r = s) to B2. Then, by operation b), B2 does not contain +(r =s), i.e., +asnt £ B2. Contradiction. Finally, it is trivial to show that operation c) preserves the desired property. 2) For all terms t e &(Par), +(t =t) is in bseiSet). Proof: By operation b), B2 ^ bse(Set) satisfies this condition. 3) For all terms r , $e 8(Par) and atomic formulas afm, if both of +[r / x]afm, -[s I x]afm are signed sentences in bseiSet), then so is -(r = s). Proof: Let r, s be any terms in 8(Par) and let afm be any atomic formula. We want to show that if both of +[r / x]afm, -[s I x]afm are signed sentences in bseiSet), then so is the signed sentence -(r = s). So we show the contrapositive, that if -(r = s) e bseiSet), then it is not the case that both of +[r / x]afm, -[s I x]afm e bseiSet). So assume that (r = s) e bseiSet). We show first that B2 does not contain both of +[r / x]afm, -[s I x]afm: We may assume that x has free occurrence in afm, since otherwise the claim holds trivially by the fact that bse(Sei) satisfies condition 1). Since by condition 1) above bseiSet) contains at least one of tasnt for every atomic sentence asnt, it follows that +(r = s) e bseiSet). Since neither operation b) nor c) adds signed sentences of the form +(r =s) (i.e., positive identity statements) to B2 or B3, it follows that +(r =s ) e B2. In case r is syntactically identical to s, so that the signed sentence +(r =s) is of the form +(r = r), it is trivially the case that if the signed sentence +[r / x]afm is in B2, then so is +[s I x]afm. In this case, then, since by condition 1) bse(Set) contains at most one of tasnt for every atomic sentence asnt, it is not the case that both of +[r / x]afm, -[s I x]afm are in B2. In case r is not syntactically identical to s, since operation a) adds to B l signed sentences of the form +(f = t) only, it follows that +(r =s) e B l . Since +(r = s) e B l , by the definition of B l , -(r =s) e 88 Set*. Since Set* is downward closed and -(r=s) e Set*, by condition 4) of 4.1.1., Set* does not contain both of -[r / x]afm, +[s I x]afm. So, by the definition of B l , B l does not contain both of +[r / x]afm, -[s I x]afm. It follows that B2 does not contain both of +[r / x]afm, -[s Ix]afm, for suppose that B2 does contain both of +[r / x]afm, -[s I x\afm. Since B l does not contain both of +[r/x]afm, -[s I x]afm and operation a) adds to B l signed sentences with positive signature only, it follows that B1 contains -[s / x]afm and operation a) adds +[r / x]afm to B l . Since operation a) adds to B l signed sentences of the form +(t =t) only and JChas free occurrence in afm, +[r / x]afm is of the form +(r =r). Then -[s I x]afm e B l is of one of three forms: -(s =s), -(s = r), or -(r = s). Since Set* is downward closed, by condition 2) of 4.1.1., Set* does not contain +(s =s) and hence, by definition, B l does not contain -(s =s). Since +(r = s) e B l and bseiSet) satisfies condition 1), -(r = s) £ B l . Hence, -[s Ix]afm e B l is of the form -(s =r) . So B l contians both of +(r = s), -(s =r), and hence Set* contains both of -(r = s), +(s =r). But since Set* is downward closed, by condition 3) of 4.1.1., Set* does not contain both of -(r = s), +(s =r). Contradiction. So we have shown that B2 does not contain both of +[r / x]afm, -[s I x]afm: But, trivially, operation c) preserves this property, so B4 = bseiSet) does not contain both of +[r / x]afm, -[s I x]afm: • Lemma 4.2.4.5.: Let Set be a downward closed set of signed sentences, and let Set*, bseiSet) be as defined above. Then, Set* n Cl(bse(Set)) = 0 . Proof of 4.2.4.5.: We show by transfinite induction on fi in definition 1.3.3. that for all fi, Set* n bseiSet) = 0 . So assume that there is an ordinal fi such that Set* n bseiSet) * 0 . Since (bseiSet) ) is well ordered under Q, there is a least ordinal fi such that Set* n bseiSet) * 0 . So let ±snt e Set* n bseiSet) . There are three main cases: i) fi = 0: Since ±snt e bseiSet)0, snt is atomic. So, since ±snt e Set*, by the definition of B l , respectively +snt e B l . Since B l ^ bseiSet) = bseiSet)0 , it follows that both of ±snt e bseiSet). This contradicts lemma 4.2.4.4.. ii) JJ.is a nonzero limit ordinal: Since ±snt e bseiSet)^and bseiSet)^ = bseiSet)p , 0 </3 89 < CO, there is a /3 < co such that respectively ±snt e bse(Set)p . Contradiction, iii) /i is a successor ordinal: There are five subcases: 1) ±snt is respectively of the form ±—iA, for some sentence A . Since ±-iA e Set* and, by lemma 4.2.4.1., Set* is downward closed, by condition 5) of 4.1.1., Set* contains the signed sentence respectively +A. Since ±—iA G bse(Set) and (bse(Set) ) is well ordered under there is a least ordinal < ji such that respectively ±—iA e bse(Set)p . So, since ±—iA G bse(Set)p but for all y< p, respectively ±-iA e bse(Set)y , it follows that ±-.A e Sc(bse(Set)p_1) by virtue of the semantic rule 1.3.2.1.. Hence bse(Sei)p_l contains the signed sentence respectively +A. Hence +A e Set* r\bse(Set)p_j . But since/J < I I , P~ 1<JI. So there is a P < Li such that Set* n bse(Set)p * 0 . Contradiction. 2) ±snt is respectively of the form ±(A A B) for some signed sentences A, B. Since ±(A A B) e Set* and, by lemma 4.2.4.1., Set* is downward closed, by condition 6) of 4.1.1., Set* contains one of +A, +B, respectively, both of -A , -B . Since ±(A A B ) e bse(Set) and (bse(Sei)y) is well ordered under Q, there is a least ordinal P<fi such that respectively ±(A A B) G bse(Set)p . So, since ±(A A B ) G bse(Sei)p but for all y< P, respectively ±(A A B ) G bse(Sei)y, it follows that ±(A A B) G ScibseiSefip^) by virtue of the semantic rule 1.3.2.2.. Hence bse(Set)p_l contains both of +A, +B, respectively, one of -A , -B . Hence Set* C\ bse(Set)p_t contains one of +A, +B, respectively, one of -A, -B. But since P < /i, /3- 1< /x. So there is a P < /i such that Set* n bse(Set)p * 0 . Contradictiort. 3) ±snt is respectively of the form ±(A —> B) for some signed sentences A, B. This subcase is similar to subcase 2) above. 4) ±snt is respectively of the form ±(x)F for some formula F. Since ±(x)F G bse(Set) and (bse(Set) ) is well ordered under Q, there is a least ordinal P < ji such that respectively ±(x)F e bse(Sei)p . So, since ±(x)F G bse(Set)p but for all y< P, respectively ±(x)F e bse(Set)y, it follows that ±(x)F G Sc(bse(Set)«_,) by virtue of the semantic rule 1.3.2.4.. We treate the two 90 cases seperately: a) ±snt is of the form +(x)F. Hence bse(Set)p_rl contains the signed sentence +[t/x]F for every t in 8(Par). Since +(x)F e Set* and, by lemma 4.2.4.1., Set* is downward closed, by condition 8) of 4.1.1., Set* contains the signed sentence +[p I x]F for some p in <?°(Set*). Since p e Par, p e 8(Par). So bse(Set)p_{ contains the signed sentence +[p I x]F. Hence Set* n bse(Set)p_j contains the signed sentence +[p I x]F. But since < fi, fi - 1< fi. So there is a /3 < }J. such that Set* n bse(Set)p * 0. Contradiction. b) ±snt is of the form -(x)F. Hence bse(Set)p_1 contains the signed sentence -[t I x]F for some tin 8(Par). Since -(x)F e Set* and, by lemma 4.2.4.1., Set* is downward closed, by condition 8) of 4.1.1., Set* contains the signed sentence -[tlx]F for every tin 5(SP(Set*)). In case x does not occur free in F, [t I x]F = F, and so Set* n bse(Set)p_1 contains the signed sentence -F. In case x occurs free in F, by lemma 4.2.4.2., ^ (Set*) = Par. Then, in this case, Set* contains the signed sentence -[t I x]F for every t in &(Par). Hence Set* n bse(Set)p_l contains the signed sentence / x]F for some t in b~(Par). But since /3 < \i, p — 1< / i . So in either case there is a /3 < such that Set* n bse(Set)p * 0. Contradiction. 5) ±snf is a signed elementary sentence of the form +[ix.<P / u]afm for some constant description term ix.® and atomic formula afm: If +[ur.d>/ u]afm is atomic, +[u\d>/ u]afm e bse(Set)0 and this case reduces to case i). So we may assume that u occurs free in afm. There are two subcases: a) Set* contains the signed sentence +(JC)(V)((<2> A [ V / x]®) —> x = v) for some variable v. Since +[xx.®/ u]afm e bse(Set)fl and (bse(Set)^) is well ordered under Q, there is a least ordinal /3, 0 < (3 < fi, such that +[\x.® I u]afm e bse(Set)p . So, since +[ix.® I u]afm e bse(Set)p for /3 > 0, but for all /< /?, +[ur.d> / u]afm g bse(Set)y , it follows from the fact that +[\x.®/ u]afm is a signed elementary sentence (and as such cannot be the output of an instance of any semantic rule other than 1.3.2.5.) that +[ix.®/ u]afm e Sc(bse(Set)p_t) by virtue of an instance I of the semantic rule for descriptions 1.3.2.5.. Hence bse(Set)contains the 91 uniqueness presupposition +(x)(z)((CP A [zl X ] C P ) —» x = z) to I for some variable z. Now it is clear that by semantic rule 1.3.2.4., if bse(Set)p_j contains the signed sentence +(x)(z)((<2> A [z / x]<P) —> x = z) for some variable z, then bseiSet)^ contains the signed sentence +(x)(z)((d> A [z / x ]CP) —> x = z) for all variables z. So Set* n bse(Set)p_t contains the signed sentence +(x)(v)((d> A [v / x]<P) -> x = v) for some variable v. But since p < fi, P- 1< fx. So there is a fi < fx such that Set* n bse(Set)p * 0 . Contradiction. b) For no variable v does Set* contain the signed sentence +(x)(v)((CP A [ V / x]d» —» x = v). Since +[ix.<Z>/ u]afm e Stef* and, by lemma 4.2.4.1., Set* is downward closed, by condition 9) of 4.1.1., Set* contains the signed sentence +[/ / x](<P A [X I u]afm) = +([t I x]<P A [t I u]afm) for every f e (Set*)). Then by condition 6) of 4.1.1., for every t e Si^iSet*)), Set* contains one of the signed sentences +[t I x]<X>, +[t I u]afm. Since +[uc.<P/ u]afm e Set* and u occurs free in afm and for no variable v does Set* contain the signed sentence +(x)(v)((d> A [ V / x]d>) -> x = v), it follows by lemma 4.2.4.3. that SCS^ C&er*)) = Far. So, for every / e h(Par), Set* contains one of the signed sentences +[t I x]d>, +[t I u]afm. Since +[ix.4>/ u]afm e bseiSet) and (bse(Set) ) is well ordered under Q, there is a least ordinal p, 0 <p< ju, such that +[ix.d>/ u]afm e bse(Set)p . So, since +[ix.<P/ u]afm e bse(Set)p but for all y< /3, +[tx.<P/ u]afm g bse(Set)y, it follows from the fact that +[ix.<P/ u]afm is a signed elementary sentence (and as such cannot be the output of an instance of any semantic rule other than 1.3.2.5.) that +[ix.<P /u]afm e Sc(bse(Set)p_j) by virtue of an instance I of the semantic rule for descriptions 1.3.2.5.. Hence bse(Set)p_t contains the existence presupposition +[s / x]d> as well as the major statement +[s I u]afm to I for some constant, possibly nonbasic, term s. In case 5 is not in 5(Par), by lemma 1.3.10., there is a descriptum ts for s in bse(Set) such that both of +[ts I x]0, +[ts I u\afm are in bse(Set)p_j. So bse(Set)p_l contains both of +[s / x]d>, +[s I u]afm for somes e 8(Par). So, since for every t e 8(Par), Set* contains one of the signed sentences +[t I x]d>, +[/ / u]afm and there is an s e 8(Par) such that bse(Set)p_1 contains both of +[s I x]<P, +[s I u]afm, it follows that there is an s e b(Par) such that Set* n bse^Sefio, contains one of +[s I x]<p, +[s I u]afm. But since P < Li, P - 1< 92 fi. So there is a /3 < such that Set* n bseiSet) p * 0 . Contradiction. 6) ±5/1/ is a signed elementary sentence of the form -[ix.® / u]afm for some constant description term ix.d> and atomic formula afm: If -[ix.® / u]afm is atomic, -[tx.3>/ u]afm e bse(Sei)0 and this case reduces to case i). So we may assume that u occurs free in afm. There are two subcases: a) Set* contains the signed sentence +(x)(v)((d> A [ V / x]®) —> x = v) for some variable v. Since -[ix.® I u]afm e bseiSet) and (bseiSet) ) is well ordered under <=, there is a least ordinal /3, 0 < /3 < /x, such that -[ix.® I u]afm e bseiSet) p . So, since -[tx.d> / u]afm e bseiSet)p for /3> 0, but for all y< /3, -[xx.®l u\afm <£ bse(Set)y, it follows from the fact that -[\x.® I u]afm is a signed elementary sentence that -[ix.® / u]afm e Sc(bse(Sef)p_j) by virtue of an instance I of the semantic rule for descriptions 1.3.2.5.. Hence bse(Set)p_j contains the uniqueness presupposition +(x)(z)((d> A [ Z / x]®) —> x = z) to I for some variable z. Now it is clear that by semantic rule 1.3.2.4., if bse(Set)p_1 contains the signed sentence +(x)(z)((d> A [ Z / x]®) —> x = z) for some variable z, then bse(Set)p_j contains the signed sentence +(x)(z)((<P A [z / x]®) —> x = z) for all variables z. So Set* n bse(Set)p_1 contains the signed sentence +{x)(v)((® A [v / x\®) -» x = v) for some variable v. But since /3 < fi, - 1< fi. So there is a P < ^ such that Set* n bseiSet)p ^ 0 . Contradiction. b) For no variable v does Set* contain the signed sentence +(x)(v)((d> A [v / x]d>) —> x = v). Since -[ix.® / u]afm e Set* and, by lemma 4.2.4.1., Set* is downward closed, by condition 9) of 4.1.1., Set* contains the signed sentence +[//x](d> A —\x I u]afm) = +([f/x]d> A u]afm) for every / e bi^3 iSet*)). Then by condition 6) of 4.1.1., for every te Si^iSet*)), Set* contains one of the signed sentences +[t / x]®,+—>[t / u]afm. Since +[tx.d> / u]afm e Set* and u occurs free in afm and for no variable v does Set* contain the signed sentence +(x)(v)((d> A [ v / x ] d » —> x = v), it follows by lemma 4.2.4.3. that 8(^s(5er*)) = Par. So, for every t e 8(Par), Set* contains one of the signed sentences +[/ / x]d>, H—\tl u]afm. If Set* contains the signed sentence +—\tl u]afm, then by condition 5) of 93 4.1.1., Set* contains the signed sentence -[tl u]afm. So, for every re 8(Par), Set* contains one of the signed sentences +[/ / x]&, -[t I u]afm. Since +[ix. CP / u]afm e bse(Set) and (bse(Set) ) is well ordered under Q, there is a least ordinal /3,0 <fi< fi, such that -[ur.CP/ u]afm e bse(Set)p . So, since +[ut.CP / w]a/m e bse(Set)pfor f3> 0, but for all y< /J, -[ur.CP/ u]a//n g bse(Set)y, it follows from the fact that -[ur.CP / u]afm is a signed elementary sentence that -[ix.0 lu]afm e Sc(bse(Set)p_1) by virtue of an instance I of the semantic rule for descriptions 1.3.2.5.. Hence bse(Set)p_t contains the existence presupposition +[s / JC]CP as well as the major statement -[s I u]afm to I for some constant, possibly nonbasic, term s. In case s is not in d(Par), by lemma 1.3.10., there is a descriptum ts for s in bse(Set) such that both of +[t$ I JC]CP , -[tg I u]afm are in bse(Set)p_j. So bse(Set)p_j contains both of +[s Ix\&, -[s I u]afm for somes e 6(Par). So, since for every t e b~(Par), Set* contains one of the signed sentences +[t I x]CP, -[t I u]afm and there is an s e 8(Par) such that bse(Set)p_{ contains both of +[s I x]CP, -[s I u]afm, it follows that there is an s e 8(Par) such that Set* n bse(Set)p_j contains one of +[s I JC]CP, -[s I u]afm. But since p<fj,fi-l<Li. So there is a p< fi such that Set* n bse(Set)p*0. Contradiction. In all cases, then, the assumption that there is an ordinal fl such that Set* n bse(Set) * 0 leads to a contradiction. Hence, for all LL, Set* n bseQSet) = 0 . Then it follows by the fact that, by definition, Cl(bse(Set)) = U bse(Set)^ ,0<LI <&Q , that Set* n Cl(bse(Set)) = 0 . • Lemma 4.2.4., the claim that every downward closed set Set of signed sentences determines a base bseiSet) such that Sef n Cl(bse(Set)) = 0 , now follows from lemmata 4.2.4.1., 4.2.4.4., 4.2.4.5. established above: Let Set be any downward closed set of signed sentences. Then by 4.2.4.1., Set has a downward closed extension Set*. By lemma 4.2.4.4., there exists a base bse(Set), which, by lemma 4.2.4.5., is such that Set* n Cl(bse(Set)) = 0 . Since Set ^ &?r*, it follows that Set n Cl(bse(Set)) = 0 . • Theorem 4.2.2., the claim that every valid sequent is strictly 2-derivable, now follows from lemmata 4.2.3. and 4.2.4. Hence, lemma 4.2.1. and the completeness of Pld has been established. 94 • 95 Section 5: Corollaries to Soundness and Completeness. In this section we state and prove some normal form results concerning Pld derivations which fall out of theorems 2.1. and 4.2.2. and then give a characterization of the set of sentences of Pld for which excluded middle holds. Corallary 5.2 (Normal Form Lemma): Every derivable sequent is strictly derivable. Proof of 5.2: Let Seq be any derivable sequent. Then, by soundness theorem 2.1., Seq is valid. Then by lemma 4.2.2., Seq is strictly 2-derivable. So by lemma 3.5., Seq is strictly derivable. • Corollary 5.3: Every derivable sequent can be derived as endsequent of a derivation tree containing no application of the cut rule 1.2.2.8.. Proof of 5.3: By corollary 5.2. and definition of strictly derivable. • Corollary 5.4: Every derivable sequent can be derived as endsequent of a derivation tree all of whose applications of the description rule 1.2.2.6. have elementary output sentences. Proof of 5.4: By corollary 5.2. and definition of strictly derivable. • Notice that corollary 5.3. allows us to give a proof of the syntactic consistency of Pld that is an alternative to the proof given in section 2. We restate and reprove the syntactic consistency of Pld: Corollary (Syntactic Consistency): For no sentence snt are both of {+snt}, {-snt} derivable sequents. Proof: Assume there is a sentence snt such that both of {+snt}, {-snt} are derivable. Since the null sequent can be derived by appending an application of the cut rule 1.2.2.8. to the derivations 96 of {+snt}, [snt}, it follows that the null sequent is derivable. Then by corollary 5.3., the null sequent is derivable as endsequent of a derivation tree containing no applications of 1.2.2.8. But since all Pld axioms are non-null sequents and every Pld deduction rule R except for 1.2.2.8. is such that if all of an applications of R's premises are non-null then that applications conclusion is non-null, it follows by a simple induction on the depth of derivation trees that the null sequent is not derivable without application of 1.2.2.8.. Contradiction • We say that excluded middle holds for a sentence snt of Pld iff for all bases bse, one of ±snt belongs to Clibse). Then, it follows from soundness and completeness by definition 1.2.5. that the set of sentences of Pld for which excluded middle holds is precisely the set Grd of grounded sentences. Since Grd is r.e., we have an r.e. characterization of set of sentences of Pld for which excluded middle holds. 97 Section 6: Some Remarks on the Frege-Strawson Doctrine. The "Frege-Strawson doctrine" (F-S D) has thus far been characterized as the claim that a sentence of a natural language that is grammatically of subject-predicate form and that contains a vacuous singular subject term cannot have a (classical) truth value associated with it. We have suggested that Pld formalizes the semantic intuition behind F-S D as applied to improper definite description in terms of a theory of truth which allows truth value gaps. In this section we evaluate the extent to which Pld can be said to be a formalization of the F-S D and then consider the problem of integrating F-S D with a general theory of truth for compound sentences of natural language. Indeed, we find that Pld suggests a natural such extension of the F-S D. A definite description of English can be informally characterized as a noun phrase of the form ftheO 1 where 'O' is an English noun phrase, qualified or unqualified, in the singular. A proper definite description of English can be informally characterized as a definite description of the form rthe ^ such that there is exactly one <£. The formal analog to an English definite description within Pld syntax is, of course, the description term. Let us say that a Pld constant description term of the form uc. CP is proper relative to a base bse iff for some constant term / and variable v, Cl(bse) contains both of the signed sentences +[t I JC]CP, +(x)(v)((CP A [ V / x]CP) —> x - v). We say that ix.& is improper relative to a base bse iff uc.cP is not proper relative to a bse. When we consider that the formal analog within predicate logic to a singular subject-predicate sentence of natural language is the atomic (or, in the terminology of Pld, the 'elementary') symbolic sentence, that is, a sentence consisting of an /i-ary predicate letter followed by /i-many singular terms, it is easy to see that Pld offers a precise formalization of the F-S D as applied to definite descriptions. For, if A is an elementary sentence, then A lacks a truth value relative to a model bse if and only if A contains a description terms that is improper relative to bse, as we now show: Theorem 6: Let bse be any base, A any elementary sentence. Then, one of ± A belongs to Clibse) 98 iff every constant description term ix.® occurring in A is proper relative to bse. Proof of 6.: => Assume that ± A belongs to Cl(bse). Let ix. ® be any constant description term occurring in A; we may assume that there is one, since otherwise it is trivially the case that every constant description term ix.® occurring in A is proper relative to bse. So A is of the form [ix.® / u]F for some elementary formula F containing free occurrence of a variable u. Then, since ±[u\d>/ u]F belongs to Clibse) andClibse) = KJbse^ ,0<fi<e0, there is a li<EQ such that ±[u*.d> / u]F belongs to bse . Let respectively<P',F' be the result of uniformily replacing every occurrence in respectively ®,F of any constant description term t z - f £ ix.® occurring in [ix.® I u]F by a descriptum t^if/e BiPar) for u - f i n bse whose existence is guaranteed by lemma 1.3.10.. By lemma 1.3.10., respectively ±[ix.®'/ u]F' belongs to bse^ . Since bse^ = KJbsep, 0 < < fj., and (bse^) is well ordered under there is a least P < ji such that ±[\x.®' I u]F' belongs to bsep . Since [ix.®' I u]F' is not atomic, P * 0. Clearly, then, p is a successor ordinal. So bsep = bsep_} u Scibsep_l). Then ±[xx.®' I u]F' belongs to Scibsep) by virtue an instance I of some semantic rule. Since [ix.®' I u]F' is an elementary sentence, I is an instance of the semantic rule for descriptions 1.3.2.5. Since ix.® is the only constant description term occurring in [ix.®' I u]F' , there are presuppositions to I of the form +[/ / x]®, +(ac)(v)((d> A [v / x]®) —> x = v) for some constant term t and variable v. Hence, there are constant term / and variable v such that bsep_t Q Clibse) contains both of the signed sentences +[t I x]®, +(x)(v)((<P A [v / x]®) —> x = v). So \x.® is proper relative to bse. <= Assume that every constant description term ix.® occurring in A is proper relative to bse. We show that one of ±A belongs to Clibse) by induction on the number #(A) of description terms occurring in A. Base step: #(A) = 0. Since A contains no description terms, A is a sentence of classical logic. Now it is easy to show that for all sentences B, if B contains no occurrence of any description term, then the sequent {-B , +B} is derivable, by induction on the syntactic complexity (defined in the usual way for sentences of classical logic) of B; indeed this is precisely the proof of the 99 redundancy of Gentzen's original set of axioms containing the sequent S —> S for every sentence S of first order classical logic. So, by semantic completeness, {-A , +A} n Clibse) * 0. Hence, one of ±A belongs to Clibse). Induction step: #(A) > 0. Assume that one of ±B belongs to Clibse) for all sentences B of Pld such that #(B) < #(A). Let \x.0 be any constant description term occurring in A; since #(A) > 0 we know there is one. So A is of the form [ix. 0 I u]F for some elementary formula F containing free occurrence of a variable u. Since one of ±[ur.d> / u]F belongs to Cl(bse) andCl{bse) = KJbse^ ,0<Li<e0, there is a H<€Q such that ±[ix.0/ u]F belongs to bse^. Then by lemma 1.3.10., there is a descriptum t^x @ e b~{Par) for ur.CP in bse such that respectively ± [ ^ d> I u^ belongs to bse^ . Clearly, #([1^ 1 u]F) < #(A). So by the hypothesis of induction, one of, not respectively, ±[tlx0/u]F belongs to Cl(bse). By assumption uc.<P is proper relative to bse, so there are constant term t and variable v such that Clibse) contains both of the signed sentences +[t I x]0, +(x)(v)((<3> A [ V / x]0) —» x = v). Then Cl{bse) contains both of +[t I x ] C P , +{x){v){{<X> A [ V / x]0) -» x = v) and one of ±[*u:.d> / u]F. Then by lemma 1.3.11., Cl{bse) contains one of ±[xx.0/u]F. So the claim holds. • As explained in the introductory section 0, the F - S D, as a doctrine concerning the primitive linguistic operations of reference and predication, is prima facie plausible to one who holds what we have called the "naive" view of the semantics of grammatically singular subject-predicate sentences. However, when we consider the difficulty of formulating a compositional semantic theory for sentences of natural language that satisfies the F-S D, that doctrine loses much of its initial attractiveness. For, if the semantic value of grammatically compound sentences is determined by the semantic value of its syntactic constituents, in particular, if the truth value of a compound sentence is a function of those of its subsentences, then every sentence is such that its truth evaluation depends ultimately on the truth evaluation of subject-predicate sentences. So, on any compositional semantic theory, the F-S D has ramifications for the evaluation of all types of sentences of natural language. In particular, a compositional semantic theory for natural language that satisfies the F-S D 100 must decide how the "undefinedness" of a subsentence of a given compound sentence effects the truth value the given sentence. Now, the simple-minded solution of straight forwardly generalizing the F-S D to all sentences of natural language, so that (on this generalized view) any sentence that contains a vacuous sigular term must lack a truth value, has obvious counter-intuitive consequences. For on this generalization of the F-S D, the English sentence 'Either grass is green or the present king of France is bald.' lacks a truth value. But clearly this consequence (of the generalized F-S D) threatens the monotonicity of many intuitively monotonic natural language inferences, since from the truth of a sentence S we may infer the truth of the sentence or p\ where P is any English sentence. More poignant examples of counter-intuitive consequences of the generalized F-S D can be found: Let S be any English sentence containing no occurrence of a vacuous singular term. Then, the English sentence ^ Either S or not-S or the present king of France is baldJ, though seemingly a logical truth, lacks a truth value on this view. So does the the following English sentence which may be considered axiomatic of the Russellian Theory of Descriptions: 'If there is exactly one present King of France and he is bald, then the present king of France is bald'. So there is a class of intuitively true (false) English sentences containing improper definite descriptions that present (at least prima facie) counterexamples to the acceptablity of the simple-minded generalization of the F-S D. Now, it is reasonable to require of any acceptable (compositional) semantic theory for natural language that satisfies the F-S D that it respect our intuitions concerning the truth value of the sentences in this "target" class. And certainly this requirement is all the more pressing on semantic theories for artificial logical languages designed to formalize the intuitive logical relationships holding between sentences of natural language. Then it is a virtue of Pld that it does respect the truth value of (the symbolic sentences corresponding to) the sentence in this class, as we now show. We may characterize the target class of intuitively true (or false) English sentences containing improper definite descriptions whose truth value we are interested in preserving as being the union of the following three classes: 1) the class of English sentences whose truth (falsehood) seems to be guaranteed by the truth (falsehood) of their contingently true (false) subsentences, 2) the class of 101 English sentences S whose truth (falsehood) seems to be guaranteed by the (logical) truth (falsehood) of subsentences of S that correspond to theorems of the first order identity calculus without descriptions, and 3) the class of English sentences that correspond to theorems of a Russellian first order description calculus (which are not theorems of the conservative extension of first order identity calculus obtained by adding description terms to the elementary syntax of that theory). The English sentence 'Either grass is green or the present king of France is bald.1 is a representative of the class of English sentences containing improper definite descriptions whose truth seems to be guaranteed by the truth of their contingently true subsentences. Now, the formal analog to the notion of the contingent truth of an English sentence is the defined notion of "truth (validity)-relative-to a-base" of a symbolic sentence of Pld. Clearly, the unrestricted monotonicity of the semantic rules 1.3.2.2., 1.3.2.3 governing the binary sentential connective of Pld insures that if A is true relative to a given base bse, then so is (the unabreviated form of) the sentence A v B where B is any symbolic sentence, in particular, one that contains a constant description term that is improper relative to bse. The English sentence, ^ Either S or not-S or the present king of France is b a l d J , where S is any English sentence containing no occurrence of a vacuous singular term, is a representative the class of logically true English sentences containing improper definite descriptions whose truth seems to be guaranteed by the truth of their logically true subsentences. The formal analog within Pld of the intuitive notion of the logical truth of an English sentence is, of course, the defined notion of validity, or truth relative to all bases, of a symbolic sentence. Again, relative to a base bse, the formal analog within Pld of the notion of a vacuous singular term of English is the defined notion of a description term that is improper relative to bse. Now, it is easily shown (by an argument similar to the proof of lemma 6 from right to left) that, for any base bse, if A is a sentence of Pld in which the only occurring description terms are proper relative to bse, then (the unabreviated form of) the sentence A v —A is true relative to bse. Hence, it follows that the sentence (A v —iA) v B is true relative to bse for every sentence B. So we can say that if A is a sentence of Pld in which the only occurring description terms are proper relative to all bases bse, 102 then (A v -iA) v B is a logical truth of Pld, even if B contains an description term that is improper to some or all bases. At this point one might object that since we have argued for the acceptability of Pld as a formal semantic theory satisfying the F-S D on the grounds that Pld insures the truth (falsehood) of symbolic sentences that correspond to intuitively true English sentences, we should bite the bullet and admit that the failure of excluded middle in Pld is a failure of Pld, period, since most people accept l~S or not-S^, for any sentence S, as a logical truth of English. However, one would here be objecting to the F-S D itself, rather than our particular formalization of it, since it is the basic intuition behind the F-S D that English sentences of the form or not-S^ are not, in general, logically true. The English sentence, 'If there is exactly one present king of France and he is bald, then the present king of France is bald', is a representative the class of intuitively true English sentences that correspond to theorems of a Russellian first order description calculus that are not theorems of the first order identity calculus (nor may be obtained from such theorems by the uniform weak substitution of description terms for terms of the first order identity calculus). Now, it is not the case that all symbolic sentences of Pld of the form (3x)0fy)((® B J I = I ) A F ) - ) [u\d>/ x]F are valid for arbitirary formulas ®, F, since sequents of the form {-[tlx]®, -(x)(v)((® A [v / x]®) —»x = v), -[t I u]F , +[\x.® I u]F} are not in general valid for arbitirary formulas ®, F. However, if we restrict ® and F so that all of the signed sentences [t I x]®, (x)(v)((® A [v I x]®) -> x = v), [t I u]F are grounded, equivalently, obey excluded middle, then it is trivially the case that, by the semantic rule for descriptions 1.3.2.5., {-[t I x]®, -(x)(v)((® A [v / x]®) —»x = v) , -[tl u]F , +[ix.®l u]F} is a valid sequent. So, for every base bse, if neither of ®, Fcontain description terms that are improper relative to bse, then the sequent {-[tlx]®, -(x)(v)((® A [v / x]®) -» x = v) , -[tl u]F , +[ix.® I u]F) is valid relative to bse. In particular, if neither of ®, F contain any description terms, the sequent in question is valid. So, if we construe the English predicates 'x is a present King of France', 'x is bald' as primitive, that is, corresponding to predicate letters of Pld, then the symbolic sentence of Pld corresponding to the English 'If there is exactly one present king of France and he is bald, then the present king of 103 France is bald' is valid. We should note that sequents of the form [-[t I x]&, -(x)(v)((CP A [ V / x]0) -> x = v), -[t I u]F , +[ix.<P/ u]F}, where all of the signed sentences [tI x]0, ( X ) ( V)((C P A [v I x]&) -> x = v), [t I u]F are grounded but neither of [t I x]0, (x)(v ) ( ( C P A [v / x]0) -> x = v) are valid/derivable, are examples of sequents that are valid relative to the semantics of Pld, but that are not derivable within a Pld version of logical syntax suggested for descriptions in Gilmore [3]. This is because the rule for descriptions given in [3] require the "presuppositions" to the application of the rule to be themselves derivable, rather than merely members of a derivable sequent. A simplified version of the rule given in [3], modified in the manner of Pld, is as follows: {+[tlx]0} { + ( X ) ( V ) ( ( < P A [V/X]0) - » JC= v)} SeqKj {±[t/u]F} SeqKj {±[\x.0/u]F} It is clear that a logical syntax L§ treating description terms with this rule only allows a sequent of the form Seq u {±[uc.<P / u]F] to be derivable only if either there are term / and variable v such that both of the signed sentences +[t I x]<P, +(x)(v)((d> A [v / JC]CP) —> x = v) are derivable or Seq is itself derivable (in which case ±[ur.CP / u]F is obtained in the derivation of Seq u [±[ur.4>/ u]F] by thinning). Now, consider a sequent Seq = {-[t /x]&, -(x)(v)((CP A [v / x]0) -> x = v) , -[tl u]F , +[ur .CP/ u]F}, where all of the signed sentences [tl JC]CP, (x)(v)((CP A [v / x ]CP) - > x = v), [/ / u]F are grounded but neither of [t I x ]CP, (x)(v)((CP A [v / x ]CP) - > x = v) are derivable, which is such that [ -[/ / x] C P, -(x)(v)((<P A [ V / x]CP) - » x = v), -[t I u]F} is not a derivable sequent. Clearly such a sequent exists. Since neither of [t I x]<P, (x)(v)((<2> A [V I x}0) -> x = v) are derivable sentences and {-[t I x]0, -(x)(v)((CP A [ V / x]0) -> x = v), -[/ / u]F] is not a derivable sequent, it follows that Seq is not derivable in LS. But, since all of the signed sentences [//x]0, (x)(v)((d>A [v /x]0) -> x = v), [tl u]F are grounded, Seq is valid in Pld. 104 Bibliography Carnap, R. [1] Meaning and Necessity, Chicago, 1947 Frege, G. [1] Uber Sinn und Bedeutung, Zeitschriftfur Philosophie und Kritik, vol. 100 (1892), pp. 25 - 50. English translation in Translations from the Philisophical Writings ofGottlob Frege, edited by Geach and Black, Oxford, 1960. [2] Grundegesetze der Arithmetik, vol. 1, Jena, 1893. English translation in The Basic Laws of Arithmetic, translated and edited with an introduction by M.Furth, Berkeley and Los Angeles, 1964. Gilmore, P.C. [1] Combining Unrestricted Abstraction with Universal Quantification, To H. B. Curry: Essays on Combinatorial Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hendley (eds.), Academic Press, i980, pp. 99 - 124. [2] Natural Deduction Based Set Theories: A New Resolution of the Old Paradoxes, Journal of Symbolic Logic, June 1986. Hilbert, D., and Bernays, P. [1] Grundlagen der Mathematik, vol. 1, Berlin, 1934. Kalish, D., Montague, R., Mar, G., [ 1] Logic: Techniques of Formal Reasoning, New York, 1980. Quine, W.V. [1] Mathematical Logic, New York, 1940. Russell, B. [1] On Denoting, Mind, vol. 14 (1905), pp. 479 - 93. 105 Strawson [1] On Referring, Mind, vol. 59 (1950), pp. 320 - 344. Whitehead, A. N., and Russell, B. [1] Principia Mathematica, vol. 1, London, 1910; 2nd edition, 1925.
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- A partial logic of descriptions
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
A partial logic of descriptions Apostoli, Peter J. 1986
pdf
Page Metadata
Item Metadata
Title | A partial logic of descriptions |
Creator |
Apostoli, Peter J. |
Publisher | University of British Columbia |
Date Issued | 1986 |
Description | Let a "partial logic" for a first order predicate language L be a formal proof-theory PT for sentences of L together with a model theoretic semantics for PT which can be considered a generalization of classical first-order Tarskian semantics in the following sense: if M is a model for PT then M is a partial function from the set of sentences of L into the set {T, F} of classical truth values such that 1) every atomic sentence of L receives exactly one truth value, and 2) if M agrees with a given Tarskian model TM on the assignment of truth values to the atomic sentences of L, then M agrees with TM everywhere M is defined. In this paper we utilize formal techniques developed by P. C. Gilmore for intensional set theories without excluded middle to present a sound and complete partial logic Pld for the first order predicate calculus with definite descriptions. Pld utilizes truth value gaps to systematically treat symbolic sentences that contain "improper" description terms, and can be seen as an acceptable formalization of the Strawsonian view that the semantic-well-formedness of a grammatically subject-predicate sentence of English presupposes the propriety of any definite description occurring as subject term therein. |
Genre |
Thesis/Dissertation |
Type |
Text |
Language | eng |
Date Available | 2010-07-12 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
DOI | 10.14288/1.0096940 |
URI | http://hdl.handle.net/2429/26358 |
Degree |
Master of Arts - MA |
Program |
Philosophy |
Affiliation |
Arts, Faculty of Philosophy, Department of |
Degree Grantor | University of British Columbia |
Campus |
UBCV |
Scholarly Level | Graduate |
AggregatedSourceRepository | DSpace |
Download
- Media
- 831-UBC_1986_A8 A66.pdf [ 6.26MB ]
- Metadata
- JSON: 831-1.0096940.json
- JSON-LD: 831-1.0096940-ld.json
- RDF/XML (Pretty): 831-1.0096940-rdf.xml
- RDF/JSON: 831-1.0096940-rdf.json
- Turtle: 831-1.0096940-turtle.txt
- N-Triples: 831-1.0096940-rdf-ntriples.txt
- Original Record: 831-1.0096940-source.json
- Full Text
- 831-1.0096940-fulltext.txt
- Citation
- 831-1.0096940.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0096940/manifest