Jump Property of Implication Proof Systems

Definitions and mathematical statement

The supplied record concerns implicit propositional proof systems, but does not define that class, the construction $[P,P]$, or the technical meaning of a jump in proof strength. Retain the source notation \[ \operatorname{imp}(P):=[P,P]. \] The intended conjecture, on the universal reading of the supplied statement, is: for every implicit propositional proof system $P$ within the source's intended scope, $\operatorname{imp}(P)$ is a jump in proof strength.

This is a schematic statement requiring clarification from the source. In particular, the admissible systems and any additional hypotheses on $P$, the definition of $[P,P]$, the comparison relation on proof systems, and the conditions defining a jump are absent from the supplied excerpt. Consequently, no precise assertion about strict increase, simulation, or other properties of a jump can be substituted without additional evidence. The excerpt itself says only that $\operatorname{imp}(P):=[P,P]$ is conjectured to be a jump; it does not explicitly state the domain or quantifier for $P$.

Short English statement

The supplied conjecture asks whether the implicit construction $\operatorname{imp}(P)=[P,P]$ gives a jump in proof strength for each admissible implicit propositional proof system $P$. Its precise mathematical content remains unresolved because the supplied excerpt omits the construction, the admissibility hypotheses, and the definition of a jump.

Sources

• Supplied local UnsolvedMath registry record: permanent ID $30005748$, source problem code catalogue entry, title "Jump Property of Implication Proof Systems."
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2024), Oberwolfach Reports, pp. 3013--3061, DOI https://doi.org/10.4171/owr/2023/53. The literature-source list labels this reference "Oberwolfach Report 53/2023." The supplied excerpt associates the conjecture with Pavel Pudlák's contribution "Consistency, implicit proofs, and cut-elimination," p. 3023. The record gives proposed year 2023 and leaves the proposer field empty.
• Supplied literature reference: Egidy, Recursive Jump Operators and Optimal Proof Systems, https://doi.org/10.4230/LIPIcs.ICALP.2026.88.
• Supplied literature assessment dated exactly 2026-08-22: the record labels the problem open, states that the report presents $\operatorname{imp}(P)=[P,P]$ as a conjecture, and says that a 2026 study still describes jump existence for $\mathrm{TAUT}$ as open, with no resolution of the extracted conjecture available in that assessment. This is supplied dated curation, not independently verified here; the record itself requests independent verification of time-sensitive status and cited claims.
• The registry marks the statement corrected_verified and reports a check against the official Oberwolfach report. That verification claim is supplied metadata and has not been independently confirmed here.