On the contrapositive of countable choice
type: Item
instance of: scholarly article
title: On the contrapositive of countable choice
zbMATH Open document ID: 1218.03034
author: Hajime Ishihara
author: Peter Schuster
published in: Archive for Mathematical Logic
publication date: 2011-03-02T00:00:00Z
review text: Relations between some principles in the framework of elementary intuitionistic analysis, EL, and intuitionistic arithmetic, HA, are considered. These principles are: the contrapositive of countable choice \[ \text{CCC:}\quad\forall f\,\exists x\,P(x,f(x))\to\exists x\,\forall y\,P(x,y), \] double negation elimination for \(\Sigma_2^0\)-formulas \[ \Sigma_2^0\text{-DNE:}\quad\neg\neg\exists x\,\forall y\,P(x,y)\to\exists x\,\forall y\,P(x,y), \] and the law of excluded middle for \(\Sigma_1^0\)-formulas \[ \Sigma_1^0\text{-LEM:}\quad\exists x\,P(x)\lor\forall x\,\neg P(x). \] In all three principles, \(P\) is a decidable predicate. Proposition 1. \(\text{EL}\vdash\Sigma_2^0\text{-DNE}\leftrightarrow\text{CCC}\). If \(f\) ranges over the recursive functions, CCC can be stated in an arithmetical form \(\text{CCC}^\circ\) using Kleene's predicate \(T\) and function \(U\). Proposition 2. (a) \(\text{HA}+\Sigma_2^0\text{-DNE}\vdash\text{CCC}^\circ\). (b) \(\text{HA}+\text{CCC}^\circ\vdash\Sigma_1^0\text{-LEM}\). (c) \(\text{HA}+\text{CCC}^\circ\vdash\Sigma_2^0\text{-DNE}\). It follows that \(\text{HA}\vdash\Sigma_2^0\text{-DNE}\leftrightarrow\text{CCC}^\circ\). Let S be an extension of HA. A predicate \(R\) is called: externally recursive in S, if there is a numeral \(t\) such that \[ \text{S}\vdash\forall x\,\exists z\,(T(t,x,z)\land(R(x)\leftrightarrow U(z)=0)); \] internally recursive in S, if \[ \text{S}\vdash\exists e\,\forall x\,\exists z\,(T(e,x,z)\land(R(x)\leftrightarrow U(z)=0)); \] decidable in S, if \[ \text{S}\vdash\forall x\,(R(x)\lor\neg R(x)). \] The following proposition is proved by using formalized realizability. Proposition 3. (a) In \(\text{HA}+\text{ECT}_0\), every decidable predicate is externally recursive. (b) In \(\text{HA}+\text{CT}_0\), every decidable predicate is internally recursive. Here \(\text{CT}_0\) and \(\text{ECT}_0\) are standard arithmetical forms of Church's thesis and extended Church's thesis, respectively.
reviewed by: Valery Plisko
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 03D55
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 5859286
zbMATH Keywords: elementary intuitionistic analysis
zbMATH Keywords: Heyting arithmetic
zbMATH Keywords: contrapositive of countable choice
zbMATH Keywords: double negation elimination
zbMATH Keywords: law of excluded middle
zbMATH Keywords: recursive
zbMATH Keywords: decidable
zbMATH Keywords: Church's thesis
MaRDI profile type: Publication
full work available at URL: s00153-010-0205-8
OpenAlex ID: W2010993234
cites work: Some intuitionistic equivalents of classical principles for degree 2 formulas
cites work: Q4126323
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Q3313858
DOI: 10.1007/S00153-010-0205-8
description: scientific article; zbMATH DE number 5859286