INTUITIONISTIC AND CLASSICAL SATISFIABILITY

Ac lassP ∗ of formulas was defined in (4) which whenever satisfied in a classical structure associated with a node of a Kripke model must also be forced at that node. Here we define a dual class R of formulas which whenever forced at a node of a Kripke model must be satisfied in the classical structure associated with that node.