Dynamic Induction for Strictly Positive Definitions

Definitions and mathematical statement

The supplied question concerns dynamic induction for inductively defined predicates. To display its known special case, write $D$ for the underlying domain, $<$ for the relation used in the definition, and $B(x)$ for the base predicate. These are placeholders: the supplied record specifies neither the domain nor hypotheses on the relation or base predicate. The displayed defining clause is \[ I(x)\leftrightarrow B(x)\lor\exists y\,(y<x\land I(y)). \] Under the usual least-fixed-point interpretation of an inductive definition, its associated operator is \[ \Phi(X)=\{x\in D:B(x)\lor\exists y\in D\,(y<x\land y\in X)\}, \qquad I=\mu\Phi, \] where $\mu\Phi$ denotes the least fixed point under inclusion. This explains a conventional interpretation of "inductive"; the displayed equivalence alone does not specify a least fixed point, and the supplied record does not explicitly give its fixed-point semantics.

For a general defining formula $A(X,x)$, strict positivity conventionally requires that occurrences of the predicate variable $X$ appear only positively and never in an implication antecedent, with negation understood as implication to falsity. The precise permitted syntax and ambient logic must be specified to make this condition formal. In a setting where such a formula defines a monotone operator $\Phi_A$ and its least fixed point exists, write $I_A=\mu\Phi_A$.

Question (schematic). Does dynamic induction, reported in the supplied source to extend from the natural numbers to inductive definitions of the displayed special form, extend to every strictly positive inductive definition $I_A=\mu\Phi_A$ in the intended framework?

The supplied literature assessment describes the intended target as a dynamic-induction extraction theorem. However, the record supplies neither the dynamic-induction rule nor the extraction theorem, its hypotheses, or its required conclusion. Consequently, this is a statement of the supplied extension question, not a fully specified proof-theoretic assertion. No well-foundedness assumption on $<$, choice of ambient logic, or extension to coinductive definitions is added.

Short English statement

The question asks whether dynamic induction extends from the stated special kind of inductive definition to every strictly positive inductive definition. A precise theorem requires the original dynamic-induction principle, its extraction guarantee, and the intended logical framework, which the supplied record does not provide. The supplied status is partially_solved; this draft does not independently verify that assessment.

Sources

• Local UnsolvedMath registry: supplied complete record for permanent ID $30002736$, title "Dynamic Induction for Strictly Positive Definitions," exact source problem code catalogue entry, in the Oberwolfach Reports Open Problems collection. No individual proposer is supplied; the recorded proposed year is 2014.
• Supplied primary-source citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2015), Oberwolfach Reports, pp. 2933--2986, DOI 10.4171/owr/2014/52. https://doi.org/10.4171/owr/2014/52. This is also the literature-source entry labelled "original OWR report." The supplied record labels the statement corrected_verified and reports that the official report passage was checked directly and its question, definitions, and notation restored without strengthening the claim. Those are supplied verification claims, not verification performed for this draft.
• Supplied literature source: "Berger, Prawf and program extraction." https://doi.org/10.1007/978-3-030-51466-2_12. The label is retained as supplied.
• Supplied literature source: "Blanqui, Jouannaud, and Rubio on strictly positive types." https://arxiv.org/abs/0708.3582.
• Supplied literature assessment, checked on exactly 2026-08-21: status partially_solved. It states that proof systems support unrestricted strictly positive inductive and coinductive definitions in substantial generality, but that the specific dynamic-induction extraction theorem for every strictly positive definition was not established. This is supplied dated curation derived from the OWR material, not an independently verified literature assessment. The record expressly requests independent verification of time-sensitive status and cited claims.