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

[benbrastmckie]

Summary

Revises PR #648 based on reviewer feedback (thomaskwaring, msg 606970606). Adds bot as a primitive constructor of Proposition (eliminating all [Bot Atom] constraints) and makes IPL the base logic by taking ex falso quodlibet as a primitive natural-deduction rule. Rebased on upstream/main post-#536.

Key changes from #648:

• bot is a primitive constructor (not an atom), so explosion and IsClassical no longer require [Bot Atom]
• Ex falso quodlibet is now a primitive rule (efq constructor of Derivation), so ⊥ has an inference rule and IPL is the base logic; minimal logic (MPL) is set aside for a separate PR/discussion, per the agreed compromise
• Reconciled with merged PR refactor(Logics/Propositional): classical and intuitionistic inference systems #536's InferenceSystem-parameterized typeclasses
• Constructor naming uses imp/impI/impE (renamed from impl/implI/implE for consistency with FormalizedFormalLogic convention; open to reverting if reviewers prefer impl)
• Semantics not included — deferred to a follow-up PR (per thomaskwaring's request)
• Connective typeclasses removed — a separate development coordinated via PR feat(Logic): logical operators #607 (this PR no longer ships Connectives.lean)
• References include Avigad 2022, Gentzen 1935, Prawitz 1965, and Troelstra & van Dalen 1988, and a link to the CSLib Zulip design thread is added

Modified files

• Cslib/Logics/Propositional/Defs.lean -- Proposition with primitive bot; derived neg, top, iff; IPL is the empty base theory and CPL adds double-negation elimination (the MPL / IsIntuitionistic / intuitionisticCompletion layer is set aside for the minimal-logic PR)
• Cslib/Logics/Propositional/NaturalDeduction/Basic.lean -- derivation constructors impI/impE, andE1/andE2, orI1/orI2 with explicit Γ arguments, plus the new primitive efq (⊥-elimination); implementation notes, references, and Zulip-thread link
• Cslib/Logics/Propositional/NaturalDeduction/Theory.lean -- [Bot Atom] removed; the classical layer (IsClassical, byContra/lem/pierce, and the CPL/LEM/Pierce instances) re-proved over the new base via the efq constructor
• references.bib -- added Avigad2022, Gentzen1935, Prawitz1965, TroelstraVanDalen1988

Design rationale

Primitive bot eliminates [Bot Atom] constraints throughout the propositional logic API, gives Proposition.subst a natural recursive case for bot, and follows the standard treatment in Avigad (2022) where bot is a logical constant rather than an atomic proposition. The trade-off (noted by thomaskwaring) is an extra bot case in structural recursions. Relatedly, taking ex falso as a primitive rule rather than leaving ⊥ a constructor with no inference behaviour follows the standard natural-deduction treatment (Gentzen 1935, Prawitz 1965, Troelstra & van Dalen 1988) and is thomaskwaring's recommendation; minimal logic — the efq-free fragment — is deferred so the fragment design can be settled on its own.

These benefits extend to planned completeness work for modal and temporal logics: primitive bot ensures Proposition.subst preserves bottom structurally (subst f .bot = .bot), whereas atom-encoded bot requires additional constraints to prevent subst f (.atom ⊥) = f ⊥ from mapping bottom to an arbitrary formula. As thomaskwaring notes, non-bottom-preserving maps are also useful (e.g., conservativity results via WithBot.some).

Coordination

• PR feat(Logic): logical operators #607 (fmontesi): connective typeclasses are a separate development; this PR no longer ships its own Connectives.lean. One design point for feat(Logic): logical operators #607: it makes negation primitive (HasNot) with no ⊥/⊤ class, but a ⊥-primitive Proposition (where ¬φ := φ → ⊥ and ⊤ := ⊥ → ⊥) registers faithfully by reusing Mathlib's Bot/Top together with a derived HasNot (not := neg) and a (φ → ⊥) = ¬φ grind bridge — no separate HasBot class needed. I'll leave a review on feat(Logic): logical operators #607.

Deferred

• Minimal logic (MPL) + fragment design -- a separate PR/discussion (the agreed deferral).
• Semantics (Bool.lean, evaluation) -- follow-up PR; the Prop vs Bool vs GeneralizedHeytingAlgebra question (raised by thomaskwaring and ctchou) will be addressed there.
• Hilbert systems, sequent calculi, and tableau -- stacked PRs.

AI Tools Used

Claude Code was used to refactor for primitive efq/IPL-base, remove the connective typeclasses and the minimal-logic layer, rebase onto upstream/main and resolve the references.bib conflict, and verify CI. All mathematical decisions reviewed.

[ctchou]

Some general comments:

• I like the idea of adding \bot as a primitive.
• I don't understand why we need both Semantics/Basic.lean and Semantics/Bool.lean. I think the latter alone is enough. Later we can add (for example) Kripke semantics for intuitionistic propositional logic.
• It is not helpful to the readers to refer to old papers from the 1930s, some of which are in German. A good modern reference is Jeremy Avigad's textbook:
  https://www.cambridge.org/core/books/mathematical-logic-and-computation/300504EAD8410522CE0C27595D2825A2
  whose chapters 2 and 3 covers everything in this PR.
• You should definitely coordinate this PR with #607 abd #587. #536 is ready to merge, so you should wait for it.

[thomaskwaring]

I think the refactor to Propositional/* you suggest could be workable, but I have a few concerns (note that while having falsum as a primitive is more conventional, the current design was discussed fairly thoroughly).

• If ⊥ is included in minimal logic it behaves precisely like the atomic formulae, so why not represent it as such?
• Minimal logic works perfectly well without ⊥ — this is the approach taken in Lectures on the Curry-Howard Correspondence for example. I don't think having [Bot Atom] assumptions where necessary is a big deal.
• Adding an extra constructor makes all the proofs, and more importantly definitions, more verbose. EG in your semantics development you have to have separate fields in the Kripke structure for the entailment relation on atoms and ⊥, which are exact duplicates.
• I see your point about substitution, but I think it is sometimes important to consider maps which don't preserve the bottom. For example, the informal statement "intuitionistic logic is conservative over minimal logic" translates to "minimal logic proves all statements that don't mention ⊥". The most sensible way to spell this (to me) would be to consider the map WithBot.some : Atom → WithBot Atom and consider mapping formulas / derivations along that. (Another analogy I have in mind is domain theory, where even if your domains have a bottom element, it's important to consider functions which may not preserve it. The correspondence there is a little loose though.)
• I think the ⊤ element being a → a for an arbitrary formula is a feature not a bug — proofs about ⊤ should only depend on the fact that it is provable, not on the specific definition. Note that lean synthesises default = ⊥ anyway, as an example shows.

Re the renaming imp / impl, I think this is fine, but citing "CSLib's existing formula types" as your own as-yet-unmerged work is not exactly convincing. Indeed the actually existing example (Modal) uses "impl".

Please split the semantics development into a separate PR. The point of requesting that large contributions are split up is not just length, but also so that conceptually separate issues can be discussed independently. FWIW, as I mentioned on zulip, imo the right way to resolve the Bool / Prop issue is to define the interpretation in any (generalised) Heyting algebra — this captures both of those as well as non-classical versions, and the proofs of soundness are no harder. Also, your proof of Evaluate_eq_BoolEvaluate, ie that the valuation into Prop factors through Bool, would work for any morphism of Heyting algebras.

Re the references, I agree with @ctchou about citing literature in English — the Gentzen paper is my bad, I read it in translation (in "The Collected Papers of Gerhard Gentzen" ed M. E. Szabo).

[benbrastmckie]

@ctchou @thomaskwaring Thank you both for the thoughtful feedback — I've reworked the PR to address each point.

Changes made:

• Rebased on upstream/main now that refactor(Logics/Propositional): classical and intuitionistic inference systems #536 is merged, and reconciled IsIntuitionistic/IsClassical with the InferenceSystem-parameterized versions from refactor(Logics/Propositional): classical and intuitionistic inference systems #536 (removing [Bot Atom] since bot is now primitive).
• Semantics files (Basic.lean, Bool.lean) removed from this PR as Thomas requested — I'll address the Prop/Bool/GeneralizedHeytingAlgebra question in a follow-up. Thomas, your suggestion of defining the interpretation for any GeneralizedHeytingAlgebra is elegant and I'd like to explore that direction.
• German-language references replaced with Avigad (2022) per ctchou's suggestion.
• Added Connectives.lean with per-operator typeclasses (HasBot, HasImp, HasAnd, HasOr) aligned with fmontesi's feat(Logic): logical operators #607.

On the imp vs impl naming: I renamed to imp for consistency with FormalizedFormalLogic, but I'm happy to revert to impl if you both prefer that. Thomas, you're right that Modal uses impl — I don't want to create unnecessary inconsistency.

On bot as primitive vs atom: The key distinction is that in minimal logic bot is an unconstrained logical constant (a nullary operator), not an atom — no axioms constrain its denotation, but it's fixed under substitution. With primitive ⊥, subst has | .bot => .bot and axiom scheme closure is automatic. With bot-as-atom, every substitution theorem acquires a side condition σ(⊥) = ⊥ and the free monad on Atom is no longer free. The bot_val parameter gives interpretive freedom without substitutability; bot-as-atom gives both, which is more than the mathematics calls for. Practically, [Bot Atom] constraints also accumulate through every signature in the strong completeness work for propositional, modal, and bimodal logics, making the API noticeably heavier. The trade-off is an extra constructor case in recursions and the bot_val parameter in algebraic semantics, but I think these are the right costs. More on this on Zulip.

On top: The current definition is top := ⊥ → ⊥ — the old a → a definition required [Inhabited Atom]. Both are provable by the same proof (impI + assumption), and as you noted, with [Bot Atom] Lean synthesises default = ⊥ anyway, so they coincide in that setting.

Looking forward to your thoughts on the revised version!

[benbrastmckie]

Thanks for the review, @ctchou. I've reworked the PR and narrowed its scope considerably since you looked at it. Here's how it stands against your comments:

Scope and semantics. Following the design discussion with Thomas Waring on the CSLib Zulip thread, #648 is now just the IPL-base foundation: ⊥ is a primitive constructor and efq (⊥-elimination) is a primitive rule, so IPL is the base logic. Per that discussion I've set minimal logic and the fragment design aside for follow-up PRs so they can be worked out properly rather than rushed here. As part of that, I've removed both semantics files (Semantics/Basic.lean and Semantics/Bool.lean) from this PR and deferred the semantics to a later PR — which also resolves your point about not needing both. The PR is now four files: Defs.lean, the two NaturalDeduction/ files, and references.bib.

References. I've added Avigad's textbook as the lead modern reference — it's cited first in both the implementation notes and the reference list. I've kept Gentzen, Prawitz, and Troelstra & van Dalen, but de-emphasized Gentzen (now last) and replaced its German title with an English gloss, so the 1930s German paper is no longer quoted. Happy to drop it entirely if you'd prefer.

Coordination. #536 has merged and this branch is rebased on top of it. Removing the semantics and the connective typeclasses from #648 also removes its overlap with #587 (notation typeclasses and models) and #607 (logical operators), which were the main points of contact; I'll leave reviews on those to help them land.

Happy to wait for other maintainers' input on the ⊥/efq design before a full re-review.