Reverse mathematics and completeness theorems for intuitionistic logic

DOI10.1305/NDJFL/1063372197MaRDI QIDQ1422103zbMATH OpenOpenAlexFDO

Authors Takeshi Yamazaki

Publication date 4 February 2004

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

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

zbMATH Keywords

ACAcompleteness theoremsintuitionistic logicKripke modelRCAreverse mathematicssecond-order arithmetic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Foundations of classical theories (including reverse mathematics) (03B30) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

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)].

Recommendations

• An intuitionistic completeness theorem for classical predicate logic
• Intuitionistic completeness and classical logic
• Reverse mathematics and uniformity in proofs without excluded middle
• scientific article; zbMATH DE number 1169382
• Completeness and incompleteness for intuitionistic logic

Cites work

• Constructivism in mathematics. An introduction. Volume I
• Decidable Kripke models of intuitionistic theories
• scientific article; zbMATH DE number 1226875 (Why is no real title available?)
• Semantical investigations in Heyting's intuitionistic logic

Cited in

(14)

• Intuitionistic completeness and classical logic
• Splittings and disjunctions in reverse mathematics
• Semantical completeness of first-order predicate logic and the weak fan theorem
• Semantic completeness of first-order theories in constructive reverse mathematics
• Intuitionistic provability versus uniform provability in \(\mathsf{RCA}\)
• The monotone completeness theorem in constructive reverse mathematics
• scientific article; zbMATH DE number 1187191 (Why is no real title available?)
• scientific article; zbMATH DE number 1536018 (Why is no real title available?)
• On Weihrauch reducibility and intuitionistic reverse mathematics
• L-Completeness of the Lambek Calculus with the Reversal Operation
• Well-Ordering Principles in Proof Theory and Reverse Mathematics
• Erratum to: ``Semantic completeness of first-order theories in constructive reverse mathematics
• Hindman's theorem, ultrafilters, and reverse mathematics
• Completeness theorems for modal logic in second-order arithmetic

This page was built for publication: Reverse mathematics and completeness theorems for intuitionistic logic

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