The faithfulness of \(\mathbf{F_{at}}\): a proof-theoretic proof

DOI10.1007/s11225-015-9620-5zbMath1378.03038OpenAlexW612033034MaRDI QIDQ897484

Gilda Ferreira, Fernando 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 deductiondisjunction propertyintuitionistic propositional calculusstrong normalizationfaithfulnesspredicative polymorphism

Mathematics Subject Classification ID

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

Related Items

Rasiowa-Harrop disjunction property ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ Atomic polymorphism and the existence property

Cites Work

• Unnamed Item
• Unnamed Item
• Commuting conversions vs. the standard conversions of the ``good connectives
• Comments on predicative logic
• Atomic polymorphism