η-conversions of IPC implemented in atomic F

DOI10.1093/JIGPAL/JZW035zbMath1405.03091OpenAlexW2469665705MaRDI QIDQ4644473

Gilda Ferreira

Publication date: 8 January 2019

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

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

zbMATH Keywords

natural deductionintuitionistic propositional calculusstrong normalizationpredicative polymorphism\(\eta\)-conversions

Mathematics Subject Classification ID

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

Related Items (5)

Rasiowa-Harrop disjunction property ⋮ A refined interpretation of intuitionistic logic by means of atomic polymorphism ⋮ Unnamed Item ⋮ Atomic polymorphism and the existence property ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

This page was built for publication: η-conversions of IPC implemented in atomic F