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

[benbrastmckie]

Summary

Revises PR #648 based on reviewer feedback. Adds bot as a primitive constructor of Proposition, eliminating all [Bot Atom] constraints. Rebased on upstream/main post-#536.

Key changes from #648:

• bot is a primitive constructor (not an atom), so IsIntuitionistic/IsClassical no longer require [Bot Atom]
• 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 files removed per thomaskwaring's request (deferred to follow-up PR)
• German-language references replaced with English alternatives (Avigad 2022)

New files

• Cslib/Foundations/Logic/Connectives.lean -- typeclass hierarchy (HasBot, HasImp, HasAnd, HasOr, PropositionalConnectives)

Modified files

• Cslib/Logics/Propositional/Defs.lean -- Proposition with primitive bot; derived neg, top, iff; typeclass instances
• Cslib/Logics/Propositional/NaturalDeduction/Basic.lean -- derivation constructors updated to impI/impE, andE1/andE2, orI1/orI2; explicit Γ arguments
• Cslib/Logics/Propositional/NaturalDeduction/Theory.lean -- [Bot Atom] removed from all signatures; added instIsIntuitionisticIntuitionisticCompletion
• Cslib.lean -- added Connectives import
• references.bib -- added Avigad2022 entry

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.

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): Both PRs define operator typeclasses, but this PR uses HasImp/imp while feat(Logic): logical operators #607 uses HasImpl/impl.
• PR feat(Foundations/Logic): Notation typeclasses and models #587 (thomaskwaring): Both PRs create Cslib/Foundations/Logic/Connectives.lean with different content. Semantics are deferred here so no conflict on models, but the file path needs coordination. Proposing a joint design thread before either PR's next revision.

Deferred

Semantics (Basic.lean, Bool.lean) deferred to a follow-up PR per thomaskwaring's request. The question of Prop vs Bool vs GeneralizedHeytingAlgebra for evaluation (raised by thomaskwaring and ctchou) will be addressed there.

AI Tools Used

Claude Code was used to rebase, resolve merge conflicts, adapt proofs for primitive bot and imp naming, and verify CI. All mathematical decisions reviewed by the human author.

[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!