Partial Proof Objects in Martin-Löf Type Theory

Definitions and mathematical statement

In Martin--Löf type theory, a typing judgment $\Gamma\vdash a:A$ states that, in context $\Gamma$, the term $a$ inhabits the type $A$. Under the propositions-as-types interpretation, such a term represents a proof of the proposition expressed by $A$.

The supplied problem asks: what mathematical objects or formal mechanisms can represent partial proofs in Martin--Löf type theory, analogously to the partial functions used in the predicative construction of Mahlo universes?

Here "partial proof" is the notion to be developed, not a notion defined by the supplied record. The record does not specify the presentation of Martin--Löf type theory, the particular predicative construction of Mahlo universes, the partial functions involved, or the properties required of the proposed analogy. Consequently, the supplied question is a request for a mathematical framework; it does not determine a precise existence assertion or theorem with specified hypotheses and quantifiers. These qualifications remain unresolved.

Short English statement

The question asks for a mathematical account of partial proofs in Martin--Löf type theory, inspired by partial functions in a predicative construction of Mahlo universes. The supplied record leaves both the intended analogy and the requirements for partial proofs unspecified.

Sources

• Local registry: data/unsolvedmath/problems.json, permanent UnsolvedMath ID $30004558$, source problem code catalogue entry. Title: Partial Proof Objects in Martin--Löf Type Theory. The supplied proposed year is 2020; no individual proposer is identified.
• Supplied source citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2021), Oberwolfach Reports, pp. 1693--1757, DOI 10.4171/owr/2020/34. Source URL: https://doi.org/10.4171/owr/2020/34. The record attributes the question to the workshop-discussion material collected in this report, without a problem-specific page or named contributor.
• Supplied literature source: "OWR 2020/34 report," https://doi.org/10.4171/owr/2020/34. Literature assessment dated 2026-08-22: the supplied curation labels the problem open and reports that the source presents partial proofs as a puzzling question without a completed definition or theorem. This is supplied dated curation, not an independently verified assessment; the record requests independent verification of time-sensitive status and cited claims.