About Goodman's theorem
type: Item
instance of: scholarly article
title: About Goodman's theorem
zbMATH Open document ID: 1284.03267
author: Thierry Coquand
published in: Annals of Pure and Applied Logic
publication date: 2013-03-15T00:00:00Z
review text: In 1978, Nicholas Goodman published a proof of the statement that \(\mathrm{HA}^{\omega}+\mathrm{ AC}\) is conservative over \(\mathrm{HA}\). Here \(\mathrm{ HA}^{\omega}\) is ``intuitionistic arithmetic in all finite types'', and AC is the ``Axiom of Choice'': \[ \forall x^{\sigma}\exists y^{\tau}\phi (x,y)\;\to\;\exists z^{\sigma\to\tau}\forall x^{\sigma}\phi (x,zx). \] Goodman's proof was an intricate mixture of a kind of forcing and realizability. The metamathematics is non-constructive. The present paper is concerned with a \textit{constructive} version of this proof. The technique of proof consists in separating the realizability part from the forcing part, and define forcing \textit{locally}, that is: for a given formula \(\psi\) such that \({\mathrm{ HA}}^{\omega}+{\mathrm{ AC}}\vdash\psi\), a notion of forcing is defined with nice properties. First, following Renardel de Lavalette, a system \(\mathrm{TAPP}\) is defined (basically, axioms for ``arithmetic plus a combinatory algebra structure'') which can easily be seen to be a conservative extension of \(\mathrm{ HA}^{\omega}\), hence also of \(\mathrm{HA}\). The theory \(\mathrm{TAPP}\) has a built-in realizability, and \(\mathrm{AC}\) is provably realized in it. As a consequence, whenever \(\mathrm{ HA}^{\omega}+\mathrm{ AC}\) proves a formula \(\phi\), \(\mathrm{TAPP}\) proves that \(\phi\) is realizable. Then, relative to a proof of a formula \(\psi\) in \(\mathrm{ HA}^{\omega}+\mathrm{ AC}\), the author defines a definitional extension of \(\mathrm{TAPP}\) with an extra sort of ``forcing conditions'' and some special constants \(c\). The constants \(c\) are meant to encode explicit choices for existential formulas occurring in the hypothetical proof, so for such a formula \(\exists nB(m,n)\) we have an axiom \[ (\exists nB(m,n))\to N(cm)\wedge B(m,cm), \] where \(cm\) is the action of \(c\) on the natural number \(m\), and \(N(cm)\) is the statement that \(cm\) is a natural number. The idea is now that …
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F60
zbMATH DE Number: 6145437
zbMATH Keywords: formal topology
zbMATH Keywords: Goodman's theorem
zbMATH Keywords: forcing
zbMATH Keywords: realizability
MaRDI profile type: Publication
full work available at URL: j.apal.2012.10.007
OpenAlex ID: W2275376313
DOI: 10.1016/J.APAL.2012.10.007
description: scientific article; zbMATH DE number 6145437