A model in which the Separation principle holds for a given effective projective Sigma-class

TL;DR

This paper proves that for any n≥3, there exists a generic extension of the constructible universe where the Separation principle holds for effective projective classes, using advanced forcing techniques.

Contribution

It provides the first complete proof that the Separation principle holds for effective classes in certain generic extensions, extending Harrington's earlier partial results.

Findings

Separation principle holds for effective classes in the constructed extension.

The proof uses a countable product of almost-disjoint forcing notions.

The result confirms a long-standing conjecture for n≥3.

Abstract

In this paper, we prove the following: If $n\ge3$, there is a generic extension of $L$ -- the constructible universe -- in which it is true that the Separation principle holds for both effective (lightface) classes $\varSigma^1_n$ and $\varPi^1_n$ for sets of integers. The result was announced long ago by Leo Harrington with a sketch of the proof for $n=3$; its full proof has never been presented. Our methods are based on a countable product of almost-disjoint forcing notions independent in the sense of Jensen--Solovay.