Registry · Theorem VII.T13 tau-effective formalized

VII.T13 — Modal Logic Soundness in τ

Internal modal logic with Box/Diamond is sound with respect to Kripke semantics; τ grounds modal reasoning.

Book VII Part 2 Ch. 25

Dependency Graph

Depends on (1)

VII.D33

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.modal_logic_soundness