Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique

DOI10.2307/421172zbMath0872.03004OpenAlexW2147202919MaRDI QIDQ3128482

Jean-Louis Krivine

Publication date: 11 September 1997

Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: http://www.math.ucla.edu/~asl/bsl/0204-toc.htm

zbMATH Keywords

intuitionistic logicprogram verification\(\lambda\)-termsintuitionistic proofcompleteness theorem of classical logicextension of \(\lambda\)-calculusformalization in second-order logicinteractive disassembleroperational behaviourprotection device for system calls

Mathematics Subject Classification ID

Related Items (7)

Soundness and completeness proofs by coinductive methods ⋮ Krivine's intuitionistic proof of classical completeness (for countable languages) ⋮ Maximal elements with minimal logic ⋮ Kripke models for classical logic ⋮ Completeness, minimal logic and programs extraction ⋮ An intuitionistic completeness theorem for classical predicate logic ⋮ Maximal ideals in countable rings, constructively

Cites Work

• Unnamed Item
• Constructivism in mathematics. An introduction. Volume II
• Classical logic, storage operators and second-order lambda-calculus

This page was built for publication: Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique