Abstract

We define intuitionistic subatomic natural deduction systems for reasoning with elementary would-counterfactuals and causal since-subordinator sentences. The former kind of sentence is analysed in terms of counterfactual implication, the latter in terms of factual implication. Derivations in these modal proof systems make use of modes of assumptions which are sensitive to the factuality status of the formula that is to be assumed. This status is determined by means of the reference proof system on top of which a modal proof system is defined. The introduction and elimination rules for counterfactual (resp. factual) implication draw on this status. It is shown that derivations in the systems normalize and that normal derivations have the subexpression/subformula property. An intuitionistically acceptable proof-theoretic semantics is formulated in terms of canonical derivations. The systems are applied to so-called counterpossibles and to related constructions.