Mail to Webmasteralc9@math.nsc.ru
![[SBRAS]](http://www-sbras.nsc.ru/gif/s_sigma.gif)
Go to Home
Non-classical logics, proof theory and universal algebra
The significance of Gentzen systems and related axiomatizations by Gentzen rules is due in large part to the fact that various metatheoretical properties of Hilbert-style deductive systems can be formulated in terms of Gentzen systems.
We start off with the standard definition of a deductive system accepted in the field of algebraic logic
Definition An abstract Hilbert-style deductive system S is an algebraic invariant closure system over the set of formulas of a given propositional language. An element of such closure system is called a theory, and the qualification invariant means that a preimage of every theory under a substitution is a theory. The set of all theories for S we denote ThS. Obviously ThS forms a complete lattice.
It is easy to see that the closure operator, associated with such closure system, defines a finitary, substitutional consequence relation. Moreover, if we take any algebraic family of theories closed under arbitrary intersections, then it is also defines a finitary consequence relation, but not substitutional in general. To any such consequence relation we assign it constructive counterpart, by simply listing all finite sequences of formulas, called sequents, such that the last formula in a sequence is derivable from previous ones. We call such structure, according to tradition, a closure relation corresponding to a closure system. Thus we have a conceptual line: algebraic closure systems, then finitary consequence relations, and, finally, as constructivizations of the latter, closure relations.
It was suggested by researchers of Barcelona group (J.Font, R.Jansana, V.Verdu and others) to define an abstract Gentzen-style deductive system as an algebraic invariant closure system over the set of all sequents of the propositional language, where a substitution acts on a sequent component-wise. Thus a theory in the case of a Gentzen system is a set of sequents, so it is a closure relation, of sort.
There are several types of Gentzen-level structures, naturally associated with Hilbert systems. In general, they are short of being Gentzen systems, because one or several conditions of the definition fail. One, that has gotten the main attention so far, is the full closure relations related to closure systems of theories defined from semantical considerations. The case when they form a Gentzen system is connected somehow to algebraizability phenomenon, a conjunction-disjunction fragment of the classical propositional logic being here a paradigmatic example. We will turn however to a different kind of closure relations, ones that are defined rather syntactically.Definition An axiomatic closure relation for a Hilbert system S is a closure relation corresponding to a closure system of theories extending a given one. The latter is seen as a collection of axioms. Thus in whole this system forms a principal filter in the lattice of all theories for S. The set of all axiomatic closure relations for S we denote AcrS.
Main Theorem. A Hilbert-style deductive system S has a multi-term Deduction-Detachment theorem (DDT) iff AcrS forms an abstract Gentzen-style deductive system, i.e., it is
|
Mail to Webmaster alc9@math.nsc.ru |
|Home Page| |English Part| |
Go to Home |