The Russell-Prawitz embedding and the atomization of universal instantiation

DOI10.1093/JIGPAL/JZAA025zbMATH Open1494.03031arXiv1909.01232OpenAlexW3046138748MaRDI QIDQ5014064FDOQ5014064

Authors: José Espírito Santo, Gilda Ferreira 

Publication date: 3 December 2021

Published in: Logic Journal of the IGPL (Search for Journal in Brave)

Abstract: Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain "dinaturality" conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system F_at; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into F_at does not.

Full work available at URL: https://arxiv.org/abs/1909.01232

Recommendations

• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• scientific article; zbMATH DE number 1858065
• Atomic polymorphism
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof
• An elementary proof of strong normalization for atomic \(\mathsf F\)

zbMATH Keywords

system Fintuitionistic propositional calculusproof reductionpredicative polymorphismRussell-Prawitz translation

Mathematics Subject Classification ID

Higher-order logic (03B16) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cited In (2)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• A refined interpretation of intuitionistic logic by means of atomic polymorphism

This page was built for publication: The Russell-Prawitz embedding and the atomization of universal instantiation

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