The faithfulness of F_at: a proof-theoretic proof

DOI10.1007/S11225-015-9620-5zbMATH Open1378.03038OpenAlexW612033034MaRDI QIDQ897484FDOQ897484

Authors: Fernando Ferreira, Gilda Ferreira 

Publication date: 7 December 2015

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-015-9620-5

Recommendations

• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• FLAGG AND FRIEDMAN'S TRANSLATION IS NOT FAITHFUL
• Atomic polymorphism
• Atomic polymorphism and the existence property
• \(\eta\)-conversions of IPC implemented in atomic F

zbMATH Keywords

natural deductionstrong normalizationdisjunction propertyfaithfulnessintuitionistic propositional calculuspredicative polymorphism

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Commuting conversions vs. the standard conversions of the ``good connectives
• Comments on predicative logic
• Atomic polymorphism

Cited In (4)

• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• Atomic polymorphism and the existence property
• Rasiowa-Harrop disjunction property
• Elementary Proof of Strong Normalization for Atomic F

This page was built for publication: The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof

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