Advertisement

From Kripke Models to Algebraic Counter-Valuations

  • Sara Negri
  • Jan von Plato
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)

Abstract

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Dyckhoff, R. (1992) Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol. 57, pp. 795–807.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 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
  3. Fitting, M. (1969) Intuitionistic Logic, Model Theory and Forcing, North-Holland, AmsterdamzbMATHGoogle Scholar
  4. Hudelmaier, J. (1989) Bounds for cut elimination in intuitionistic propositional logic, PhD thesis, University of Tübingen.Google Scholar
  5. Hudelmaier, J. (1992) Bounds for cut elimination in intuitionistic propositional logic, Archive for Mathematical Logic, vol. 31, pp. 331–354.zbMATHCrossRefMathSciNetGoogle Scholar
  6. Negri, S. (1997) Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic, to appear.Google Scholar
  7. 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
  8. von Plato, J. (1997) Positive Heyting algebras, manuscript.Google Scholar
  9. 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
  10. Troelstra, A. S. and D. van Dalen (1988) Constructivism in Mathematics, vol. 1, North-Holland, Amsterdam.Google Scholar
  11. Troelstra, A. S. and H. Schwichtenberg (1996) Basic Proof Theory, Cambridge University Press.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Sara Negri
    • 1
  • Jan von Plato
    • 1
  1. 1.Department of PhilosophyUniversity of HelsinkiFinland

Personalised recommendations