What was already known
Øgaard proved signed variable sharing and unsigned depth relevance separately, and left their conjunction open. The separate properties do not force the same variable to witness both.
AI involvement
Simonelli prompted the question and lists the result as autonomous work by GPT-5.6 Sol. Øgaard later gave the specific correction and conceptual comment.
Model authorship and Simonelli’s first-person autonomy account support independent development after the problem prompt.
Importance
Claims the open combined relevance property for subDL.
Limitations
Øgaard identified an earlier notation error and a link to Brady’s ω rule. No complete check of the terminal soundness and finite-level separation argument is documented.
Technical verification
Øgaard’s correction and comment document human checking of a notation-sensitive portion. Simonelli’s general correctness statement does not specify a completed check of every axiom, rule and separation lemma; no machine formalization is documented.
Independent checking
Human reading that identified a notational error and conceptual antecedent
- Checker
- Tore Fjetland Øgaard
- Scope
- Earlier draft’s M0 relevant-arrow and designatedness-collapse notation, and relation of the terminal clause to Brady’s ω rule
- Basis
- Reported by the linked checker
Human understanding
The named humans identify a notation issue and a prior ω-rule connection, but no human account of the complete terminal soundness and separation mechanism is documented; Few is the evidence default.
Correction and publication history
Claims the open combined relevance property for subDL.
Read this published revision