A syntactic embedding of predicate logic into second-order propositional logic

DOI10.1215/00294527-2010-029MaRDI QIDQ609763zbMATH OpenOpenAlexFDO

Authors Paweł Urzyczyn, M. H. B. Sørensen

Publication date 1 December 2010

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1215/00294527-2010-029

zbMATH Keywords

first-order intuitionistic predicate logicIPC2propositional quantificationsecond-order intuitionistic propositional logicsyntactic translation

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25)

Recommendations

• Embedding first order predicate logic in fragments of intuitionistic logic
• On second order intuitionistic propositional logic without a universal quantifier
• A secondary semantics for Second Order Intuitionistic Propositional Logic
• Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic
• scientific article; zbMATH DE number 1088204

Cited in

(8)

• Embeddings between the elementary ontology with an atom and the monadic second-order predicate logic
• Embedding first order predicate logic in fragments of intuitionistic logic
• Syntactical truth predicates for formulas with atomic negation
• Polymorphic higher-order termination
• A simpler undecidability proof for system F inhabitation
• The existential fragment of second-order propositional intuitionistic logic is undecidable
• Type checking and typability in domain-free lambda calculi
• Formalizing Dijkstra's predicate transformer wp in weak second-order logic

This page was built for publication: A syntactic embedding of predicate logic into second-order propositional logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q609763)