From Kripke Models to Algebraic Counter-Valuations
- 227 Downloads
Starting with a derivation in the refutation calculus CRIP of Pinto and Dyckhoff, we give a constructive algebraic method for determining the values of formulas of intuitionistic propositional logic in a counter-model. The values of compound formulas are computed point-wise from the values on atoms, in contrast to the non-local determination of forcing relations in a Kripke model based on classical reasoning.
Unable to display preview. Download preview PDF.
- Dyckhoff, R. and L. Pinto (1996) Implementation of a loop-free method for construction of counter-models for intuitionistic propositional logic, CS/96/8, Computer Science Division, St Andrews University.Google Scholar
- Hudelmaier, J. (1989) Bounds for cut elimination in intuitionistic propositional logic, PhD thesis, University of Tübingen.Google Scholar
- Negri, S. (1997) Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic, to appear.Google Scholar
- Pinto, L. and R. Dyckhoff (1995) Loop-free construction of counter-models for intuitionistic propositional logic, in Behara et al. eds., Symposia Gaussiana, Conf. A, pp. 225–232, de Gruyter, Berlin.Google Scholar
- von Plato, J. (1997) Positive Heyting algebras, manuscript.Google Scholar
- Stoughton, A. (1996) Porgi: a Proof-Or-Refutation Generator for Intuitionistic propositional logic. CADE-13 Workshop on Proof Search in Type-Theoretic Languages, Rutgers University, pp. 109–116.Google Scholar
- Troelstra, A. S. and D. van Dalen (1988) Constructivism in Mathematics, vol. 1, North-Holland, Amsterdam.Google Scholar
- Troelstra, A. S. and H. Schwichtenberg (1996) Basic Proof Theory, Cambridge University Press.Google Scholar