Hostname: page-component-78c5997874-8bhkd Total loading time: 0 Render date: 2024-11-13T00:51:01.273Z Has data issue: false hasContentIssue false
  • English
  • Français

The decidability of dependency in intuitionistic propositional logic

Published online by Cambridge University Press:  12 March 2014

Dick de Jongh  and
L. A. Chagrova
Dick de Jongh
Affiliation:
Department of Mathematics and Computer Science, University of Amsterdam, 1018 TV Amsterdam, The Netherlands, E-mail: [email protected]
L. A. Chagrova
Affiliation:
Tver State University, 170013 Tver, Russia
Get access Rights & Permissions [Opens in a new window]

Abstract

A definition is given for formulae A1, …, An in some theory T which is formalized in a propositional calculus S to be (in)dependent with respect to S. It is shown that, for intuitionistic propositional logic IPC, dependency (with respect to IPC itself) is decidable. This is an almost immediate consequence of Pitts’ uniform interpolation theorem for IPC. A reasonably simple infinite sequence of IPC-formulae Fn (p, q) is given such that IPC-formulae A and B are dependent if and only if at least on of the Fn (A, B) is provable.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 60 , Issue 2 , June 1995 , pp. 498 - 504
Copyright
Copyright © Association for Symbolic Logic 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1970] de Jongh, D. H. J., A characterization of the intuitionistic propositional calculus, in Kino, Myhill, and Vesley [1970] pp. 211–217.CrossRefGoogle Scholar
[1982] de Jongh, D. H. J., Formulas of one propositional variable in intuitionistic arithmetic, in Troelstra and van Dalen [1982] pp. 51–64.CrossRefGoogle Scholar
[1993] de Jongh, D. H. J. and Visser, A., Embeddings of Hey ting algebras, ILLC Prepublications ML-93-14, ILLC, University of Amsterdam, Amsterdam.Google Scholar
[1970] Kino, A., Myhill, J., and Vesley, R. E. (editors), Intunionism and proof theory, North-Holland, Amsterdam.Google Scholar
[1982] Maksimova, L. L., Interpolation properties of superintuitionistic, positive and modal logics, Intensional logic: Theory and Applications, Acta Philosophica Fennica, vol. 35, pp. 70–78; Societas Philosophica Fennica, Helsinki.Google Scholar
[1992] Pitts, A., On an interpretation of second order quantification in first order intuitionistic propositional logic, this Journal, vol. 57, pp. 33–52.Google Scholar
[1992] Rybakov, V. V., Rules of inference with parameters for intuitionistic logic, this Journal, vol. 57, pp. 912–923.Google Scholar
[1993] Shavrukov, V., Subalgebras of diagonalizable algebras of theories containing arithmetic, Dissertationes Mathematicae/Rozprawy Matematyczne, vol. 323.Google Scholar
[1978] Shehtman, V. B., Rieger-Nishimura lattices, Soviet Mathematics Doklady, vol. 19, pp. 1014–1018.Google Scholar
[1973] Smoryński, C., Applications of Kripke models, in Troelstra [1973] pp. 324–391.CrossRefGoogle Scholar
[1973] Troelstra, A. S. (editor), Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin.CrossRefGoogle Scholar
[1982] Troelstra, A. S. and van Dalen, D. (editors), The L. E. J. Brouwer centenary symposium, North-Holland, Amsterdam.Google Scholar