feat(Foundations/Logic, Logics/Propositional): Hilbert proof systems, metalogic, ND equivalence, and Kripke semantics#633

Closed

benbrastmckie wants to merge 19 commits into

leanprover:mainfrom

benbrastmckie:pr1/foundations-logic

Commits on Jun 11, 2026

feat(Logics/Propositional): add Hilbert-ND equivalence, derived rules, and intuitionistic hierarchy
benbrastmckie
committed
fix(NaturalDeduction/FromHilbert): remove unused DecidableEq parameter
benbrastmckie
committed
chore(Cslib): reorder imports per mk_all canonical order
benbrastmckie
committed
Merge remote-tracking branch 'upstream/main' into pr1/foundations-logic
benbrastmckie
committed
feat(Logics/Propositional): add semantics, metalogic, and cross-logic embeddings
benbrastmckie
committed
feat(Logics/Propositional): parameterize proof system and ND equivalence over axiom sets
benbrastmckie
committed
chore(Cslib): add propositional metalogic and embedding imports
benbrastmckie
committed
fix(Logics): remove FromPropositional files incompatible with branch Modal/Temporal types
benbrastmckie
committed
task 122: fix propositional CI check failures on main
benbrastmckie
committed
Merge remote-tracking branch 'upstream/main' into pr1/foundations-logic
benbrastmckie
committed
task 123 phase 2: update propositional logic references
benbrastmckie
committed
task 123 phase 3: add modal logic references sections
benbrastmckie
committed
task 123 phase 4: fix line-length warnings and verify build
benbrastmckie
committed
task 136: citation conformance edits

benbrastmckie
and
claude
committed

Commits on Jun 12, 2026

task 166: apply syntactic sugar to PR #633 Propositional files
benbrastmckie
committed