feat(references, Propositional): restore 7 bib entries and architecture docstring

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

Author: benbrastmckie

Cslib/Logics/Propositional/Defs.lean

@@ -34,6 +34,25 @@ public import Mathlib.Order.TypeTags
 - `Theory.intuitionisticCompletion` : the freely generated intuitionistic theory extending a given
   theory.
 
+## Architecture
+
+Two proof systems are defined for this propositional language:
+
+- **Layer 1 — Natural Deduction** (`NaturalDeduction/Basic.lean`): a `Theory.Derivation` inductive
+  with 10 primitive constructors (axiom, assumption, conjunction intro/elim ×2, disjunction
+  intro ×2/elim, implication intro/elim). The theory parameter controls logic strength: `MPL`
+  (Johansson's minimal logic, [Johansson1937]), `IPL` (intuitionistic), and `CPL` (classical).
+
+- **Layer 2 — Hilbert System** (`ProofSystem/`): an axiom predicate hierarchy
+  (`MinPropAxiom` / `IntPropAxiom` / `PropositionalAxiom`) with sequent derivability and a
+  Hilbert-style proof-theoretic treatment.
+
+- **Bridge**: `NaturalDeduction/Equivalence.lean` establishes extensional equivalence between the
+  two proof systems for all three logic strengths, in both closed-context (`hilbert_iff_nd`,
+  `hilbert_iff_nd_min`, `hilbert_iff_nd_int`, `hilbert_iff_nd_cl`) and context-based forms
+  (`hilbert_iff_nd_ctx`, `hilbert_iff_nd_ctx_min`, `hilbert_iff_nd_ctx_int`,
+  `hilbert_iff_nd_ctx_cl`).
+
 ## Notation
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,

references.bib

@@ -112,6 +112,16 @@ @misc{         WikipediaMyhillNerode2026
   note         = {[Online; accessed 9-April-2026]}
 }
 
+@book{Church1956,
+  author       = {Church, Alonzo},
+  title        = {Introduction to Mathematical Logic},
+  volume       = {1},
+  publisher    = {Princeton University Press},
+  address      = {Princeton},
+  year         = {1956},
+  isbn         = {978-0-691-02906-1}
+}
+
 @article{         Chargueraud2012,
 	title = {The {Locally} {Nameless} {Representation}},
 	volume = {49},
@@ -149,6 +159,17 @@ @article{ FLP1985
   numpages  = {9}
 }
 
+@article{Gentzen1935,
+  author       = {Gentzen, Gerhard},
+  title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}},
+  journal      = {Mathematische Zeitschrift},
+  volume       = {39},
+  number       = {1},
+  pages        = {176--210},
+  year         = {1935},
+  doi          = {10.1007/BF01201353}
+}
+
 @article{        Girard1987,
   title={Linear logic},
   author={Girard, Jean-Yves},
@@ -204,6 +225,37 @@ @article{         Hennessy1985
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{Johansson1937,
+  author       = {Johansson, Ingebrigt},
+  title        = {Der Minimalkalk{\"u}l, ein reduzierter intuitionistischer Formalismus},
+  journal      = {Compositio Mathematica},
+  volume       = {4},
+  pages        = {119--136},
+  year         = {1937},
+  url          = {http://www.numdam.org/item/CM_1937__4__119_0/}
+}
+
+@article{McKinsey1939,
+  author       = {McKinsey, J. C. C.},
+  title        = {Proof of the Independence of the Primitive Symbols of {H}eyting's Calculus
+                  of Propositions},
+  journal      = {Journal of Symbolic Logic},
+  volume       = {4},
+  number       = {4},
+  pages        = {155--158},
+  year         = {1939},
+  doi          = {10.2307/2268715}
+}
+
+@article{Wajsberg1938,
+  author       = {Wajsberg, Mordchaj},
+  title        = {Untersuchungen {\"u}ber den Aussagenkalk{\"u}l von {A}. {H}eyting},
+  journal      = {Wiadomo{\'s}ci Matematyczne},
+  volume       = {46},
+  pages        = {45--101},
+  year         = {1938}
+}
+
 @book{             KatzLindell2020,
   author       = {Jonathan Katz and
                   Yehuda Lindell},
@@ -296,6 +348,15 @@ @Book{            Montesi2023
   keywords      = {choreographic-programming,choreographic-language,choreography,concurrency-theory}
 }
 
+@book{Prawitz1965,
+  author       = {Prawitz, Dag},
+  title        = {Natural Deduction: A Proof-Theoretical Study},
+  publisher    = {Almqvist \& Wiksell},
+  address      = {Stockholm},
+  year         = {1965},
+  note         = {Reprinted by Dover Publications, 2006}
+}
+
 @article{         Nipkow2001,
   title        = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
   author       = {Nipkow, Tobias},
@@ -337,6 +398,18 @@ @Book{            Sangiorgi2011
   doi           = {10.1017/CBO9780511777110}
 }
 
+@book{TroelstraVanDalen1988,
+  author       = {Troelstra, A. S. and van Dalen, D.},
+  title        = {Constructivism in Mathematics: An Introduction},
+  volume       = {1},
+  series       = {Studies in Logic and the Foundations of Mathematics},
+  number       = {121},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  year         = {1988},
+  isbn         = {978-0-444-70506-8}
+}
+
 @incollection{ Thomas1990,
   author       = {Wolfgang Thomas},
   editor       = {Jan van Leeuwen},