feat: add Logics/Propositional/NaturalDeduction/* by thomaskwaring · Pull Request #91 · leanprover/cslib

thomaskwaring · 2025-10-09T14:28:33Z

Natural deduction for minimal logic

This PR adds the definitions and basic properties of natural deduction for propositional logic.

Key developments:

Definition of Theory.Derivation, the type of derivation trees.
Definitions of derivability and equivalence.
Operations on derivations: weakening, substitution and cut.

## Summary - Updates `bump_toolchain_nightly-testing.yml` to change the mathlib dependency name from `mathlib` to `mathlib-nightly-testing` in `lakefile.toml` - This ensures the workflow correctly references the nightly-testing variant of mathlib, not just updating the rev ## Changes - Added `sed` command to update `name = "mathlib"` to `name = "mathlib-nightly-testing"` - This runs alongside the existing `rev` update ## Test plan - [ ] Verify the workflow runs successfully on the next scheduled execution or manual trigger - [ ] Confirm `lakefile.toml` on `nightly-testing` branch has both correct name and rev after workflow runs 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>

…eanprover#99) ## Summary - Validates lakefile.toml has git-based mathlib4-nightly-testing dependency - Updates only the `rev` field (not `name` field) - Fails if dependency not in expected git-based format This avoids Reservoir by assuming nightly-testing branch already uses git field. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>

Add repository checks to nightly-testing workflows to prevent them from running in forks.

Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

[x] Introduce the namespace `Cslib` for all `Cslib` files [x] Introduce the namespace `CslibTests` for all `CslibTests` files [x] Fix the inconsistencies in linebreaks for all namespace related declarations [x] Use the convention that the namespace begins one line after the module docstring. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

…prover#102) Normally we check that our library and documentation are using the same `lean-toolchain`. However the [nightly testing workflow](.github/workflows/merge_main_into_nightly-testing.yml) by design is meant to test a toolchain ahead of our current pinned version. To accommodate this, this PR changes the doc toolchain check to only happen during pull requests and commits to the `main` branch.

Note that in Mathlib we actually enforce in CI that everything in scripts/ is documented in this file. Not implemented here.

This is the initial version of ωSequence with reference to: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Automata/near/543709917 --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>

closes leanprover#108

…eanprover#112)

`ωSequence.flatten` is analogous to `List.flatten`: it concatenates an infinite sequence of (finite) lists to form an infinite sequence.

…decidability (leanprover#113) This file did not depend on Mathlib, which given the use of `weak` in `lakefile.toml` meant that this was silently not linted. There are three other files for which this is true: ``` Cslib.Foundations.Syntax.HasAlphaEquiv Cslib.Foundations.Syntax.HasSubstitution Cslib.Foundations.Syntax.HasWellFormed ``` but they only define notation typeclasses and have no lint problems. While here, I also took the opportunity to make a decidability proof easier to read.

This pull request extends the development of SKI combinatory logic — adding notions of evaluation and normal forms, and proving a version of [Rice's theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem). The results and definitions are contained in the new file `CombinatoryLogic/Evaluation.lean`, which is based heavily on the [following development](https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166) by Bhavik Mehta. ### Notes The definitions and results of this PR allows us to define normal-order evaluation as a `PFun`, in [the sense of Mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFun.html). The missing piece to make this useful is the so-called _Standardisation theorem_, saying that normal-order reduction will find a normal form, if there is one. The proof of Theorem T9 of Section C in _A Mathematical Logic Without Variables_ (Rosser, 1935) should be amenable to formalization. This would be very interesting, as it ought to define a surjection from SKI terms to, for instance, [partial recursive functions](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/Partrec.html) on the natural numbers, demonstrating that SKI terms are Turing-complete. --------- Co-authored-by: twwar <tom.waring@unimelb.edu.au> Co-authored-by: Maximiliano Onofre-Martínez <maxonomar@ciencias.unam.mx> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Fabrizio Montesi <famontesi@gmail.com> Co-authored-by: Tristan F.-R. <pub.tristanf@gmail.com> Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: euprunin <euprunin@users.noreply.github.com> Co-authored-by: kei <70096720+thelissimus@users.noreply.github.com> Co-authored-by: Juan Pablo Yamamoto <jpy051@uregina.ca> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: Clark Barrett <barrett@cs.stanford.edu> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

[This commit](leanprover-community/mathlib4@ed4fde1#diff-54ef6c59abdddf67950b1ee785a0c22c7e03d04f9ad8cdb7cf1d336a72f4d850) in mathlib4 moves `foldl_eq_foldr` to another module, so we need to import it or the build fails with ```lean error: Cslib/Computability/URM/Basic.lean:178:27: Unknown constant `List.foldl_eq_foldr` ``` This PR updates the lake manifest past this commit with `lake update mathlib` and fixes the issue

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com> Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com> Co-authored-by: Alexandre Rademaker <arademaker@gmail.com> Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>

fmontesi

Looks good to me now, just minor easy nitpicks about names.

twwar added 5 commits October 8, 2025 13:07

define proposition, theory

6555b17

definition and basics of natural deductions

eaf5d24

substitution

8d7c530

extensions of theories

cdde61f

docs

2b6a79c

thomaskwaring requested a review from fmontesi as a code owner October 9, 2025 14:28

scope grinds, lemmas

4110032

thomaskwaring force-pushed the nj-deduction branch from af39522 to 4110032 Compare October 11, 2025 11:58

thomaskwaring mentioned this pull request Oct 11, 2025

feat: Heyting algebra semantics for propositional logic #93

Open

twwar and others added 21 commits April 6, 2026 15:43

update defs

b950b53

scope grinds, lemmas

5630d56

edits

9f1c5bb

classical logics don't need explicit efq

fe15f1f

grind patterns

e21755a

modules?

5f48a6e

chore: fix CI step that bumps nightly-testing toolchain (leanprover#96)

263d917

chore: install lake in bump nightly-testing toolchain CI (leanprover#97)

c370571

chore: skip nightly-testing workflows in forks (leanprover#100)

f9788fb

Add repository checks to nightly-testing workflows to prevent them from running in forks.

chore: bump toolchain to v4.24.0 (leanprover#103)

a407068

Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

chore: add scripts/README.md (leanprover#106)

c4dd839

Note that in Mathlib we actually enforce in CI that everything in scripts/ is documented in this file. Not implemented here.

feat: add Cslib/Foundations/Data/OmegaSequence/* (leanprover#90)

23fcdda

This is the initial version of ωSequence with reference to: https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Automata/near/543709917 --------- Co-authored-by: Fabrizio Montesi <famontesi@gmail.com>

feat(CI): add workflow to check for commit convention (leanprover#110)

b68ffcc

closes leanprover#108

chore: add namespace Cslib to Cslib/Foundations/Data/OmegaSequence (l…

e774d05

…eanprover#112)

feat: Flattening operation on OmegaSequence (leanprover#111)

9786a02

`ωSequence.flatten` is analogous to `List.flatten`: it concatenates an infinite sequence of (finite) lists to form an infinite sequence.

marcelolynch and others added 2 commits April 6, 2026 15:57

thomaskwaring requested review from chenson2018 and kim-em as code owners April 6, 2026 13:57

twwar and others added 13 commits April 6, 2026 16:15

merge

0f474c7

Merge branch 'main' into nj-deduction

5785c5a

Merge branch 'main' into nj-deduction

1bb1215

defer theory ordering to later pr

db8c7bc

docs & lint

641d719

docs

e187d4f

docs again

488711b

inference system

9874a75

proposition as a functor

8df78b7

docs

a78ab0b

generalise Derivation.subs, tidy up

4fcbceb

more consistent namespacing

7d494b1

implementation note

c436dee

arademaker reviewed Apr 19, 2026

View reviewed changes

Comment thread Cslib/Logics/Propositional/NaturalDeduction/Basic.lean Outdated

Comment thread Cslib/Logics/Propositional/NaturalDeduction/Basic.lean Outdated

twwar and others added 5 commits April 19, 2026 17:51

naming, universes

aa41f02

Merge branch 'leanprover:main' into nj-deduction

ce2ba33

update to tagged inference system

7553c45

docs

223c13d

fix inductive indexes

bf79049

fmontesi requested changes Apr 29, 2026

View reviewed changes

Comment thread Cslib/Logics/Propositional/NaturalDeduction/Basic.lean Outdated

Comment thread Cslib/Logics/Propositional/NaturalDeduction/Basic.lean Outdated

Comment thread Cslib/Logics/Propositional/NaturalDeduction/Basic.lean Outdated

Comment thread Cslib/Logics/Propositional/Defs.lean Outdated

thomaskwaring force-pushed the nj-deduction branch from 83bb811 to bf79049 Compare April 29, 2026 15:34

naming and docs

58c8545

fmontesi approved these changes Apr 29, 2026

View reviewed changes

fmontesi added this pull request to the merge queue Apr 29, 2026

Merged via the queue into leanprover:main with commit 6d112db Apr 29, 2026
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add Logics/Propositional/NaturalDeduction/*#91

feat: add Logics/Propositional/NaturalDeduction/*#91
fmontesi merged 218 commits intoleanprover:mainfrom
thomaskwaring:nj-deduction

thomaskwaring commented Oct 9, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

fmontesi left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

Conversation

thomaskwaring commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Natural deduction for minimal logic

Uh oh!

Uh oh!

Uh oh!

fmontesi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

thomaskwaring commented Oct 9, 2025 •

edited

Loading