Multi-Page Printing

ALGEBRAIZABLE LOGICS 7 CnsTC | J CnsT' (9) finite P C T a(CnsT)C Cnscr(T) (10) for every substitution a. Conversely, any function from the power set of formu- las into itself satisfying conditions (6)-(10) gives rise in the obvious way to a deductive system (£,(-5). Consequently, S can be alternatively characterized as the pair (£, Cra$), and this is how deductive systems have traditionally been defined.4 Deductive systems in the form {C,Cn$) are called standard systems in Wqjcicki [48]. We shall consider exclusively standard systems in this paper, and will thus systematically omit the qualifying term. The set of all S -theories is denoted by ThS . ThS is closed under arbitrary intersection and hence forms a complete lattice ThS — (T/iS,n, V 5 ) . The largest theory is the set Fm of all formulas, and the smallest is the set of S- theorems (i.e., the formulas p such that \~s ip: where h$ p stands for 0 h5 (p.) V 5 denotes the (binary) join operation on ThS. For any two5-theories T, 5 we have T V 5 5 =f]{R G ThS :TUS C R}. Alternatively, T V 5 5 = C n 5 ( T u 5 ) so T \/s S is the theory generated by T U 5 . The infinitary join operation of T h 5 is denoted by \/ , as in the case of two theories, the join of an arbitrary set {T{ : i £ 1} of theories can be characterized as the theory generated by [JiejTi. Conversely, the consequence operator Cns, and hence also the consequence relation h $ , can be defined in terms of the lattice ThS. So we could also have characterized a deductive system as the pair (£,Th«S). The finitary character of the consequence relation Crts has important con- sequences for the structure of the theory lattice. An element of an arbitrary complete lattice is called compact if a \J X implies a V X' for some finite X1 C X. A lattice is algebraic if it is complete and every element is the (pos- sibly infinite) join of compact elements. A subset Y of a lattice is directed if every finite subset of Y has an upper bound in Y. The proof of the following lemma is straightforward and will be omitted. L e m m a 1.1 Let S — (£,h$ ) be an arbitrary deductive system. (i) The compact elements of ThS coincide with the finitely generated S- theories. (ii) ThS is closed under unions of directed sets. (I.e., for every directed set {Ti :ie 1} ofS-theories, \JieI T{ e ThS.) (hi) The lattice ThS is algebraic. I 4 The notion of deductive system characterized by conditions (6)-(9) (but not (10)) origi- nated with Tarski [42]. He gave it no particular name, but refers to a closely related notion in [43] as a theory. In both papers he uses the term deductive system to refer to what we call a theory below. Our interchanging of the two terms conforms to current usage in the literature.