Embedding first order predicate logic in fragments of intuitionistic logic

DOI10.2307/2272390zbMath0358.02012OpenAlexW2107589331MaRDI QIDQ4133591

Martin Löb

Publication date: 1977

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

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

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55)

Related Items (14)

Propositional quantification in the topological semantics for \(\mathbf S4\) ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ Conservativity between logics and typed λ calculi ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable ⋮ Inhabitation of polymorphic and existential types ⋮ Third-order matching in the polymorphic lambda calculus ⋮ Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic ⋮ Unnamed Item ⋮ Eigenvariables, bracketing and the decidability of positive minimal predicate logic ⋮ Unnamed Item ⋮ Mereotopology in 2nd-Order and Modal Extensions of Intuitionistic Propositional Logic ⋮ CPS-translation as adjoint ⋮ A simple proof of the undecidability of inhabitation in λP ⋮ A sequent calculus for subtyping polymorphic types

This page was built for publication: Embedding first order predicate logic in fragments of intuitionistic logic