Exact real number computations relative to hereditarily total functionals. (Q1607298): Difference between revisions

We show that the continuous existential quantifier \(\exists_{\omega}\) is not definable in Escardó's Real-\(PCF\) from all functionals equivalent to a given total one in a uniform way. We further prove that relative to any total functional of type \((I\rightarrow I)\rightarrow I\) which gives the maximum-value for any total input, we may, given a computable, total functional \(\Phi\) of type \((R\rightarrow R)\rightarrow R\) find a Real-\(PCF\)-definable total \(\Psi\) equivalent to \(\Phi\).