A Lopez-Escobar Theorem for Continuous Domains

TL;DR

This paper establishes an effective version of the Lopez-Escobar theorem for continuous domains, linking topological definability with logical formulas, and applies it to positive computable embeddings and linear orderings.

Contribution

It proves a new effective Lopez-Escobar theorem for continuous domains and derives a pullback theorem for positive computable embeddings.

Findings

Invariant sets are characterized by $ ext{Pi}^0_eta$ formulas and definable by $ ext{Pi}^p_eta$ formulas.

A new pullback theorem for positive computable embeddings is established.

Results on embeddings into the class of linear orderings are obtained.

Abstract

We prove an effective version of the Lopez-Escobar theorem for continuous domains. Let $Mod(\tau)$ be the set of countable structures with universe $\omega$ in vocabulary $\tau$ topologized by the Scott topology. We show that an invariant set $X \subseteq Mod(\tau)$ is $\Pi^0_\alpha$ in the effective Borel hierarchy of this topology if and only if it is definable by a $\Pi^p_\alpha$ - formula, a positive $\Pi^0_\alpha$ formula in the infinitary logic $L_{\omega_1,\omega}$. As a corollary of this result we obtain a new pullback theorem for positive computable embeddings: Let $K$ be positively computably embeddable in $K'$ by $\Phi$, then for every $\Pi^p_\alpha$ formula $\xi$ in the vocabulary of $K'$ there is a $\Pi^p_\alpha$ formula $\xi^\star$ in the vocabulary of $K$ such that for all $A \in K$, $A \models \xi^\star$ if and only if $\Phi(A) \models \xi$. We use this to obtain new results on the possibility of positive computable embeddings into the class of linear orderings.