Sophie's World - UFPL Notes (Lean 4)

A small Lean/UFPL notebook that formalizes bite‑sized ideas from Sophie's World as multi‑modal logic formulas and toy models.

• UFPL: typed terms, first‑order formulas, and modalities: alethic (□/◇), epistemic (K/B), deontic (Obl), temporal (G/F/H/P), with both Prop semantics (sat) and an executable Boolean semantics (satB). We use satB for quick checks. Source: UFPL repo.
• Build: lake build - Run: lake exe sw.

Layout

SophiesWorld/Core/Signature.lean  # shared predicates
SophiesWorld/Core/Model.lean      # one tiny shared model + EvalSupport
SophiesWorld/Examples/Kant.lean   # Obl (promise‑keeping)
SophiesWorld/Examples/Socrates.lean

References

• UFPL (library & semantics): see repo's README.
• Lake/TOML project setup: Lean docs.