-conversions of IPC implemented in atomic F

DOI10.1093/JIGPAL/JZW035MaRDI QIDQ4644473zbMATH OpenOpenAlexFDO

Authors Gilda Ferreira

Publication date 8 January 2019

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

Full work available at URL http://hdl.handle.net/10400.2/7091

zbMATH Keywords

natural deductionstrong normalizationintuitionistic propositional calculuspredicative polymorphism\(\eta\)-conversions

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07)

Recommendations

• Atomic polymorphism
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• An elementary proof of strong normalization for atomic \(\mathsf F\)

Cited in

(6)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• scientific article; zbMATH DE number 7577586 (Why is no real title available?)
• Rasiowa-Harrop disjunction property
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof
• Atomic polymorphism and the existence property
• A refined interpretation of intuitionistic logic by means of atomic polymorphism

This page was built for publication: \(\eta\)-conversions of IPC implemented in atomic F

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