appendix sectionnotation

First-order proofs

symbol	meaning	first
symbol	meaning	first
$Γ ⊢_{N} A$	intuitionistic natural-deduction judgment, extended to first-order formulas in chapter 3	chapter 2
$Γ \Rightarrow A$	one-conclusion LJ sequent	chapter 3
$\| A \|$	first-order formula rank	chapter 3
$G \Rightarrow_{S, E}^{m} A$	derived bounded-search judgment with branch eigenparameters $E$ and remaining logical height $m$	definition 3.35
$s ⟼ s^{'}$	one administrative transition between bounded-search states	definition 3.35