Incompleteness and Self-Consistency Below Robinson Arithmetic

Definitions and mathematical statement

Let $R$ denote the theory called Robinson's theory $R$ in the supplied record. Its axioms and language are not supplied, so its exact presentation remains to be confirmed. Fix a notion of interpretation, and write $A\preccurlyeq B$ when $B$ interprets $A$. Define strict interpretability by \[ A\lhd B\quad\Longleftrightarrow\quad A\preccurlyeq B\ \text{and}\ B\not\preccurlyeq A. \] The record does not specify the permitted interpretations or theory languages; the formulation below is conditional on fixing these conventions.

A theory is recursively axiomatizable if it admits a recursively enumerable set of axioms, and is consistent if it proves no contradiction. A consistent theory $S$ is incomplete if there is a sentence $\varphi$ of its language such that $S\nvdash\varphi$ and $S\nvdash\neg\varphi$. Define \[ \begin{aligned} G1(T)\quad\Longleftrightarrow\quad &\text{for every recursively axiomatizable consistent theory }S,\\ &T\preccurlyeq S\ \Longrightarrow\ S\text{ is incomplete}. \end{aligned} \] Let \[ \mathcal D=\{T:T\text{ is recursively axiomatizable and consistent},\ T\lhd R,\ G1(T)\}. \] The supplied corrected statement and dated assessment report that $\mathcal D\neq\varnothing$. This is supplied background, not an independently verified theorem here.

1. Is $(\mathcal D,\lhd)$ well founded? Explicitly, does every nonempty subset $\mathcal E\subseteq\mathcal D$ contain a theory $T$ for which no $U\in\mathcal E$ satisfies $U\lhd T$? Equivalently, in the usual set-theoretic setting, is there no sequence $(T_n)_{n\in{\mathbb{N}}}$ in $\mathcal D$ with $T_{n+1}\lhd T_n$ for every $n\in{\mathbb{N}}$?
2. Does $G2$ hold for $R$, in the sense of the supplied corrected statement: \[ R\nvdash\operatorname{Con}(R)? \] Here $\operatorname{Con}(R)$ is intended to be an arithmetical sentence expressing that there is no $R$-proof of a contradiction. The effective presentation of $R$, proof coding, and internal consistency formula are not specified in the record; this question therefore requires those choices to be fixed before it is fully precise.

The original statement instead asks whether such a theory $T\lhd R$ exists and defines $G2$ using the opposite assertion, that a theory proves its own consistency. The supplied verification note says that the report uses nonprovability of consistency, records the existence result below $R$, and leaves well-foundedness and $G2$ open. The questions above follow that supplied correction while retaining this formulation conflict explicitly. The dated assessment's claim to answer the "first question" concerns the original existence question; it does not supply an answer to well-foundedness.

Short English statement

Consider recursively axiomatizable consistent theories strictly below Robinson's theory $R$ under interpretation, such that every recursively axiomatizable consistent theory interpreting them is incomplete. Ask whether this class is well founded under strict interpretation, and whether $R$ fails to prove its own consistency. The supplied record reports existence of such theories, but the interpretation conventions, presentation of $R$, and consistency sentence require clarification. Its original and corrected formulations disagree about the meaning of $G2$.

Sources

• Local UnsolvedMath registry: supplied complete record with permanent ID $30004552$, exact source problem code catalogue entry, title Incompleteness and Self-Consistency Below Robinson Arithmetic, in Oberwolfach Reports Open Problems. The proposed year is supplied as 2020; no individual proposer is identified.
• Supplied report 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 these reports as documenting workshops and their open-problem discussions.
• Supplied literature source: Cheng, Finding the Limit of Incompleteness I. https://doi.org/10.1017/bsl.2020.9. The supplied assessment attributes to Cheng the construction of recursively enumerable theories $U\lhd R$ satisfying $G1$.
• Supplied literature source: Oberwolfach Report 34/2020. https://doi.org/10.4171/owr/2020/34.
• Literature assessment date: 2026-08-22. This is supplied dated curation, not an independently verified assessment. It labels the problem partially solved, reports the below-$R$ existence result, and describes the $G2$ question for $R$ as open in the cited literature. The background explicitly requests independent verification of time-sensitive status and cited claims.
• The registry labels the statement corrected_verified. Its supplied verification note says the official report was checked, that $G2$ means nonprovability of consistency, and that well-foundedness and $G2$ remain open there. This is a report of supplied verification metadata; no source visit or independent verification is asserted here.