Proof-Theoretic Strength of Minimalist Foundations

Definitions and mathematical statement

Let $\mathrm{MF}$ denote the Minimalist Foundation referred to in the supplied source record, and let $\mathrm{MF}+\mathrm{EM}$ denote its classical extension by the law of excluded middle. Here excluded middle is expressed schematically as \[ \varphi\lor\neg\varphi \] for propositions $\varphi$ in the intended formulation; the precise language and scope of this schema must be specified by that formulation.

Problem. Determine the exact proof-theoretic strength of each of the theories \[ \mathrm{MF}\qquad\text{and}\qquad\mathrm{MF}+\mathrm{EM}. \]

Unresolved specifications. The supplied record does not give the axioms, inference rules, or precise presentation of $\mathrm{MF}$, nor does it specify how excluded middle is added in that presentation. It also does not define the intended measure of proof-theoretic strength. Its accompanying assessment mentions an exact ordinal or proof-theoretic calibration, without specifying an ordinal invariant, reference theories, or comparison relation. Consequently, the question above preserves the supplied target, but a fully specified formal problem requires these choices to be recovered from the cited sources; no particular choices or equivalence between possible calibrations are asserted here.

Short English statement

Determine exactly how strong the Minimalist Foundation and its extension by excluded middle are in proof-theoretic terms. The supplied record leaves the formal presentation and intended measure of strength unspecified. Its open status is supplied dated curation, not an independently verified conclusion.

Sources

• Local UnsolvedMath registry: supplied record with permanent ID $30004553$, title Proof-Theoretic Strength of Minimalist Foundations, in the Oberwolfach Reports Open Problems collection. Exact source problem code: catalogue entry. The record gives proposed year 2020 and supplies no individual proposer attribution.
• Supplied source citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2021), Oberwolfach Reports, pp. 1693--1757, DOI 10.4171/owr/2020/34. https://doi.org/10.4171/owr/2020/34. The background describes Oberwolfach Reports as documenting mathematical workshops and their open-problem discussions.
• Supplied literature reference: Maietti--Sabelli, 2024. https://doi.org/10.1016/j.apal.2024.103524. No article title or relevant theorem numbers are supplied.
• Supplied literature reference: Oberwolfach Report 34/2020. https://doi.org/10.4171/owr/2020/34.
• Literature assessment dated 2026-08-22: the supplied curation labels the problem open and reports that recent work establishes equiconsistency and useful upper bounds without identifying the exact ordinal or proof-theoretic calibration for $\mathrm{MF}$ and $\mathrm{MF}+\mathrm{EM}$. This is supplied dated curation derived from the supplied OWR curation, not independently verified source inspection or a new literature assessment. The record explicitly calls for independent verification of time-sensitive status and cited claims.