Decision procedures for the conditions true in certain metric structures

After establishing a completeness theorem for continuous logic, Ben Yaacov and Pedersen conclude that if T is a complete recursive L -theory in continuous logic, and v ( φ ) is the truth value of the L -sentence φ in models of T, then v ( φ ) is a recursive real uniformly recursive in φ. Some of the examples to which the latter result applies are theories of the following structures: atomless probability structures, the Urysohn space of diameter 1, Hilbert space, the lattice-ordered group or ring of real-valued continuous functions on the Cantor set, and the complex ⁎-algebra of continuous functions on the Cantor set. This paper will explain why these examples obey much stronger results, yielding (for example) decision procedures for the conditions true in these structures.