feat(Foundations/Logic): propositional theorems, modal S5 theorems, and MCS consistency foundations#629
Closed
benbrastmckie wants to merge 4 commits into
Closed
Conversation
…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>
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>
- 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>
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>
benbrastmckie
requested review from
arademaker,
chenson2018 and
fmontesi
as code owners
Author
|
Closing to resubmit as a combined PR that includes both the original Foundations/Logic content and the subsequent propositional Hilbert additions (ND-Hilbert equivalence, intuitionistic base hierarchy, derived connective rules). |
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 11, 2026
Combined PR 1+1.5 submitted as PR leanprover#630. Closed PR leanprover#629. All CI checks pass: build, test, lint, checkInitImports, lint-style, mk_all, shake. Session: sess_1781153904_261d3f
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 11, 2026
Combined PR 1+1.5 submitted as PR leanprover#630. Closed leanprover#629. All CI checks passed: lake build, test, lint, checkInitImports, lint-style, mk_all, shake. Session: sess_1781153904_261d3f
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 14, 2026
Combined PR 1+1.5 submitted as PR leanprover#630. Closed PR leanprover#629. All CI checks pass: build, test, lint, checkInitImports, lint-style, mk_all, shake. Session: sess_1781153904_261d3f
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jun 14, 2026
Combined PR 1+1.5 submitted as PR leanprover#630. Closed leanprover#629. All CI checks passed: lake build, test, lint, checkInitImports, lint-style, mk_all, shake. Session: sess_1781153904_261d3f
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Superseded by #630, then by #633. See #635 for the extracted sub-PR.