Problem detail · source-aware

Signed Depth Relevance of subDL

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

subDL is a logic developed for paraconsistent mathematics by Zach Weber (2021), combining elements of relevant logic and affine logic. Tore Øgaard (2026) shows that subDL satisfies two important relevance properties: the signed variable-sharing property, which requires premises and conclusions of a valid inference to share a propositional variable with the appropriate polarity, and the depth-relevance property, which requires such a shared variable to occur at matching implicational depths. He leaves open whether subDL satisfies the stronger signed depth-relevance property, which combines these two constraints by requiring a variable to occur with both the appropriate sign and the appropriate implicational depth. The result proved here answers Øgaard’s question affirmatively: subDL satisfies the signed depth-relevance property. The proof proceeds by constructing, from any counterexample to signed depth relevance, an interpretation for subDL under which the premises receive designated values while the conclusion does not, contradicting validity. The construction can also be viewed as a simplification of Brady’s ω-rule technique for establishing relevance properties.

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

ChatGPT 5.6-Sol

The strongest AI attribution in this catalog, and it is not a disclosure statement but a byline: the paper's author line reads "GPT-5.6 Sol", dated 22 August 2026, with a single footnote - "Initially prompted by Ryan Simonelli." The model is credited as the author of the paper, not thanked in an acknowledgment. The submitter, who is Simonelli, describes his own role as having prompted it and summarises the model's as having "entirely constructed the proof", which the byline corroborates rather than merely asserts. Øgaard is thanked separately for correcting a notational error in an earlier draft and for observing the connection to Brady's $\omega$-rule.

Provider: OpenAI · Prompt public: unknown · Independence: unknown

Verification boundary

unreviewed

Filed as Unreviewed rather than the submitted Expert-verified, and the distinction is narrow enough to spell out. The paper's acknowledgments thank Tore Fjetland Øgaard - who posed the question, and so is both a named domain expert and a person with no stake in this proof - "for identifying the notational error concerning $\Rightarrow_m$ and $\to$ in an earlier draft and for pointing out the relation between the terminal clause and Brady's $\omega$-rule". That is genuine engagement by the right person: he read it closely enough to catch an error. It is not an endorsement of the final proof, and it is the only publicly checkable trace of his involvement. The submission states that he has verified the proof correct; that may well be so, but it rests on a private communication a reader cannot follow, and the Expert-verified rung on this site requires a checkable endorsement (its worked example is a published essay stating outright that named experts checked a proof and believe it correct). This site checked the surrounding facts, not the mathematics: Øgaard's paper exists as cited and leaves exactly this question open, and the proof itself - five pages over the Anderson-Belnap matrix $M_0$ - was read but not audited.

Correctness: unknown · statement fidelity: unaudited · peer review: none

Timeline

  1. Signed Depth Relevance for subDL

    subDL satisfies the signed depth relevance property, answering an open question posed by Øgaard (2026). More precisely, every valid inference in subDL contains a propositional variable that occurs in both the premises and conclusion with matching sign and at matching implicational depth.

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.