Email Gateway (Jun 05 2026 at 16:06): Email Gateway (Jun 05 2026 at 16:06):From: Tobias Nipkow <nipkow@in.tum.de>
Mechanized Metasemantics of Modal Necessity: Valuation Factorization and Modal
Non-Collapse
Yong-Dock Kim
This formalization develops a mechanized metasemantics for modal necessity in
Isabelle/HOL. Its core construction factorizes Kripke-style valuation as V = I o
delta, where delta maps object-language formulas to syntactic distinctions and I
maps such distinctions to possible-worlds truth-conditions. Thus modal
evaluation is carried out over interpreted distinctions rather than over
valuation alone. The development provides three witnesses. First, a concrete
satisfiability witness shows that the abstract interpretive-structure locale is
jointly satisfiable. Second, a nontrivial truth-condition witness shows that
I0(delta0(Atom 0)) separates the two worlds of the concrete model. Third, a
no-collapse witness proves that Dia (Atom 0) w holds while Box (Atom 0) w fails.
The development introduces no additional global axioms; its locale assumptions
are discharged by an explicit concrete model. Hence the framework is
non-vacuous, nontrivial, and non-collapsing. This shows that, in the present
framework, modal force is not a feature of bare syntax alone, but is grounded in
syntactic distinctions only insofar as they are interpreted as possible-worlds
truth-conditions.
https://isa-afp.org/entries/Mechanized_Metasemantics.html
Enjoy!
Last updated: Jun 12 2026 at 04:13 UTC