η-conversions of IPC implemented in atomic F

It is known that the β-conversions of the full intuitionistic propositional calculus (IPC) translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering...

Full description

Bibliographic Details
Main Author: Ferreira, Gilda (author)
Format: article
Language:eng
Published: 2018
Subjects:
Mathematical logic
Eta-conversions
Predicative polymorphism
Intuitionistic propositional calculus
Strong normalization
Natural deduction
Online Access:http://hdl.handle.net/10400.2/7091
Country:Portugal
Oai:oai:repositorioaberto.uab.pt:10400.2/7091

Internet

http://hdl.handle.net/10400.2/7091

Similar Items