doc: add citation references for Lukasiewicz convention sources

Author: benbrastmckie

Cslib/Foundations/Logic/Connectives.lean

@@ -25,6 +25,13 @@ The hierarchy follows the Foundation pattern (FormalizedFormalLogic/Foundation):
 
 Each concrete formula type duplicates its constructors (Lean 4 cannot extend inductives)
 and registers as an instance of the appropriate bundled class.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Heyting, *Die formalen Regeln der intuitionistischen Logik*][Heyting1930]
+* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
 -/
 
 @[expose] public section

Cslib/Logics/Propositional/Defs.lean

@@ -34,6 +34,11 @@ theory.
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
 conjunction, disjunction, implication and negation.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
 -/
 
 @[expose] public section

Cslib/Logics/Propositional/NaturalDeduction/Basic.lean

@@ -49,11 +49,11 @@ the Lukasiewicz definitions of `∧` and `∨` in terms of `→` and `⊥`.
 
 ## References
 
-- Dag Prawitz, *Natural Deduction: a proof-theoretical study*.
-- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely
-presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*, and
-in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (Suggestions of better
-references welcome!)
+* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965]
+* [A. S. Troelstra, D. van Dalen,
+  *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988], Section 10.4
+* [G. Gentzen,
+  *Untersuchungen über das logische Schließen*][Gentzen1935]
 -/
 
 @[expose] public section

references.bib

@@ -49,6 +49,17 @@ @book{Blackburn2001
   collection={Cambridge Tracts in Theoretical Computer Science}
 }
 
+@book{ChagrovZakharyaschev1997,
+  author       = {Chagrov, Alexander and Zakharyaschev, Michael},
+  title        = {Modal Logic},
+  series       = {Oxford Logic Guides},
+  volume       = {35},
+  publisher    = {Oxford University Press},
+  address      = {Oxford},
+  year         = {1997},
+  isbn         = {978-0-19-853779-3}
+}
+
 @misc{Burghardt2018,
 	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
 	url = {https://arxiv.org/abs/1806.05036v2},
@@ -61,17 +72,6 @@ @misc{Burghardt2018
 	year = {2018},
 }
 
-@book{ChagrovZakharyaschev1997,
-  author       = {Chagrov, Alexander and Zakharyaschev, Michael},
-  title        = {Modal Logic},
-  series       = {Oxford Logic Guides},
-  volume       = {35},
-  publisher    = {Oxford University Press},
-  address      = {Oxford},
-  year         = {1997},
-  isbn         = {978-0-19-853779-3}
-}
-
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},
@@ -123,6 +123,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},
@@ -160,6 +170,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},
@@ -215,6 +236,15 @@ @article{         Hennessy1985
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{Heyting1930,
+  author       = {Heyting, Arend},
+  title        = {Die formalen Regeln der intuitionistischen Logik},
+  journal      = {Sitzungsberichte der Preu{\ss}ischen Akademie der
+                  Wissenschaften, physikalisch-mathematische Klasse},
+  year         = {1930},
+  pages        = {42--56}
+}
+
 @book{             KatzLindell2020,
   author       = {Jonathan Katz and
                   Yehuda Lindell},
@@ -307,6 +337,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},
@@ -348,6 +387,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},