Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity

DOI10.1023/B:LOGI.0000021744.10237.D0MaRDI QIDQ1826435zbMATH OpenFDO

Authors Richard Zach

Publication date 6 August 2004

Published in Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0203113

zbMATH Keywords

decidabilityintuitionistic logicmodal logicKripke modeltree structurequantified propositional formulas

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Model theory (03C99)

Abstract: Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers forall p, exists p over propositions. In the context of Kripke semantics, a proposition is a subset of the worlds in a model structure which is upward closed. Kremer (1997) has shown that the quantified propositional intuitionistic logic Hpi+ based on the class of all partial orders is recursively isomorphic to full second-order logic. He raised the question of whether the logic resulting from restriction to trees is axiomatizable. It is shown that it is, in fact, decidable. The methods used can also be used to establish the decidability of modal S4 with propositional quantification on similar types of Kripke structures.

Recommendations

• On the complexity of propositional quantification in intuitionistic logic
• Computer Science Logic
• A criterion for admissibility of rules in the modal system S4 and intuitionistic logic
• scientific article; zbMATH DE number 3957081
• Undecidability of First-Order Intuitionistic and Modal Logics with Two variables

Cites work

• scientific article; zbMATH DE number 1696769 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• Decidability of Second-Order Theories and Automata on Infinite Trees
• On the complexity of propositional quantification in intuitionistic logic
• Propositional quantifiers in modal logic1
• Quantifying over propositions in relevance logic: nonaxiomatisability of primary interpretations of ∀p and ∃p
• Semantical investigations in Heyting's intuitionistic logic
• Some theorems about the sentential calculi of Lewis and Heyting

Cited in

(4)

• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• On the logic of belief and propositional quantification
• A note on algebraic semantics for \(\mathsf {S5}\) with propositional quantifiers
• Axiomatizability of propositionally quantified modal logics on relational frames

This page was built for publication: Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity \(\leq \omega\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1826435)