Un plongement de la logique classique du 2nd ordre dans AF2

DOI10.1016/S0764-4442(97)83922-5MaRDI QIDQ4355235zbMATH OpenOpenAlexFDO

Authors T. Joly

Publication date 20 November 1997

Published in Comptes Rendus de l'Académie des Sciences - Series I - Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0764-4442(97)83922-5

zbMATH Keywords

natural deductionnormalizationsecond-order logicinteger representationssecond-order functional arithmetic\(\lambda\mu\)-calculus reductionproof translations

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Stabilization -- an alternative to double-negation translation for classical natural deduction
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• scientific article; zbMATH DE number 1722662

Cited in

(3)

• 2-cnfs and logical embeddings
• Non-strictly positive fixed points for classical natural deduction
• Stabilization -- an alternative to double-negation translation for classical natural deduction

This page was built for publication: Un plongement de la logique classique du 2nd ordre dans AF2

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