6
W. J. BLOK AND D. PIGOZZI
In addition h$ is finitary in the sense
T\-s f = r h
5
if for some finite V C I\ (4)
and it is structural in the sense
T\-s p^ cr(T)hs crp (5)
for every substitution a. Conversely, Los and Suszko [25] have shown that
every relation satisfying conditions (l)-(5) is the consequence relation for some
deductive system S. Consequently, in the sequel by a deductive system we will
mean a pair (C,\~s) where \~s is a function from the powerset of Fmc into
Fmc that satisfies conditions (2)-(6); defining axioms and rules of inference
are not assumed.
Associated with any deductive system are its various extensions, subsys-
tems, and fragments. By an extension of a deductive system S over the lan-
guage C we mean any system S'
(C^s1)
over the same language such that
r H$ V ? = r h$/ (f for all T U } C Fmc] S is called a subsystem of S' in
this case. S' is an axiomatic extension of S if it is obtained by adjoining new
axioms but leaving the rules of inference fixed.
Let C be a sublanguage of £, and let \-& be the restriction of (-$ to C in
the sense that T \~s ^ iff T U {^} C Fm& and r h$ y. It is easy to see that
conditions (l)-(5) continue to hold with h$/ in place of h$, and hence that
5
;
= (£',1-5') is a deductive system over C. S' is called the C-fragment of 5 .
1.1 The Lattice of Theories
Let S be an arbitrary deductive system. A set T of formulas is called a theory
of S (a S-theory for short) if T h$ y? implies / ? £ T for every p £ Fm, or,
equivalently, if T contains all substitution instances of the axioms, and is closed
under the inference rules. For any T C Fm we take
CnsT = {pe Fm:T\-s p}.
CnsT is the smallest 5-theory including T, and T is said to generate CnsT.
Cns , treated as a function on the power set of Fm, is called the consequence op-
eratorofS (the S-consequence operator). The characteristic properties (l)-(5)
of the consequence relation h$ correspond to the following closure properties
of Cns:
rccn
5
r
;
(6)
r c A ^ CnsTC CnsA] (7)
CnsCnsTC CnsT] (8)
Previous Page Next Page