Corresponding to the semantic relation ⊧Ω there is a quasi-syntactic proof relation ⊢Ω. The “proofs” are certain robust sets of reals (universally Baire sets of reals) and the test structures are models that are “closed” under these proofs. The precise notions of “closure” and “proof” are somewhat technical and so we will pass over them in silence.[7] 