PFA and the definability of the nonstationary ideal

TL;DR

The paper addresses whether the nonstationary ideal on $\omega_1$ can be made $\Pi_1$-definable in a model of ${\sf PFA}$. It introduces a coding/certification framework built on a two-phase forcing: add a partition of $\omega_1$ via ${\rm Col}(\omega_1,\omega_1)$ and run a countable-support iteration interleaving certification forcings with the ${\sf PFA}$ iteration, guided by a supercompact Laver function. This yields a model $V[g]$ in which ${\sf PFA}$ holds, ${\sf NS}_{\omega_1}$ is $\Pi_1$-definable relative to a parameter from $H_{\aleph_2}$, and ${\sf CFB}$ fails (with ${\sf NS}_{\omega_1}$ not saturated). The construction demonstrates a robust method to code ideals via certification that is absolute to stationary-set-preserving extensions, with potential applicability to other ideals. The results have implications for the definability strength of the NS-ideal under strong forcing axioms.

Abstract

We produce, relative to a ${\sf ZFC}$ model with a supercompact cardinal, a ${\sf ZFC}$ model of the Proper Forcing Axiom in which the nonstationary ideal on $ω_1$ is $Π_1$-definable in a parameter from $H_{\aleph_2}$.

Theorems & Definitions (15)

• Theorem 1.1
• Lemma 2.1
• proof
• Lemma 2.2
• proof
• Lemma 2.3
• proof
• Lemma 2.4
• Definition 3.1
• Lemma 3.2