From Kripke models to algebraic counter-valuations. Summary

Sara Negri and Jan von Plato

Starting with a derivation in the refutation calculus CRIP (Pinto and Dyckhoff 1995), we give a constructive algebraic method for determining the values of formulas of intuitionistic propositional logic in a counter-model. These are computed pointwise from the values on atoms, in contrast to the non-local and non-constructive determination of forcing relations in a Kripke model.