appendix sectionnotation

Polarization and focusing

symbol	meaning	first
symbol	meaning	first
$P, Q$ / $N, M$	positive / negative polarized propositions	chapter 39
$↓ N, ↑ P$	shifts ending right / left focus	chapter 39
$P \otimes Q$	positive intuitionistic conjunction	chapter 39
$N & M$	negative intuitionistic conjunction	chapter 39
$P \Rightarrow N$	polarized implication	chapter 39
$Γ ⟹ A$	unfocused sequent; long arrow is punctuation	chapter 39
$Γ ⊢ [P]$	right-focus sequent	chapter 39
$Γ; Ω ⊢ U$	ordered-queue inversion sequent	chapter 39
$Γ; [N] ⊢ U$	left-focus sequent with stable succedent	chapter 39
$⟨ P ⟩, ⟨ N ⟩$	suspended positive hypothesis / negative succedent	chapter 39
$(-)^{\circ}$	named syntactic erasure of polarization, shifts, focus, and suspension	chapter 39
$cl (S), B (S)$	input subformula closure / queue-size bound	chapter 39
$C (S), X_{n}$	finite candidate space / saturation stage	chapter 39