is positive. The only freedom is over atoms are assigned a polarity freely. For negative formulas provability is invariant under the application of a right rule; and, dually, for a positive formulas provability is invariant under the application of a left rule. In either case one can safely apply rules in any order to hereditary sub-formulas of the same polarity. In the case of a right rule applied to a positive formula, or a left rule applied to a negative formula, one may result in invalid sequents e.g., in LK and LJ there is no proof of the sequent beginning with a right rule. A calculus admits the focusing principle if when an original reduct was provable then the hereditary reducts of the same polarity are also provable. That is, one can commit to focusing on decomposing a formula and its sub-formulas of the same polarity without loss of completeness. Focused system A sequent calculus is often shown to have the focusing property by working in a related calculus where polarity explicitly controls which rules apply. Proofs in such systems are in focused, unfocused, or neutral phases, where the first two are characterised by hereditary decomposition; and the latter by forcing a choice of focus. One of the most important operational behaviours a procedure can undergo is backtracking i.e., returning to an earlier stage in the computation where a choice was made. In focused systems for classical and Intuitionistic logic, the use of backtracking can be simulated by pseudo-contraction. Let and denote change of polarity, the former making a formula negative, and the latter positive; and call a formula with an arrow neutral. Recall that is positive, and consider the neutral polarized sequent , which is interpreted as the actual sequent . For neutral sequents such as this, the focused system forces on to make an explicit choice of which formula to focus on, denoted by . To perform a proof-search the best thing is to choose the left formula, since is positive, indeed (as discussed above) in some cases there are no proofs where the focus is on the right formula. To overcome this, some focused calculi create a backtracking point such that focusing on the right yields , which is still as . The second formula on the right can be removed only when the focused phase has finished, but if proof-search gets stuck before this happens the