Interpretation of Hybrid Counterfactual Logic into Hybrid Tense Logic: and Comparison of Their Expressive Power on Temporal Sphere Models

Lewis (Noûs 13:455–476, 1979) claimed that branching-time(-like) models can be derived from his sphere models. However, he did not present any specific construction of branching-time(-like) models from his sphere models formally. Meanwhile, Hosokawa (in: Modern logic of modality and its philosophical range: counterfactuals, Gettier problem, and information flow, Tokyo Metropolitan University, 2018) presented a logico-mathematically strict manner in which sphere models can be reconstructed from branching-time models. Subsequently, Hosokawa (J Logic Lang Inf 32:677–706, 2023) presented a proof-theoretically refined version of hybrid tense logic for a certain type of conditionals, which is referred to as hybrid tense logic for temporal conditionals ( \(\textbf{HTL}_{TC}\) ${\mathbf{HTL}}_{\mathit{TC}}$ ). In this paper, we interpret a hybrid version \({\textbf{V}}_{\mathcal {HC(@, \downarrow )}}\) ${\mathbf{V}}_{\mathcal{HC}(@,\downarrow )}$ of Lewis’s counterfactual logic \({\textbf{V}}\) $\mathbf{V}$ into \(\textbf{HTL}_{TC}\) ${\mathbf{HTL}}_{\mathit{TC}}$ , and then prove that \(\textbf{HTL}_{TC}\) ${\mathbf{HTL}}_{\mathit{TC}}$ is more expressive than \({\textbf{V}}_{\mathcal {HC(@, \downarrow )}}\) ${\mathbf{V}}_{\mathcal{HC}(@,\downarrow )}$ on the class of temporal sphere models, i.e., sphere models derived from a type of branching-time models.