Second order intuitionistic propositional logic of the real line is decidable

2016/12/21 by Zdanowski, Konrad
#03B20 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1612.07167

Abstract

It is known that the set of tautologies of second order intuitionistic propositional logic, IPC 2, is undecidable. Here, we prove that the sets of formulas of IPC 2 which are true in the algebra of open subsets of reals or rationals are decidable.

Related

• First-Order Intuitionistic Logic with Decidable Propositional Atoms
• De Jongh's Theorem for Intuitionistic Zermelo-Fraenkel Set Theory
• A completeness theorem in proof-theoretic semantics via set-theoretic semantics
• Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic
• A polynomial time complete disjunction property in intuitionistic propositional logic