Signed Depth Relevance of subDL
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.
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Paraconsistent logic and foundations
- Posed by
- Tore Øgaard
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-08-04
- Model
- ChatGPT 5.6-Sol
- Vendor
- OpenAI
- Collaborators
- Ryan Simonelli
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 7 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
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.
What the AI did
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 -rule.
Verification
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 and in an earlier draft and for pointing out the relation between the terminal clause and Brady's -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 - was read but not audited.
Sources
Submitted by BraveEgret318 on