-conversions of IPC implemented in atomic F

DOI10.1093/JIGPAL/JZW035zbMATH Open1405.03091OpenAlexW2469665705MaRDI QIDQ4644473FDOQ4644473

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

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\)

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)

Cited In (6)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof
• Atomic polymorphism and the existence property
• Rasiowa-Harrop disjunction property
• Title not available (Why is that?)

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)