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

DOI10.1023/B:LOGI.0000021744.10237.D0zbMATH Open1054.03011arXivmath/0203113MaRDI QIDQ1826435FDOQ1826435

Authors: Richard Zach 

Publication date: 6 August 2004

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

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.

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

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

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)

Cites Work

• Propositional quantifiers in modal logic1
• Title not available (Why is that?)
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Semantical investigations in Heyting's intuitionistic logic
• Some theorems about the sentential calculi of Lewis and Heyting
• On the complexity of propositional quantification in intuitionistic logic
• Quantifying over propositions in relevance logic: nonaxiomatisability of primary interpretations of ∀p and ∃p
• Title not available (Why is that?)

Cited In (4)

• Title not available (Why is that?)
• 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)