feat(Logics/Modal): semantics for the modal metalogic, compatible with constructive modal theories

[benbrastmckie]

Contributes a foundational semantic layer for the modal metalogic, designed to be compatible with the intuitionistic and constructive modal systems (IK, CK). This is the substantive ambition of the PR; the native Proposition datatype it is built on is the enabling foundation.

The semantic layer

Built on a native 7-primitive Proposition:

Proposition {atom, bot, imp, and, or, box, diamond}

(negation and verum stay derived via the Łukasiewicz convention ¬φ := φ → ⊥, ⊤ := ⊥ → ⊥, mirroring Cslib.Logic.PL.Proposition's native and/or), it provides:

• Satisfies — the satisfaction relation, defined natively over all 7 constructors.
• Denotational semantics — Denotation.lean extended to every constructor, with satisfies_mem_denotation, not_denotation, and theoryEq_denotation_eq.
• The duality theorem ◇φ ↔ ¬□¬φ — recovered as a proved semantic theorem (Satisfies.dual, via excluded middle) rather than baked in as a definition.
• One decomposition lemma per connective — now Iff.rfl, since every connective is structural (no Łukasiewicz-bridge lemmas).
• K-axiom validity, and the T/B/4/5/D frame-correspondence results and their converses, all preserved.

Why both box and diamond primitive?

Classically ◇φ := ¬□¬φ suffices, but in IK/CK □ and ◇ are not interdefinable ([Simpson 1994]). Keeping both native means the same datatype carries unchanged into those systems, and the semantic/tableau layer gets one clean decomposition rule per connective. Classically nothing is lost — the duality is recovered as the theorem above.

Relationship to #607 (rebase plan)

The native primitive-constructor design — {atom, bot, imp, and, or, box, diamond} with box/diamond both primitive — is the subject of #607, where the operator layer is being standardised. This PR is intended to be rebased onto #607 once it lands, so that the primitive constructors come from #607 and this PR carries only the semantic layer on top.

Until then it is based on main and self-contained, so it builds and can be reviewed independently. Coordination on the native primitive set is ongoing on #607 and the CSLib > Modal Logic Zulip thread.

Changes (5 files, +145 / −40 against main; the base will move to #607 on rebase)

• Cslib/Logics/Modal/Basic.lean — 7-primitive Proposition; native Satisfies; derived neg/top/iff; per-connective characterisation lemmas (now Iff.rfl); Satisfies.dual as a semantic theorem. All existing theorems preserved — including the T/B/4/5/D frame-correspondence results and their converses.
• Cslib/Logics/Modal/Denotation.lean — denotation extended to all 7 constructors; satisfies_mem_denotation, not_denotation, theoryEq_denotation_eq preserved.
• Cslib/Logics/Modal/Cube.lean — unchanged except an import; the Modal Cube (K…S5) and its validities carry over.
• Cslib/Logics/Modal/LogicalEquivalence.lean — one-hole Context not→neg former; congruence/LogicalEquivalence instances preserved.
• references.bib — adds the Simpson 1994 reference.

Notation (¬ ∧ ∨ → □ ◇ ↔) and every theorem name are preserved. Two derived definitions are renamed to match the native constructors — Proposition.not → Proposition.neg and Proposition.impl → Proposition.imp — and box/or move from derived definitions to native constructors under the same names (Proposition.Context.not is likewise renamed to neg). Sorry-free; axioms limited to propext / Classical.choice / Quot.sound. Full lake build, checkInitImports, lake lint, lint-style, lake test, and shake pass.

AI Disclosure

This work was drafted with the assistance of an AI coding agent (Claude, Anthropic) under the contributor's direction. All proofs were machine-checked by lake build/lake lint and the full CSLib CI, and reviewed before submission. Design decisions and review are the contributor's.

[benbrastmckie]

I've retitled this to reflect what it's really aiming at. The 7-primitive Proposition refactor is the enabling foundation, but the substantive contribution is the semantic layer for the modal metalogic: the Satisfies relation, the denotational semantics, the duality ◇φ ↔ ¬□¬φ recovered as a proved semantic theorem (Satisfies.dual, via excluded middle rather than by definition), one decomposition lemma per connective, and K-axiom validity.

The reason both □ and ◇ are native primitives here — rather than defining ◇φ := ¬□¬φ — is that this is what keeps the layer compatible with the intuitionistic and constructive modal systems (IK, CK), where the two are genuinely not interdefinable ([Simpson 1994]). That's the metalogic I want to build on top of this. Classically nothing is lost: the duality comes back as the theorem above.

On the primitive constructors themselves, this mirrors #607, which is where the native {atom, bot, imp, and, or, box, diamond} operator design is being worked out. Coordination on standardising that primitive set is ongoing on #607 and the CSLib > Modal Logic Zulip thread; this PR builds the semantics on that basis.