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!

[thomaskwaring]

this looks pretty good to me! i'd like opinions from other logic contributors, but on the whole i'd be happy for this to be merged.

[thomaskwaring]

i think the comment about not needing an axiom for explosion is unnecessary & possibly confusing

[benbrastmckie]

Done — removed that clause from the module docstring.

[thomaskwaring]

the part about "primitives" is i think covered by the docstrings of the constructors

[benbrastmckie]

Done — dropped the "Primitives:" list; it's covered by the constructor docstrings.

[thomaskwaring]

are the explicit arguments necessary here? if so what broke about the old proof?

[benbrastmckie]

Good catch — the explicit arguments weren't necessary on the simple recursive arms, so I've reverted those to plain constructor patterns (matching substAtom). I kept the explicit binders only on the orE/impI arms, where A'/B'/Γ are referenced by name in the show rewrites. Builds cleanly.

[thomaskwaring]

i don't have a strong opinion on imp vs impl, so long as after #607 lands it is consistent across the library (noting eg Modal has impl also)

[benbrastmckie]

Agreed — leaving imp as-is for now; I'll reconcile the naming with the rest of the library once #607 lands.

[thomaskwaring]

no need for the comment about inference rule vs axiom here — that was only relevant for the old design which has no trace in the current file, so i think it just adds potential for confusion

[benbrastmckie]

Done — removed that note from the IPL docstring.