Gamen.jl logo Gamen.jl / Notebooks

B&D Companion Notebooks

Interactive Pluto notebooks following Boxes and Diamonds (Zach 2025). Each notebook makes the textbook's definitions and exercises live — modify a formula or model and see all results update immediately. Use Binder to run them interactively, or browse the static versions below.

Chapters

  1. Ch 0 Propositional Logic Connectives, implications, tautologies, and the limits of propositional reasoning
  2. Ch 1 Syntax and Semantics Modal formulas, Kripke models, truth at a world, satisfiability and validity
  3. Ch 2 Frame Definability Reflexivity, symmetry, transitivity, seriality, euclideanness, and the T/B/4/D/5 schemas
  4. Ch 3 Axiomatic Derivations Hilbert-style proof systems, modal axioms, substitution, and derivability
  5. Ch 4 Completeness Canonical models, the Truth Lemma, Lindenbaum's Lemma, and completeness of K
  6. Ch 5 Filtrations and Decidability Filtrations, the finite model property, and decidability of modal logics
  7. Ch 6 Modal Tableaux Prefixed signed tableaux, automated proof search, consistency checking
  8. Ch 14 Temporal Logics Always (𝐆), eventually (𝐅), historically (𝐇), previously (𝐏); linear frames and temporal validity
  9. Ch 15 Epistemic Logics Knowledge operators Ka, S5 axioms, multi-agent knowledge, public announcements

Extension

  1. Ext Combined Deontic–Temporal Logic Obligations over time; the KDt system; combining deontic seriality with temporal operators
→ Health Application Notebooks