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 logicKripke modelmodal logicquantified propositional formulastree structure

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Modal logic (including the logic of norms) (03B45) 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.

Review text

The long title describes the contents of this article, but not the context. In J. Symb. Log. 62, 529--544 (1997; Zbl 0887.03002), \textit{P. Kremer} showed that the set of quantified propositional formulas, valid with respect to all the Kripke structures (i.e., quasi-order with the minimal element), is highly undecidable; indeed, it is recursively isomorphic to the valid second-order formulas. He left open the problem: what happens if structures are confined to tree orders. The author answers this by showing the decidability in this setting. Actually, he considers three classes of structures: all the trees as described in the title, the exactly \(n\)-branching full tree, and the finite trees. In each of these classes, the set of valid formulas is decidable. He reduces the problem to the 1969 vintage result of \textit{M. O. Rabin} on the decidability of the second-order tree language [Trans. Am. Math. Soc. 141, 1--35 (1969; Zbl 0221.02031)] by giving a translation of intuitionism formulas to tree formulas. Modal system S4 is similarly shown to be decidable. The author also considers the case when the structures are linear orders of various kinds [Gödel-Dummet logics], and cites a number of open problems.

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

• Decidability of Second-Order Theories and Automata on Infinite Trees
• scientific article; zbMATH DE number 1696769 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• 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

(5)

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

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)