We begin our analysis of contractions in S(K) by introducing additional terminology. We call contraction constituents the active formulas of an application of a contraction rule, and define the rank of a contraction of x:A, in symbols rank(x:A), to be the largest number of steps immediately preceding the conclusion of the contraction and containing at least one of the contraction constituents. Since we can always transform a backwards proof so that a contraction of x:A immediately precedes the step introducing the second constituent, the rank measures how many steps stand between the introduction of the first and second constituent (so that the minimum possible rank of a contraction is 2).
KeywordsLogical Rule Block Form Relational Reasoning Propositional Classical Logic Disjunction Property
Unable to display preview. Download preview PDF.