Intuitionistic first-order proof theory

One intuitionistic first-order language with fixed-arity function and predicate symbols, $\mathrm{\perp },\wedge ,\vee ,\to ,\mathrm{\forall },\mathrm{\exists }$, capture-avoiding individual substitution, natural deduction, labeled proof terms, and single-conclusion LJ with explicit Cut, weakening, and contraction. Universal-right introduction and universal proof abstraction require the eigenvariable to be fresh for both the antecedent and the quantified conclusion formula. No equality predicate, induction axiom, multiple-conclusion LK, or focusing is present.

Individual substitution and proof substitution, the two ND–LJ translations, producer- and consumer-side commuting multicut reductions, cut elimination, the subformula property, and consistency are proved in chapter 3. The chapter defines every first-order compatible proof context and proves exact beta-normal-form grammar. Translation through cut elimination proves normal inhabitation of the same labeled judgment. It does not prove that the original proof term reduces to that inhabitant, so weak or strong proof-term normalization is not claimed.

The displayed search is terminating, sound, and complete only for analytic cut-free derivations within its finite term pool and height bound. Its eigenvariables are chosen fresh for the entire current sequent. This is not a decidability theorem for unrestricted first-order intuitionistic validity.

The Kappa companion in artifacts/ch03-first-order/ returns, prints, and independently checks proof trees for the Ax, implication, and universal search fragment. It verifies exact height, the negative bound range, right-to-left fallback, the two quantified-rule side conditions, alpha-normal cache reinstantiation, and a killed membership-only Ax-checker mutant. The runs are implementation evidence, not a mechanization of search completeness, cut elimination, or proof-term normal inhabitation.