Registry · Theorem VII.T28 tau-effective formalized

VII.T28 — Kripke Soundness in τ

Modal operators (necessity/possibility) sound with respect to Kripke semantics realized as quantification over accessible internal worlds.

Book VII Part 6 Ch. 73

Dependency Graph

Depends on (1)

VII.D62

Lean Formalization

Module: TauLib.BookVII.Ethics.CIProof

Symbol: Tau.BookVII.Ethics.CIProof.kripke_soundness