Nontriviality of number-restricted arithmetic over subDMQ
Weber's programme of paraconsistent mathematics keeps unrestricted comprehension and revises the logic of inference so that contradictions do not make every statement provable. Ripley and Weber's 2026 proposal restricts induction to numbers as part of a strategy for blocking paradox, and Ripley's presentation of it records that the resulting theory is not known to be trivial, the programme working "without a net: no nontriviality proofs". Is number-restricted arithmetic over subDMQ nontrivial: does it, together with naive comprehension and induction over the combined language, avoid proving everything?
- Result
- Disproved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Paraconsistent logic and foundations
- Posed by
- Ellie Ripley and Zach Weber
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-09-10
- Model
- GPT-6 Astra
- Vendor
- OpenAI
- Collaborators
- Ryan Simonelli
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Number-restricted induction over subDMQ derives A ⇒ A ⊗ A for every formula A to which induction applies, without using quantifier splitting. Restricted quantifier splitting follows as a corollary. A second argument obtains contraction from unrestricted quantifier splitting and a separated domain partition. With suitable Curry fixed points, contraction yields triviality.
What the AI did
The paper's author line is "GPT-6 Astra (context 1e44c278f25b)", dated 10 September 2026, with a footnote: "Ryan Simonelli initiated and guided the research conversation that produced this note. The argument emerged from repeated unsuccessful attempts, at his prompting, to find an elegant sequent calculus with syntactic cut elimination for Ripley's reconstruction of Weber's mathematics." The submitter adds that after those attempts failed, the model instead established that the intended theory is trivial, and produced the proof constructions, the manuscript, the proof certificates and the checking code; Simonelli directed the investigation and assessed the outputs. Discovered rather than co-developed on that record: the model is credited as the author, and the human role was direction and assessment.
Verification
Filed as Unreviewed rather than the submitted Expert-verified, for the same reason as this submitter's earlier subDL entry, and the trace is stronger this time. The paper's footnote 3 reads: "I thank Ellie Ripley for confirming that the argument poses a problem for the intended programme, and for feedback on an earlier draft that helped to clarify and shorten this note." Ripley is exactly the right person - the proposer of subDMQ and of the restricted-induction strategy, confirming a result against their own proposal - and that footnote records agreement, not merely a correction. But it is the author's report of a private exchange, not the expert's own words a reader can follow to the source, and the Expert-verified rung's worked example is a published statement by the experts themselves. A public statement from Ripley would lift it. The paper supplies finite Hilbert-style proof certificates replayed by a custom Python checker and Isabelle replay scripts that the submitter reports have not been executed; neither was run here. This site checked the surrounding facts, not the derivations: Ripley's slides state the question as open, and the paper's source comparison pins Ripley's formalisation to the commit it examined.
Sources
Submitted by BraveEgret318 on