feat(Logic): logical operators by fmontesi · Pull Request #607 · leanprover/cslib

fmontesi · 2026-05-29T12:56:23Z

This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.

chenson2018 · 2026-05-29T13:18:27Z

+public import Cslib.Foundations.Logic.Operators.Not
+public import Cslib.Foundations.Logic.Operators.Box
+public import Cslib.Foundations.Logic.Operators.Diamond
+public import Cslib.Foundations.Logic.Operators.Iff


Would it be better to just have one file for these? If they're just notation typeclasses it seems unlikely to be heavyweight and they're likely to be used together.

I don't know yet. We will expand these files with extended classes for expected properties about these operators, but you're right that some will require importing more than one.. I think we'll know more once we get there.

I propose 3 files:

Modal containing box and diamond.

Tensor by itself.

Propositional for the reset.

BTW, do we need parameterized box and diamond for HML?

The class was intentionally uninstantiated dead code. Its neg/top rationale (minimal-logic validity) now lives in the module docstring; formula types define neg/top as abbrevs directly. Future generic abstractions should use PR leanprover#607-style HasNeg/HasTop atomic classes. Session: sess_1781312776_63c955

Upstream PR landscape audit for Modal/ logic. No competing signature-change PRs. PR leanprover#607 stalled with CHANGES_REQUESTED. Recommends stacking Modal PR on feat/temporal-formula-propositional. Session: sess_1781531573_4cdbb4

Diplomatic PR description for Modal/ formula primitives refactoring, stacking on PR leanprover#648. Coordinates with PRs leanprover#607, leanprover#528, leanprover#535, leanprover#649. Session: sess_1781535860_c7d8e9

benbrastmckie · 2026-06-17T21:34:59Z

Hi @fmontesi — I wanted to flag some overlap with PR #648 so we can coordinate.

PR #648 includes Connectives.lean with a single-file approach to connective typeclasses (HasBot, HasImp, HasAnd, HasOr), following @chenson2018's consolidation suggestion. A planned Modal follow-up would extend it with HasBox/ModalConnectives.

The main naming difference is HasImpl/impl here vs HasImp/imp in #648. I went with imp for consistency with FormalizedFormalLogic and the rule name prefix convention (impI/impE), but happy to align whichever way you and other reviewers prefer.

A follow-up to #648 would refactor the Modal constructors from {atom, not, and, diamond} to {atom, bot, imp, box}. The case for primitive bot is in this Zulip message (substitution invariance, free algebra property). Related reasoning favors primitive box: necessitation becomes a pure rule — ⊢ φ → ⊢ □φ — stated in terms of box alone, rather than an interaction rule requiring dia and neg, or dia, bot, and imp. This would affect how typeclass instances are written. I'd welcome your input on this issue and will post on the Modal Zulip thread.

eric-wieser · 2026-06-19T23:07:13Z

I'd suggest merging all these operators into a single LogicOperators file, since then you can give one docstring that summarizes the conventions of their meanings.

eric-wieser · 2026-06-19T23:07:51Z

-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
-@[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}


A little cleaner as

Suggested change

instance : HasAnd (Proposition Atom) := {and := Proposition.and}

instance : HasAnd (Proposition Atom) where and := .and

etc

eric-wieser · 2026-06-19T23:28:12Z

    induction ctx <;> grind [= Context.fill]

-noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where
+noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where


Note that the Has prefix is largely a Lean 3-ism.

…#648 refresh Recreates the four tasks lost during the main cleanup, aligned with Thomas Waring's closing recommendation in the CSLib Zulip "Propositional Logic" thread (606970606) and our synthesis decision: - 398 efq_nd_rule_ipl_base_keep_mpl: make IPL the base logic (efq as a primitive ND rule) while PRESERVING all completed MPL metatheory as a retained layer. Depends on 397 (green main). - 399 refresh_pr648_ipl_base_foundation: update PR leanprover#648 to the settled IPL-base foundation (refs + Zulip link), small + upstream-based cherry pick, connectives excluded. Depends on 398. - 400 reconcile_connectives_pr607: unbundle connectives, reconcile with fmontesi PR leanprover#607 (Waring flag a). - 401 polymorphic_evaluator_bool_prop_dpll: AlgEvaluate at Bool/Prop for DPLL (Doty/Waring). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NarRy36MgZCZP7TRsrL5Df

… falso Promote ex falso quodlibet (bottom-elimination) to an ungated primitive constructor of the natural-deduction Derivation, so IPL is the base propositional logic and the primitive bot constructor has an inference rule. IPL becomes the empty base theory; CPL still adds double negation elimination. The minimal-logic (MPL) layer is deferred to a separate PR: this removes MPL, the IsIntuitionistic typeclass, intuitionisticCompletion, and the derived efq rules, keeping the classical layer (byContra/lem/pierce and the IsClassical instances for CPL/LEM/Pierce) intact, re-proved via the efq constructor. Per reviewer feedback (Waring, CSLib Zulip 'Propositional Logic'): - Drop the connective typeclasses (Foundations/Logic/Connectives.lean and its registration instances) -- a separate development handled via PR leanprover#607. - Restore references (Gentzen 1935, Prawitz 1965, Troelstra-van Dalen 1988) and add the CSLib Zulip thread link. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019sHZHp7U5qSiEzioK1nGEH

benbrastmckie · 2026-06-29T21:55:10Z

Following up on my comment above: the overlap I flagged is now resolved on #648's side — I've removed the connective typeclasses from #648, so it no longer duplicates the classes in this PR. #648 now contributes the five-primitive Proposition (primitive ⊥), its natural deduction, and an MPL/IPL/CPL/IsIntuitionistic theory layer.

That leaves one spot where the two PRs still meet: your head has since its own Proposition and a near-identical MPL/IPL/CPL/IsIntuitionistic development in the same file, Propositional/Defs.lean. To stay coordinated we'd need a single Proposition and one copy of that theory layer. The one substantive decision is how ⊥ is represented — here it's Proposition = {atom, and, or, impl} with ⊥ = atom ⊥ gated on [Bot Atom]; in #648 ⊥ is a primitive constructor.

I'd favor the primitive ⊥, mainly for substitution-invariance (Zulip): when ⊥ = atom ⊥, falsum lies in the image of atom, so a substitution Atom → Proposition can rewrite it and the type is no longer the free algebra over the signature. A primitive bot keeps ⊥ fixed under substitution, drops the [Bot Atom]/[Inhabited Atom] side-conditions (not_eq : (A → ⊥) = ¬A becomes an unconditional rfl, and minimal logic works over any atom type), and gives ⊥ its own case in every recursion rather than folding it into atom. The gap is narrow either way — #607 already reuses Mathlib Bot/Top and has not_eq := rfl — so whichever we pick, that theory layer should live in one place; happy to do the merge, or to adapt #648 to whatever you settle on.

Two smaller notes: I'd keep the Has* prefix (bare And/Or/Iff clash with core, and CSLib already uses HasSubstitution/HasFresh), and the connective precedences are worth recording in NOTATION.md. The file consolidation and the grind-into-notation point already look covered.

fmontesi and others added 6 commits May 21, 2026 14:48

Logical operators

31fb1ca

PL connectives, start modal

31dcc0e

fix not_def

060954e

fix modal connectives

2f4b4c9

Merge branch 'main' into fmontesi/connectives

1024345

indirection in _def lemmas

d4410e3

fmontesi requested a review from chenson2018 as a code owner May 29, 2026 12:56

fmontesi changed the title ~~feat (Logic): logical operators~~ feat(Logic): logical operators May 29, 2026

update cslib.lean

63918a2

chenson2018 requested changes May 29, 2026

View reviewed changes

ctchou mentioned this pull request Jun 12, 2026

refactor: Proposition type to bot/imp primitives #635

Closed

This was referenced Jun 14, 2026

feat(Logics/Propositional): five-primitive formula type with connective typeclasses #647

Closed

feat(Logics/Propositional): five-primitive formula type with primitive bot #648

Open

fmontesi added 3 commits June 16, 2026 08:34

merge main

500a9d9

merge main again

9669f24

fix compilationg

604ba15

fmontesi requested a review from arademaker as a code owner June 16, 2026 06:37

fmontesi and others added 5 commits June 16, 2026 08:52

fix some proofs

20b4a92

fix simp lints

c7e5a4c

merge main

abf73e5

parametrised logical equivalence

059a85c

grind annotation for not

c2ec296

benbrastmckie mentioned this pull request Jun 19, 2026

feat(Logics/Modal): refactor formula primitives to {atom, bot, imp, box} #662

Open

eric-wieser reviewed Jun 19, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(Logic): logical operators#607

feat(Logic): logical operators#607
fmontesi wants to merge 15 commits into
mainfrom
fmontesi/connectives

fmontesi commented May 29, 2026

Uh oh!

Uh oh!

chenson2018 May 29, 2026

Uh oh!

fmontesi May 29, 2026

Uh oh!

ctchou Jun 1, 2026

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

eric-wieser Jun 19, 2026

Uh oh!

eric-wieser Jun 19, 2026

Uh oh!

eric-wieser Jun 19, 2026

Uh oh!

benbrastmckie commented Jun 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

	instance : HasAnd (Proposition Atom) := {and := Proposition.and}
	instance : HasAnd (Proposition Atom) where and := .and

Uh oh!

Conversation

fmontesi commented May 29, 2026

Uh oh!

Uh oh!

chenson2018 May 29, 2026

Choose a reason for hiding this comment

Uh oh!

fmontesi May 29, 2026

Choose a reason for hiding this comment

Uh oh!

ctchou Jun 1, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

benbrastmckie commented Jun 17, 2026

Uh oh!

eric-wieser Jun 19, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jun 19, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jun 19, 2026

Choose a reason for hiding this comment

Uh oh!

benbrastmckie commented Jun 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants