doc: fix docstrings for primitive bot perspective

Update intuitionisticCompletion docstring — the old wording "Attach a
bottom element" was misleading since bot is already a constructor.
Change "five-primitive propositional signature" to "five constructors"
in Connectives.lean to avoid conflating generators with operations.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: benbrastmckie

Cslib/Foundations/Logic/Connectives.lean

@@ -16,7 +16,7 @@ axiom definitions and notation that work uniformly across different formula type
 
 ## Design
 
-The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`,
+The hierarchy adopts five constructors `{atom, bot, imp, and, or}`,
 following the operator-typeclass direction of fmontesi's PR #607 (one class per operator):
 - **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`
 - **Bundled class**: `PropositionalConnectives` (extends `HasBot` and `HasImp`)

Cslib/Logics/Propositional/Defs.lean

@@ -142,7 +142,9 @@ abbrev CPL : Theory Atom :=
 omit [DecidableEq Atom] in
 lemma dne_mem_cpl (A : Proposition Atom) : (¬¬A → A) ∈ CPL (Atom := Atom) := ⟨A, rfl⟩
 
-/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
+/-- Extend a theory `T` to an intuitionistic theory over a larger atom type by adding the principle
+of explosion. The atom type is extended with `WithBot` to ensure the result is over a strictly
+larger language. -/
 @[reducible]
 def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
   (WithBot.some <$> T) ∪ IPL