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

DOI10.2307/421172zbMATH Open0872.03004OpenAlexW2147202919MaRDI QIDQ3128482FDOQ3128482

Authors: Jean-Louis Krivine 

Publication date: 11 September 1997

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

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

Recommendations

• scientific article; zbMATH DE number 517083
• scientific article
• Programming and Proving with Classical Types
• A symmetric lambda calculus for classical program extraction
• Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic

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

Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Cites Work

• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Classical logic, storage operators and second-order lambda-calculus

Cited In (20)

• Maximal ideals in countable rings, constructively
• Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic
• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
• An intuitionistic completeness theorem for classical predicate logic
• Title not available (Why is that?)
• Classical logic as limit completion
• Title not available (Why is that?)
• Completeness, minimal logic and programs extraction
• Almost all Classical Theorems are Intuitionistic
• Soundness and completeness proofs by coinductive methods
• Title not available (Why is that?)
• Title not available (Why is that?)
• Kripke models for classical logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intuitionistic completeness for first order classical logic
• Maximal elements with minimal logic
• Satisfaction and Friendliness Relations within Classical Logic: Proof-Theoretic Approach
• Unified Classical Logic Completeness
• Krivine's intuitionistic proof of classical completeness (for countable languages)

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

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