Wraith Redundancy for Algebraic Theories

Definitions and mathematical statement

Let $T$ range over algebraic theories in the sense intended by the source report, and let $\varphi$ range over sentences in the language and logical fragment intended there. The supplied literature assessment describes the restricted class as algebraic coherent theories. Write $\operatorname{Red}_T(\varphi)$ for the source's property that $\varphi$ is $T$-redundant, and write $G_T$ for its intended generic model of $T$.

The question is whether, for every such $T$ and every such $\varphi$, \[ \operatorname{Red}_T(\varphi) \quad\Longrightarrow\quad G_T\models\varphi. \] Here satisfaction must be interpreted in the semantics intended for the generic model.

The supplied record does not define $T$-redundancy, specify the permitted sentence fragment, define the generic model or its ambient semantics, or give the precise convention for algebraic theories. Consequently, the displayed implication records the quantified target using placeholders for these missing definitions; it is not yet a fully specified mathematical assertion. In particular, the relationship between the statement's algebraic theories and the assessment's algebraic coherent theories requires clarification from the cited sources.

Short English statement

For every algebraic theory $T$, must every $T$-redundant sentence hold in its generic model? The supplied record leaves the central definitions and logical semantics unspecified, so this statement-only draft requires clarification and human mathematical review.

Sources

• Supplied local registry record, permanent UnsolvedMath ID $30003656$, title Wraith Redundancy for Algebraic Theories, exact source code catalogue entry, in the Oberwolfach Reports Open Problems collection. No individual proposer is identified; the supplied proposed year is 2017.
• Supplied source citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2018), Oberwolfach Reports, pp. 3121--3183, DOI 10.4171/owr/2017/53. https://doi.org/10.4171/owr/2017/53. The background describes these reports as documenting mathematical workshops and their open-problem discussions.
• Supplied literature reference: Bezem--Buchholtz--Coquand, Syntactic forcing models for coherent logic. https://doi.org/10.1016/j.indag.2018.06.004.
• Supplied literature reference: Oberwolfach Report 53, algebraic-theory open problem. https://doi.org/10.4171/owr/2017/53.
• Literature assessment dated exactly 2026-08-21: the supplied curation labels the problem open, reports that the general Wraith question is disproved, and states that a positive answer for algebraic coherent theories remains unresolved. This is supplied dated curation derived from the OWR material, not an independently verified literature assessment; its status and cited claims require independent verification.
• The registry labels the statement corrected_verified and says that notation, typography, and sentence structure were repaired while mathematical content was preserved. These are supplied editorial claims, not independent verification of the formulation in this draft.