Bar-Recursive Interpretation of Second-Order Arithmetic

Definitions and mathematical statement

In the customary proof-theoretic reading, full second-order arithmetic $Z_2$ is the classical two-sorted theory of natural numbers and sets of natural numbers, with arithmetic and induction and the full comprehension scheme \[ \exists X\ \forall n\left(n\in X\leftrightarrow\varphi(n)\right), \] for formulas $\varphi$ of the two-sorted language, allowing set quantifiers and parameters, with $X$ not free in $\varphi$. This refers to an axiom system, not an assertion that a first-order proof calculus captures all full-semantic second-order truths.

The source's conjecture is that the particular uniform functional interpretation described in the report can be extended, via bar recursion, to full second-order arithmetic. The requested extension must cover the full comprehension instances, rather than just a fixed restricted subsystem, and must extend that interpretation rather than provide an unrelated interpretation.

To give a precise soundness theorem one would need the report's formula translation, interpretation of assumptions and conclusions, target typed functional calculus, variant and type levels of bar recursion, and meaning of uniformity. For a proof-to-realizer reading, uniformity would concern one systematic construction for proofs, with realizers satisfying the translated conclusions in the specified target theory. This is an explanatory reading only: the source does not provide those rules or identify which added bar-recursive principles are permitted. No unrestricted proof-extraction theorem is asserted without them, and no particular bar-recursion schema or choice principle is invented.

Short English statement

Can the report's uniform functional interpretation be extended by bar recursion to all of second-order arithmetic, including unrestricted comprehension? The specific interpretation, recursion principles, and target soundness statement are not reproduced.

Sources

• Local UnsolvedMath registry, permanent ID $30000945$, source code catalogue entry, "Bar-Recursive Interpretation of Second-Order Arithmetic." No individual proposer is supplied.
• Mathematical Logic: Proof Theory, Constructive Mathematics (2009), Oberwolfach Reports, DOI 10.4171/owr/2008/18, pp. 907--952, also listed as "Oberwolfach Report 18/2008": https://doi.org/10.4171/owr/2008/18.
• Supplied reference, "Blot, interpretation via bar recursion": https://arxiv.org/abs/1804.00731.
• Supplied literature triage, checked 2026-08-21: status "open." It reports bar-recursive interpretations for substantial fragments and extensions of second-order arithmetic, but no verified complete resolution of this particular conjectural extension. This dated assessment derives from supplied OWR curation; time-sensitive status and cited claims require independent verification.