
In this paper we study the expressive power and algorithmic properties of the language of $\Sigma$formulas intended to represent computability on the real numbers. In order to adequately represent computability we extend the reals by the structure of hereditarily finite sets. In this setting it is crucial to consider the real numbers without equality since the equality test is undecidable over the reals. We prove Engeler's Lemma for $\Sigma$definability over the reals without the equality test which relates $\Sigma$definability with definability in the constructive infinitary language $L_{\omega_1\omega}$. Thus, a relation over the real numbers is $\Sigma$definable if and only if it is definable by a disjunction of a recursively enumerable set of quantifier free formulas. This result reveals computational aspects of $\Sigma$definability and also gives topological characterisation of $\Sigma$definable relations over the reals without the equality test.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 