refactor(Studies): disaggregate PIP — relocate to Studies, consume Core, Prop-native

[hawkrobe]

PIP (Plural Intensional Presuppositional predicate calculus, Keshet & Abney) was a 6-file framework masquerading as theory-layer substrate in Semantics/PIP/, despite being consumed only by its own author program. This relocates it to Studies/KeshetAbney2024/, makes it consume Core's modal logic and quantifier theory instead of duplicating them, and removes the Bool-as-predicate machinery.

• Modals: .must/.might now are Core.Logic.Intensional.boxR/diamondR by construction; BAccessRel (duplicated Bool accessibility) deleted for AccessRel. Bridge theorems collapse to Iff.rfl.
• Quantifiers: deleted pipEvery/pipSome (byte-identical copies of Core.Quantification.every_sem/some_sem) and their re-proved conservativity/monotonicity; setEvery/setSome now bridge straight to Core and inherit every_conservative etc.
• Bool→Prop: truth/felicitous and all model predicates; Fintype/FiniteDomain/noncomputable plumbing dropped. Genuine boolean data (coverage table) stays Bool.

Post-merge a multi-reviewer audit drove follow-up fixes in this PR: removed a vacuous K ≤ T lemma, corrected paper item-number citations (verified against the SP/Glossa PDFs), and fixed stale sorry-claiming docstrings.

Deferred to a follow-up PR (pre-existing, not Bool→Prop): the hypothesis-circular must_allows/might_blocks lemmas → reformalize via the incremental-discourse-felicity condition so the modal does real work; the 2024→2025 chronological import dependency; PIPExpr := PIPExprF Empty deduplication.