The intuitionistic propositional calculus with quantifiers |
| |
Authors: | S K Sobolev |
| |
Institution: | (1) V. A. Steklov Mathematical Institute, Academy of Sciences of the USSR, USSR |
| |
Abstract: | Let L be the language of the intuitionistic propositional calculus J completed by the quantifiers and , and let calculus 2J in language L contain, besides the axioms of J, the axioms xB (x) B(y) and B(y) xB (x). A Kripke semantics is constructed for 2J and a completeness theorem is proven. A result of D. Gabbay is generalized concerning the undecidability of C2J+-extension of 2J by schemes x (x B) and x(A B(x))A xB (x) specificially: the undecidability is proven of each T theory in language L such that 2J]T C2J+] (2J] (2J] denotes the set of all theorems of calculus 2J).Translated from Matematicheskie Zametki, Vol. 22, No. 1, pp. 69–76, July, 1977. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|