Reverse mathematics and completeness theorems for intuitionistic logic
type: Item
instance of: scholarly article
title: Reverse mathematics and completeness theorems for intuitionistic logic
zbMATH Open document ID: 1036.03008
author: Takeshi Yamazaki
published in: Notre Dame Journal of Formal Logic
publication date: 2004-02-04T00:00:00Z
review text: This article investigates the mathematical logic of intuitionistic propositional and predicate calculi using the framework of reverse mathematics [\textit{S. G. Simpson}, Subsystems of second order arithmetic, Berlin: Springer (1999; Zbl 0909.03048)]. Working in RCA\(_0\), the author shows that a version of the strong completeness theorem asserting the existence of a particular sort of Kripke model is equivalent to ACA\(_0\). The paper includes a proof that the saturation lemma for intuitionistic predicate logic is equivalent to WKL\(_0\). These results can also be found in \S{3.2} of the author's thesis [Model-theoretic studies on subsystems of second order arithmetic, Tohoku Mathematical Publications. 17. Sendai: Tohoku Univ. (2000; Zbl 0964.03059)].
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F55
zbMATH DE Number: 2038296
zbMATH Keywords: reverse mathematics
zbMATH Keywords: RCA
zbMATH Keywords: ACA
zbMATH Keywords: second-order arithmetic
zbMATH Keywords: completeness theorems
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: Kripke model
reviewed by: Jeffry L. Hirst
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1063372197
OpenAlex ID: W2036685181
cites work: Semantical investigations in Heyting's intuitionistic logic
cites work: Decidable Kripke models of intuitionistic theories
cites work: Q4220572
cites work: Constructivism in mathematics. An introduction. Volume I
DOI: 10.1305/NDJFL/1063372197
description: scientific article; zbMATH DE number 2038296