The completeness of provable realizability

DOI10.1305/NDJFL/1093635158MaRDI QIDQ916636zbMATH OpenOpenAlexFDO

Authors G. E. Mints

Publication date 1989

Published in Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1305/ndjfl/1093635158

zbMATH Keywords

complete axiomatizationintuitionistic logicrealizability

Mathematics Subject Classification ID

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

Review text

The paper gives a complete axiomatization for intuitionistic logic without disjunction but with so called strong conjunction \& which is determined by the stipulation: \(x\) realizes \(A\&B\) iff \(x\) realizes both \(A\) and \(B\). It is shown also that the provability of a formula \(A\) in this calculus coincides with the classical provability of the first order formula ``the \(\lambda\)-term \(t\) realizes the formula \(A\). Realizing terms here are required to be untyped and the derivation of realizability is classical.

Recommendations

• Proof-functional connectives and realizability
• scientific article; zbMATH DE number 1497741
• Absolute L-realizability and intuitionistic logic
• scientific article; zbMATH DE number 2174389
• scientific article; zbMATH DE number 176126

Cited in

(12)

• Types with intersection: An introduction
• Proof-functional connectives and realizability
• The ``relevance of intersection and union types
• A realizability interpretation for intersection and union types
• Verificationism and Classical Realizability
• Inhabitation of Low-Rank Intersection Types
• scientific article; zbMATH DE number 3979048 (Why is no real title available?)
• Universality of Regular Realizability Problems
• The emptiness problem for intersection types
• The -calculus: syntax and types
• A type checker for a logical framework with union and intersection types (system description)
• Well-foundedness in realizability

This page was built for publication: The completeness of provable realizability

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