The faithfulness of F_at: a proof-theoretic proof

DOI10.1007/S11225-015-9620-5MaRDI QIDQ897484zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Atomic polymorphism
• Comments on predicative logic
• Commuting conversions vs. the standard conversions of the ``good connectives

Cited in

(8)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• Atomic polymorphism and the existence property
• Instantiation overflow
• \(\eta\)-conversions of IPC implemented in atomic F
• An elementary proof of strong normalization for atomic \(\mathsf F\)
• The Russell-Prawitz embedding and the atomization of universal instantiation
• Rasiowa-Harrop disjunction property

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)