一句话：将轻量 Dialectica 解释扩展到模态公式，并证明其对基于 Gödel T 与经典 S4 的非标准模态算术可靠。
本文把轻量 Dialectica 解释扩展到通常与轻量模态公式（含布尔和自然数变量全称量化），并证明其对基于 Gödel T 与经典 S4 的非标准模态算术可靠。轻量模态 Dialectica 的目标是通常的非模态有限类型经典算术（含布尔类型），其命题核心为布尔而非 S4。作者提出“重”模态 Dialectica：该技术无法在原有轻量解释中模拟，合成泛函不劣于旧法而翻译过程更优。最后，经典 S5 定义公理的 realizer 存在性被归约为 Smullyan 的饮酒原则。
We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standard modal arithmetic based on Goedel's T and classical S4. The range of this light modal Dialectica is the usual (non-modal) classical Arithmetic in all finite types (with booleans); the propositional kernel of its domain is Boolean and not S4. The `heavy' modal Dialectica interpretation is a new technique, as it cannot be simulated within our previous light Dialectica. The synthesized functionals are at least as good as before, while the translation process is improved. Through our modal Dialectica, the existence of a realizer for the defining axiom of classical S5 reduces to the Drinking Principle (cf. Smullyan).