Abstract

The purpose of this paper is to describe a set of counterfactual temporal alethic-deontic systems, i.e. systems that include counterfactual, temporal, alethic and deontic operators. All systems are described both semantically and proof theoretically. We use a kind of possible world semantics, inspired by the so-called T x W semantics, to characterise our systems semantically and semantic tableaux to characterise them proof theoretically. Our models contain several different accessibility relations and a similarity relation between possible worlds, which are used in the definitions of the truth conditions for the various operators. Soundness results are obtained for every tableau system and completeness results for a subclass of them.