Polarized propositional intuitionistic focusing

The calculus ${\mathcal{F}}_{\mathsf{IPL}}$ of chapter 39 has the polarized propositional grammar of appendix A, three sequent forms, finite-set persistent contexts, and ordered inversion queues. It has no quantifiers, equality, recursion, linear resources, or dependent types.

De-focalization is theorem 39.13; focal substitution, four cuts, and both identity expansions are lemma 39.14, theorem 39.15; structural rules and ordinary invertibility are lemma 39.10, lemma 39.2; structural focalization is theorem 39.19. No result depends on an exercise case.

The total-size bound includes every legal input and intermediate queue. The candidate space is finite and rule closed by lemma 39.22; least-fixed-point search is exact and terminating by theorem 39.23. The chapter gives an explicit exponential candidate-table bound, while memoized reachable-graph search is exact and terminating by corollary 39.24.

Simmons’s archived propositional intuitionistic source supplies Figures 3–7 and Theorems 1–4. Andreoli’s original paper is present on the shelf as a scan and is the primary bibliographic origin of focusing; the chapter imports no theorem from it. Linear focusing and polarized CBPV are outside this signature.

The pinned Kappa rule graph recorded in appendix E checks phase, choice, cycle, and negative cases. Its duplicate-free list representation compares persistent contexts by finite-set equality. It proves none of the metatheorems above.