Glueing of analysis models in an intuitionistic setting (Q1098848): Difference between revisions

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.