Abstract

Logical implication is an attempt to catch the essence of causeeffect relationships of the real world in the context of formal deductive systems. The Deduction-Detachment Theorem being, in its turn, a statement about essential logical properties of classical implication, was therefore of great interest for logicians. Although a statement about a Hilbert-style deductive system, DDT can be formulated by means of Gentzen-style rules, and as such seems to be a statement about the metatheoretical properties of Hilbert-style deductive systems. As is often the case with metatheoretical properties, DDT leaves the question about its meaning and scope a bit vague or at least requires a higher order abstraction layer to formalize them. Closure relations, discussed in this paper, present a convenient context to give a precise formal statement of the DDT and its connection with Hilbert- and pertinent Gentzen-style deductive systems.