sequent may remove the focused component thereby returning to the choice e.g., must be taken to as no other reductive inference can be made. This is a pseudo-contraction since it has the syntactic form of a contraction on the right, but the actual formula doesn't exist i.e., in the interpretation of the proof in the focused system the sequent has only one formula on the right. References Logic Proof theory Reductionism Logic programming