refactor: Proposition type to bot/imp primitives by benbrastmckie · Pull Request #635 · leanprover/cslib

benbrastmckie · 2026-06-12T01:45:20Z

Summary

Refactors the propositional Proposition inductive type to use {atom, bot, imp} as its
primitive constructors. Negation (neg), verum (top), conjunction (and), and disjunction
(or) become derived connectives defined as abbrevs. This replaces the previous
and/or/impl primitives.

Why falsum and implication as the primitives

The choice is justified on its own merits, not merely as a historical convention:

Functional completeness ⇒ definability. {imp, bot} is functionally complete for classical
propositional logic. Every other connective is therefore definable from these two, so it can be
a derived abbrev instead of a constructor with its own meaning.
A minimal inductive. Fewer constructors means fewer cases in every recursion and induction
over formulas — every function (complexity, atoms, subst, satisfaction, …) and every proof
by induction is correspondingly shorter.
Definitional, not axiomatic, connectives. Because ¬, ∧, ∨, ↔ are abbrevs, they
unfold to imp/bot by rfl. Reasoning about them reduces to reasoning about the two
primitives with no bridging lemmas and no risk of a derived connective drifting from its intended
meaning.
A smaller proof system. Implication internalises the consequence relation (the deduction
theorem) and bot gives negation as · → bot plus ex falso. The natural-deduction calculus over
this basis needs only 5 primitive rules instead of 10; the conjunction/disjunction rules become
derivable rather than postulated, so there is less to state and keep mutually consistent.

This basis is also the standard one in the literature (Heyting 1930; Gentzen 1935; Church 1956;
Chagrov & Zakharyaschev 1997) — see references.bib and the Connectives.lean header — but the
reasons above are why it is adopted here.

Context

This is Sub-PR 1.1.1 extracted from the larger PR #633, isolating the foundational Proposition
refactor as a self-contained, independently reviewable change. The Modal layer (#637) is stacked on
top of it.

Zulip topic: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Propositional.20Logic/with/602336739

File-by-file change summary

Cslib.lean

Adds public import Cslib.Foundations.Logic.Connectives (alphabetical position).

Cslib/Foundations/Logic/Connectives.lean (new)

Typeclass hierarchy for composable logics, shared across Propositional/Modal/Temporal/Bimodal:
- Atomic: HasBot, HasImp, HasBox, HasUntil, HasSince.
- Bundled: PropositionalConnectives, ModalConnectives, TemporalConnectives,
  BimodalConnectives.
- Derived defaults: ImpBotDerived, giving neg/top/or/and from bot/imp. It is
  intentionally uninstantiated (concrete formula types use directly-computing abbrevs); it is
  retained as a specification artifact and for future polymorphic proof-system abstractions.

Cslib/Foundations/Logic/InferenceSystem.lean

Visibility adjustment (public import Cslib.Init → import Cslib.Init) and a module docstring.

Cslib/Logics/Propositional/Defs.lean

Replaces and/or/impl constructors with bot/imp; defines neg/top/and/or as
derived abbrevs; registers the relevant Has*/PropositionalConnectives instances.
Updates Proposition.complexity, Proposition.atoms, and Proposition.subst for the new
constructors.

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

Reduces the primitive inference rules from 10 to 5 (axiom, assumption, implication
introduction/elimination, ex falso); conjunction/disjunction rules become derivable.

references.bib

Adds Church1956, Gentzen1935, Heyting1930, ChagrovZakharyaschev1997, Prawitz1965,
TroelstraVanDalen1988.

AI Disclosure

This PR was prepared with the assistance of Claude Code (Anthropic), used for drafting/extracting
files from a development branch, running CI verification commands, and drafting this description.
All Lean code was written by the author (Benjamin Brast-McKie) and verified to
compile on the PR branch.

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.

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.

eric-wieser · 2026-06-12T21:21:46Z

+/-- A type has a falsum (bottom) connective. -/
+class HasBot (F : Type*) where
+  /-- The falsum/bottom connective. -/
+  bot : F
+
+/-- A type has an implication connective. -/
+class HasImp (F : Type*) where
+  /-- The implication connective. -/
+  imp : F → F → F


Here you could co-opt mathlib's Bot and HImp classes

ctchou · 2026-06-12T23:18:06Z

First, are you aware of this PR: #607 ?

Second, and more seriously, can all logical connectives be reduced to implication and falsum in intuitionistic propositional logic? I don't think Cslib/Logics/Propositional/Defs.lean was designed for classical propositional logic alone.

Regarding natural deduction, so far as I can tell, the presentations in Prawitz and Troelstra & can Dalen do not do this kind of reduction at all. (I have Troelstra & van Dalen's book and I'm looking at it. At least part of Prawitz's book can be browsed here: https://www.google.com/books/edition/Natural_Deduction/sJj3DQAAQBAJ?hl=en)

ctchou · 2026-06-12T23:33:52Z

Also, you wrote:

This basis is also the standard one in the literature (Heyting 1930; Gentzen 1935; Church 1956;
Chagrov & Zakharyaschev 1997) — see references.bib and the Connectives.lean header — but the
reasons above are why it is adopted here.

Attached below is the Gentzen paper you cited:
BF01201353.pdf

I don't read German. But, judging from the formulas I can read, it seems to me that Gentzen was not using the implication+falsum basis you are proposing.

ctchou · 2026-06-12T23:52:26Z

I can't find the original text of the Heyting (1930) paper you cited. But the following discussion in "The development of intuitionistic logic" in Stanford Encyclopedia of Philosophy:
https://plato.stanford.edu/entries/intuitionistic-logic-development/#Heyt1930
is suggestive. In particular, consider the following passage:

Both conjunction and disjunction are there.

benbrastmckie · 2026-06-12T23:57:23Z

That's helpful. I think it may be best to close this and I'll think through the set up again.

Quality audit of 42 files in Propositional/ and Foundations/Logic/. Three teammates: architecture/imports, proof quality/naming, references/rigor. Literature references independently verified against PR leanprover#635 lesson. Session: sess_1781384225_4617ac Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

benbrastmckie requested review from arademaker, chenson2018 and fmontesi as code owners June 12, 2026 01:45

benbrastmckie changed the title ~~refactor: Proposition type to Lukasiewicz convention~~ refactor: Proposition type to Hilbert-style primitives Jun 12, 2026

benbrastmckie changed the title ~~refactor: Proposition type to Hilbert-style primitives~~ refactor: Proposition type to bot/imp primitives Jun 12, 2026

This was referenced Jun 12, 2026

feat(Foundations/Logic): propositional theorems, modal S5 theorems, and MCS consistency foundations #629

Closed

feat(Foundations/Logic): Hilbert proof systems, ND equivalence, and intuitionistic hierarchy #630

Closed

benbrastmckie mentioned this pull request Jun 12, 2026

refactor(Modal): bot/imp/box primitives for modal propositions #637

Closed

benbrastmckie force-pushed the refactor/proposition-lukasiewicz branch from a8e27b7 to 3ab8023 Compare June 12, 2026 09:22

eric-wieser reviewed Jun 12, 2026

View reviewed changes

benbrastmckie mentioned this pull request Jun 12, 2026

feat(Logics/Temporal/Syntax): temporal formula type and syntax utilities #642

Closed

benbrastmckie closed this Jun 12, 2026

benbrastmckie deleted the refactor/proposition-lukasiewicz branch June 13, 2026 00:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: Proposition type to bot/imp primitives#635

refactor: Proposition type to bot/imp primitives#635
benbrastmckie wants to merge 1 commit into
leanprover:mainfrom
benbrastmckie:refactor/proposition-lukasiewicz

benbrastmckie commented Jun 12, 2026 •

edited

Loading

Uh oh!

eric-wieser Jun 12, 2026

Uh oh!

ctchou commented Jun 12, 2026 •

edited

Loading

Uh oh!

ctchou commented Jun 12, 2026

Uh oh!

ctchou commented Jun 12, 2026

Uh oh!

benbrastmckie commented Jun 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

benbrastmckie commented Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Why falsum and implication as the primitives

Context

File-by-file change summary

Cslib.lean

Cslib/Foundations/Logic/Connectives.lean (new)

Cslib/Foundations/Logic/InferenceSystem.lean

Cslib/Logics/Propositional/Defs.lean

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

references.bib

AI Disclosure

Uh oh!

eric-wieser Jun 12, 2026

Choose a reason for hiding this comment

Uh oh!

ctchou commented Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ctchou commented Jun 12, 2026

Uh oh!

ctchou commented Jun 12, 2026

Uh oh!

benbrastmckie commented Jun 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

benbrastmckie commented Jun 12, 2026 •

edited

Loading

ctchou commented Jun 12, 2026 •

edited

Loading