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

disjunction propertyfaithfulnessintuitionistic propositional calculusnatural deductionpredicative polymorphismstrong normalization

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
• -conversions of IPC implemented in atomic F

Cites work

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

Cited in

(10)

• Atomic polymorphism and the existence property
• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• Rasiowa-Harrop disjunction property
• An elementary proof of strong normalization for atomic F
• Instantiation overflow
• -conversions of IPC implemented in atomic F
• The Russell-Prawitz embedding and the atomization of universal instantiation
• How to avoid the commuting conversions of \textbf{IPC}
• Categorical proof-theoretic semantics

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)