The completeness of provable realizability
type: Item
instance of: scholarly article
title: The completeness of provable realizability
zbMATH Open document ID: 0704.03004
published in: Notre Dame Journal of Formal Logic
publication date: 1989-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 4154406
zbMATH Keywords: complete axiomatization
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: realizability
author: G. E. Mints
reviewed by: Sergei Artemov
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1093635158
OpenAlex ID: W2016129710
DOI: 10.1305/NDJFL/1093635158
description: scientific article; zbMATH DE number 4154406