Session: sess_1749568800_orchestrate83

Analyzed public import Cslib.Init in Connectives.lean, InferenceSystem.lean,
and FrameConditions.lean. All 3 can be downgraded to plain import with 5
compensating imports in downstream Foundations/Logic files. Identified why
task 70's previous attempt failed (missing compensating imports).

Session: sess_1781118126_4901e1

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Session: sess_1781118126_4901e1

Session: sess_1781118126_4901e1

Research missed 7 files that use @[expose] from Cslib.Init transitively.
Build passes with all 12 compensating imports plus 3 downgrades.

Session: sess_1781118126_4901e1

lake shake shows no Cslib.Init warnings for any modified files.
All 4 phases complete.

Session: sess_1781118126_4901e1

Downgraded public import Cslib.Init in 3 Foundations/Logic files,
added 12 compensating imports. Build and lake shake verified clean.

Session: sess_1781118126_4901e1

…nd MCS consistency foundations

Adds the Cslib/Foundations/Logic/ module hierarchy: 16 files, 3,704 lines total.
Provides Hilbert-style proof system infrastructure for downstream modal, temporal,
and bimodal metalogic modules.

- Core definitions: InferenceSystem typeclass, HasBot/HasImp connective classes,
  polymorphic axiom abbrevs, bundled proof system typeclasses, LogicalEquivalence
- Theorem libraries: SKI/BCC combinators, propositional core (LEM, DNE, RAA),
  derived connective theorems, big conjunction, K-level and S5-level modal theorems,
  temporal derived theorems, frame conditions
- Metalogic foundations: DerivationSystem with Lindenbaum's lemma via Zorn's lemma,
  MCS construction; HasHilbertTree with generic deduction theorem helpers

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

… branch

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add 6 new files (ProofSystem/{Axioms,Derivation,Instances}, Metalogic/{DeductionTheorem,MCS},
NaturalDeduction/FromHilbert), update 2 modified files (Defs, NaturalDeduction/Basic),
add transitive dependency (Foundations/Data/ListHelpers), and update Cslib.lean imports.

Session: sess_1781124422_5169f2

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Session: sess_1781124422_5169f2

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- FromHilbert.lean: change 6 `def` to `theorem` for Prop-valued results,
  remove redundant `noncomputable` modifiers
- Instances.lean: wrap instances in `Cslib.Logic.PL` namespace to fix
  topNamespace lint errors
- Defs.lean: replace Set.Image import with Set.Basic per lake shake

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Session: sess_1781124422_5169f2

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Reflects addition of 8 Propositional files + ListHelpers (task 85),
growing PR from 16 files/3,704 lines to 25 files/5,120 lines.
Adds new sections: Propositional Proof System Architecture, expanded
file inventory and dependency graph.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Replace Mathlib.Order.SuccPred.LinearLocallyFinite with
Mathlib.Data.Finset.Attr for import minimization.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Explains why the Hilbert system is primitive for metalogic (uniform
extensibility, MCS closure, deduction theorem as theorem, simple
induction) and natural deduction is derived.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Session: sess_1781129709_2498f0

Session: sess_1781128371_8f84f0

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Brings in lint fixes from task 85 and task 86 (phases 1-2):
- Task 85: Propositional file lint fixes, FrameConditions import fix
- Task 86 phase 1: trivial fixes (double blank line, unused tactics)
- Task 86 phase 2: flexible simp -> simp only replacements
- Upstream: Bisimulation golf, governance, toolchain bump

Lean files resolved to feature branch (lint-fixed) versions.
Cslib.lean resolved to main (preserves Temporal imports).

Session: sess_1781128371_8f84f0

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Phases 1-2 completed (trivial fixes + simp only replacements).
Phases 3-5 remain (import removals, restructuring, CI verification).
Cleaned up orchestrator transient files.

Session: sess_1781128371_8f84f0

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Removed unused `import Cslib.Init` from FrameConditions.lean.
Connectives.lean and InferenceSystem.lean require Cslib.Init for
Type* notation (via Mathlib.Tactic.TypeStar) so were kept unchanged.

Session: sess_1781130632_b2a8c2

Session: sess_1781131142_bf29ba

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Investigation found that lake exe shake recommendations are not
applicable: Theorems files need their theorem-bearing imports (not
just ProofSystem typeclasses), and all files need private import
Cslib.Init for Type* notation since the public import chain uses
private Cslib.Init throughout.

Session: sess_1781130632_b2a8c2

0 critical, 0 high, 3 medium, 3 low issues found.
Fixed stale active_topics in state.json.

Session: sess_1781131440_3f1197

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Reverted FrameConditions.lean Cslib.Init removal (checkInitImports
requires all modules to import Cslib.Init). All 4 runnable CI checks
pass with 0 errors in scope files. Added noshake.json config file.

Session: sess_1781130632_b2a8c2

- Removed unused `public import Mathlib.Data.Finset.Attr` from
  FrameConditions.lean (verified by shake and full build)
- Removed scripts/noshake.json to match upstream (upstream deleted it
  in commit 2293f61 when upgrading to --add-public --keep-implied
  --keep-prefix flags; shake is commented out in upstream CI)
- Tested all shake import recommendations for in-scope files;
  every recommendation either breaks the build or fails checkInitImports
- All 4 active upstream CI checks pass: lake lint, lint-style,
  checkInitImports, mk_all --module --check

Session: sess_1781130632_b2a8c2

Session: sess_1781282351_53fffc

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Replace raw constructor calls with notation in Propositional/Metalogic/:
- MinCompleteness: Proposition.bot -> ⊥, φ.imp ψ ∈ T.val -> (φ → ψ) ∈ T.val
- MinLindenbaum: Proposition.bot -> ⊥, a.imp φ -> (a → φ), deductionWithMem arg
- IntLindenbaum: a.imp φ -> (a → φ), deductionWithMem arg, return type existential
- Completeness: φ.imp ψ -> (φ → ψ) in prop_negation_complete call, Proposition.neg → (¬·)
- MCS, DeductionTheorem: all .imp in ∀-quantified positions, skipped per constraints
- Soundness, IntSoundness, MinSoundness, IntCompleteness: no changes needed

Plan Phase 4 marked [COMPLETED].

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Replace expression-position raw constructors with notation in:
- Cslib/Logics/Modal/Basic.lean: theorem signatures (.neg φ→¬φ, .diamond φ→◇φ,
  .and→∧, .or→∨) and change tactics using only prefix operators (◇◇φ, ◇φ)
- Cslib/Logics/Modal/LogicalEquivalence.lean: Context.fill function body
  (.imp→→, .box→□ in match arm results)
- Cube.lean and Denotation.lean: no safe replacements found (pattern match arms
  and tactic arguments only)

Key constraint learned: change tactics with Proposition.imp (→) notation are
unsafe because the tactic parser sees → as Lean's function arrow. Only prefix
operators (◇, □, ¬) are safe in change/have type annotations.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

All 16 ProofSystem/Instances files examined. All Proposition.imp/box/bot/diamond
occurrences are inside inductive constructor return types and must not be replaced.
No expression-position occurrences found. Build passes.

Session: sess_1749800000_165ph6

Session: sess_1749805000_165ph7

…rems

Session: sess_1749810000_165ph8

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Applied safe syntactic sugar replacements to 10 temporal metalogic files:
DenseCompleteness, WitnessSeed, Chronicle/Frame, CompletenessHelpers,
TemporalContent, MCS, Chronicle/ChronicleConstruction, Chronicle/RRelation,
Chronicle/CounterexampleElimination, Chronicle/PointInsertion.

Replaced Formula.X ∈/∉ patterns with notation (¬, 𝐅, 𝐆, 𝐏, 𝐇, U, S, →)
in set membership contexts only. Total ~230 replacements across all files.
lake build Cslib.Logics.Temporal.Metalogic passes. Phase 9 complete.

Session: sess_1749820000_165ph9b

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

All 9 phases complete. Replaced ~650+ raw constructor calls with scoped
notation across Propositional, Modal, and Temporal logic modules.
lake test passes (8976 jobs).

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Session: sess_1749783600_orchestrate

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Session: sess_1749783600_orchestrate

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Three tasks to incorporate task 165 syntactic sugar changes into open PRs:
- 166: PR leanprover#633 (pr1/foundations-logic) — Propositional, addresses xcthulhu review comment
- 167: PR leanprover#637 (refactor/modal-primitives) — Modal
- 168: pr3/temporal-formula branch — Temporal (no PR submission)

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

A previous modification to CODEOWNERS had the unintended consequence that chenson2018 couldn't approve PRs to logic any longer, which is too restrictive until we get more logic maintainers.

Adds logical equivalence for modal logic, proving that it is a
`Congruence` (for any modal logic, regardless of the class of models
considered) and a `LogicalEquivalence` (for logic K, i.e., when
considering the class of all models).

The PR also renames `Proposition.neg` to `Proposition.not` and adds a
useful lemma on `Proposition.iff`.

Depends on leanprover#528.

---------

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>

I forgot `declare_term_config_elab` generated these for Boolean options
when writing this documentation.

Refactor the propositional `Proposition` to `{atom, bot, imp}` primitives, with
negation, conjunction, disjunction, and verum as derived `abbrev`s. `{imp, bot}`
is functionally complete for classical logic, so the other connectives are
definable rather than postulated: this keeps the inductive minimal (fewer cases
in every recursion and induction) and lets the derived connectives unfold
definitionally, so reasoning about them needs no separate axioms or bridging
lemmas.

- Add `Cslib/Foundations/Logic/Connectives.lean`: the connective typeclass
  hierarchy (`HasBot`, `HasImp`, `HasBox`, `HasUntil`, `HasSince`; bundled
  `PropositionalConnectives`/`ModalConnectives`/`TemporalConnectives`/
  `BimodalConnectives`; and `ImpBotDerived` for the derived-connective defaults).
- Replace `and`/`or`/`impl` constructors with `bot`/`imp` in
  `Propositional/Defs.lean`; update `complexity`, `atoms`, and `subst`.
- Cut the natural-deduction rules from 10 to 5; the derived-connective rules
  become derivable rather than primitive.
- Add bibliography entries (Church, Gentzen, Heyting, Chagrov & Zakharyaschev,
  Prawitz, Troelstra & van Dalen).

Refactor the modal `Proposition` inductive to the `{atom, bot, imp, box}`
primitive basis: falsum and implication as the primitive propositional
connectives, box as the primitive modality. Negation, conjunction,
disjunction, verum, possibility, and biconditional become derived connectives
via the `Cslib.Foundations.Logic.Connectives` interface introduced in leanprover#635;
`Proposition` is registered as a `ModalConnectives` instance.

- Replace `not`/`and`/`diamond` constructors with `bot`/`imp`/`box`; derived
  connectives are `abbrev`s, enabling definitional unfolding.
- Rewrite `Satisfies` on the new primitives and add explicit characterisation
  lemmas (`neg_iff`, `diamond_iff`, `and_iff`, `or_iff`, `iff_iff_iff`).
- Replace all `grind`-based axiom-validity proofs (K, dual, T, B, 4, 5, D and
  their frame-correspondence converses) with explicit term-mode proofs.
- Update `Denotation.lean` for the new primitives with explicit proofs.
- Rework `LogicalEquivalence.lean`: a one-hole `Proposition.Context` and a
  direct `LogicallyEquivalent`/`congruence`, in place of instantiating the
  shared `LogicalEquivalence` typeclass (rationale in the file's Design Notes).
- Add `#grind_lint skip` entries for the derived-connective characterisations
  whose `@[scoped grind =]` annotations have long instantiation chains.

Stacked on leanprover#635 (propositional primitives); review/merge that first.