Nontriviality of number-restricted arithmetic over subDMQ
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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?
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra
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.
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.
Contraction from Number-Restricted Induction in subDMQ
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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.