Glueing of analysis models in an intuitionistic setting
type: Item
instance of: scholarly article
title: Glueing of analysis models in an intuitionistic setting
zbMATH Open document ID: 0637.03059
DOI: 10.1007/BF00373273
published in: Studia Logica
publication date: 1986-01-01T00:00:00Z
review text: The author has earlier written a paper on a model-theoretic construction using Beth models for some mathematical results about intuitionistic principles such as continuity and Kripke's schema. This paper is concerned with the formalization of these arguments in an intuitionistic meta-theory. It is slightly tricky as the argument appears to involve a proof by contradiction. The difficulty is partly overcome by appealing to a formalized version of the Beth completeness theorem (Dyson and Kreisel). The result of the formalization of the glueing construction is a proof of the existence and disjunction properties for this theory T: intuitionistic analysis with bar induction, weak continuity, Kripke's schema, and AC-NF. But when the verification of the axioms is done, we have the proof of the disjunction property only within T, not in reality. Let us try to obtain it in reality: suppose T proves \(\exists xA\); then we can verify that fact in T and so obtain from the formalized argument, \(\exists x\Pr_ T(\ulcorner A[\bar x]\urcorner)\). So now we need to know that \(\Sigma^ 1_ 0\) sentences proved by T are true. For this the author appeals (p. 182) to the model of Krol (without which we don't even know T is consistent). This clever, if roundabout, formalization of an apparently classical argument in an intuitionistic theory is not the only known proof of the existence and disjunction properties for T. The model of Krol can also be used directly for this purpose, as is acknowledged in the paper's last sentence.
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F55
zbMATH DE Number: 4037861
zbMATH Keywords: Beth models
zbMATH Keywords: intuitionistic meta-theory
zbMATH Keywords: Beth completeness theorem
zbMATH Keywords: intuitionistic analysis
zbMATH Keywords: bar induction
zbMATH Keywords: weak continuity
zbMATH Keywords: Kripke's schema
zbMATH Keywords: disjunction property
zbMATH Keywords: model of Krol
author: Dirk van Dalen
MaRDI profile type: Publication
cites work: An interpretation of intuitionistic analysis
cites work: How to glue analysis models
cites work: Q4492739
cites work: Concepts of general topology in constructive mathematics and in sheaves
cites work: Kripke models and the intuitionistic theory of species
cites work: A Topological Model for Intuitionistic Analysis with Kripke's Scheme
cites work: Q4126323
cites work: Q4163218
full work available at URL: https://doi.org/10.1007/bf00373273
OpenAlex ID: W2104885172
description: scientific article; zbMATH DE number 4037861