On an interpretation of second order quantification in first order intuitionistic propositional logic

DOI10.2307/2275175zbMath0763.03009OpenAlexW2127394739MaRDI QIDQ4008745

Publication date: 27 September 1992

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

Full work available at URL: https://doi.org/10.2307/2275175

zbMATH Keywords

interpolation quantification Heyting algebras Heyting's intuitionistic propositional calculus second order propositional calculus

Mathematics Subject Classification ID

Logical aspects of lattices and related structures (03G10) Heyting algebras (lattice-theoretic aspects) (06D20) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (70)

Uniform interpolation and compact congruences ⋮ Interpolation property for bicartesian closed categories ⋮ An algebraic theory of normal forms ⋮ Uniform interpolation from cyclic proofs: the case of modal mu-calculus ⋮ Duality and Universal Models for the Meet-Implication Fragment of IPC ⋮ Positive Formulas in Intuitionistic and Minimal Logic ⋮ Uniform Lyndon interpolation for basic non-normal modal logics ⋮ Uniform interpolation via nested sequents ⋮ Undefinability of propositional quantifiers in the modal system S4 ⋮ Model completions and r-Heyting categories ⋮ Uniform interpolation and propositional quantifiers in modal logics ⋮ Propositional quantification in the topological semantics for \(\mathbf S4\) ⋮ Questions and dependency in intuitionistic logic ⋮ ON FLATTENING ELIMINATION RULES ⋮ UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS ⋮ The decidability of dependency in intuitionistic propositional logic ⋮ Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ Conservativity between logics and typed λ calculi ⋮ Logic-based ontology comparison and module extraction, with an application to DL-Lite ⋮ THE AUTOMORPHISM GROUP OF THE FRAÏSSÉ LIMIT OF FINITE HEYTING ALGEBRAS ⋮ Proof theory for positive logic with weak negation ⋮ A sheaf representation and duality for finitely presented Heyting algebras ⋮ Interpolation Property on Visser's Formal Propositional Logic ⋮ Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey ⋮ A decidability result for the model checking of infinite-state systems ⋮ Uniform interpolation and sequent calculi in modal logic ⋮ Extendible formulas in two variables in intuitionistic logic ⋮ Admissibility of structural rules for contraction-free systems of intuitionistic logic ⋮ The Lyndon property and uniform interpolation over the Grzegorczyk logic ⋮ The Logical Difference Problem for Description Logic Terminologies ⋮ Bisimulation quantifiers and uniform interpolation for guarded first order logic ⋮ Uniform interpolation and coherence ⋮ An open mapping theorem for finitely copresented Esakia spaces ⋮ CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC: A CORRECTION ⋮ Completeness for the modal \(\mu\)-calculus: separating the combinatorics from the dynamics ⋮ Propositional quantification in the monadic fragment of intuitionistic logic ⋮ Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi ⋮ Pitts' quantifiers are not topological quantification ⋮ Rules and arithmetics ⋮ An axiomatization of bisimulation quantifiers via the \(\mu\)-calculus ⋮ On Bellissima's construction of the finitely generated free Heyting algebras, and beyond ⋮ Investigations on the dual calculus ⋮ Computing interpolants in implicational logics ⋮ Unnamed Item ⋮ Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic ⋮ Interpolation properties for provability logics GL and GLP ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ Harmony in Proof-Theoretic Semantics: A Reductive Analysis ⋮ Fixed-Point Elimination in the Intuitionistic Propositional Calculus ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Formal Properties of Modularisation ⋮ Model completeness, covers and superposition ⋮ Mathematical Logic for Life Science Ontologies ⋮ The many faces of interpolation ⋮ Interpolation in non-classical logics ⋮ Description of all functions definable by formulæ of the 2nd order intuitionistic propositional calculus on some linear Heyting algebras ⋮ Mereotopology in 2nd-Order and Modal Extensions of Intuitionistic Propositional Logic ⋮ Uniform interpolation and the existence of sequent calculi ⋮ Doing logic by computer: Interpolation in fragments of intuitionistic propositional logic ⋮ Uniform Lyndon interpolation property in propositional modal logics ⋮ Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus ⋮ Combination of uniform interpolants via Beth definability ⋮ Some Formal Semantics for Epistemic Modesty ⋮ DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV ⋮ Combined covers and Beth definability ⋮ Sequent Calculi and Interpolation for Non-Normal Modal and Deontic Logics ⋮ The G4i analogue of a G3i sequent calculus ⋮ Second order propositional operators over Cantor space ⋮ MODEL COMPLETIONS FOR UNIVERSAL CLASSES OF ALGEBRAS: NECESSARY AND SUFFICIENT CONDITIONS

Cites Work

This page was built for publication: On an interpretation of second order quantification in first order intuitionistic propositional logic