Baumgartner's finite-condition generic club forcing is proper

Let $M$ be a relevant countable elementary submodel, let $p\in \mathbb{B}\cap M$, and put $\delta =M\cap {\omega }_1$. Then $M\cap {\omega }_1$ is an initial segment with no largest member, so $\delta$ is a countable limit ordinal. By elementarity choose in $M$ a normal $h:{\omega }_1\to {\omega }_1$ extending $p$. For every $\alpha <\delta$, both $\alpha$ and $h(\alpha )$ belong to $M\cap {\omega }_1$, while $h(\alpha )\ge \alpha$; hence $\sup h\mathrm{‘}\mathrm{‘}\delta =\delta$ and continuity gives $h(\delta )=\delta$. Thus $q=p\cup \{(\delta ,\delta )\}$ belongs to $\mathbb{B}$ and satisfies $q\le p$.

For each $\alpha <{\omega }_1$, the set $E_{\alpha }=\{p:\alpha \in \mathrm{dom}(p)\}$ is dense: extend a witness normal function for $p$ and add its value at $\alpha$. Directedness of $G$ makes $F=\bigcup G$ a function, and meeting all $E_{\alpha }$ makes it total. Given $\alpha <\beta$, take two filter conditions specifying the two values and a common stronger condition; its normal extension shows $F(\alpha )<F(\beta )$.

Fix $r\le q$. Any normal extension of $r$ contains $(\delta ,\delta )$, so strict increase gives $\alpha <\delta ⟺r(\alpha )<\delta$ for every $\alpha \in \mathrm{dom}(r)$. Consequently $s=r\cap M$ is exactly the part of $r$ whose coordinates and values lie below $\delta$. It is a finite condition, belongs to $M$, and is extended by $r$. If $D\in M$ is dense, elementarity supplies $r^{\mathrm{\prime }}\in D\cap M$ with $r^{\mathrm{\prime }}\le s$. Every coordinate and value of the finite $r^{\mathrm{\prime }}$ lies below $\delta$.

Let $\delta <{\omega }_1$ be a nonzero limit and put $\gamma =\sup F\mathrm{‘}\mathrm{‘}\delta \le F(\delta )=\beta$. Suppose $\gamma <\beta$, and choose $p\in G$ containing $(\delta ,\beta )$. Below $p$, conditions which specify some $(\alpha ,\rho )$ with $\alpha <\delta$ and $\gamma <\rho <\beta$ are dense. Indeed, from any $s\le p$, take a normal extension $u$; continuity at $\delta$ gives an $\alpha <\delta$, beyond the finite lower domain of $s$, with $\gamma <u(\alpha )<\beta$, and add $(\alpha ,u(\alpha ))$. A generic containing $p$ meets this dense-below-$p$ set (equivalently, adjoin the conditions incompatible with $p$ to make it globally dense), contradicting the definition of $\gamma$. Hence $F(\delta )=\sup F\mathrm{‘}\mathrm{‘}\delta$, and $F$ is normal.

The conditions $r$ and $r^{\mathrm{\prime }}$ are compatible. To verify the point suppressed by the usual proof, choose a normal $u$ extending $r$. By elementarity choose a normal $v\in M$ extending $r^{\mathrm{\prime }}$. Both satisfy $u(\delta )=v(\delta )=\delta$: for $u$ this follows from $(\delta ,\delta )\in r$, and for $v$ by the calculation in step 1.1. Splice $v$ below and at $\delta$ with $u$ above $\delta$. The result is normal: both pieces agree at $\delta$, their values on the lower piece are below $\delta$, and replacing the lower piece by another sequence cofinal in $\delta$ does not change continuity at any later limit. It extends $r\cup r^{\mathrm{\prime }}$, so that finite union is a common condition. Therefore $D\cap M$ is predense below $q$. By F1 and F2, $q$ is an $(M,\mathbb{B})$-master below $p$, and $\mathbb{B}$ is proper.

The range $C=F\mathrm{‘}\mathrm{‘}{\omega }_1$ is unbounded because strict increase implies $F(\alpha )\ge \alpha$. It is closed: if $\eta <{\omega }_1$ is a limit point of $C$, then $\xi =\sup \{\alpha :F(\alpha )<\eta \}$ is a nonzero limit below ${\omega }_1$, and continuity and cofinality of the selected values give $F(\xi )=\eta$. Thus $C$ is club by F3.

Finally fix any ground-model normal function $a:{\omega }_1\to {\omega }_1$. The set $E_a=\{p\in \mathbb{B}:(\mathrm{\exists }\alpha \in \mathrm{dom}(p))p(\alpha )\mathrm{\ne }a(\alpha )\}$ is dense. Given $p$, choose a normal extension $u$, a successor $\alpha$ above its finite domain, and two successive values above $u(\alpha )$; at least one differs from $a(\alpha )$, and replacing the value at that new successor by the chosen larger value and continuing normally witnesses an extension in $E_a$. Genericity makes $F\mathrm{\ne }a$ for every ground normal $a$. If $C$ were in the ground model, its increasing enumeration would be a ground normal function and, as the unique increasing bijection from ${\omega }_1$ onto $C$, would equal $F$. This contradiction proves that the club $C$ is new. The forcing is nonempty (the empty map is greatest), and all finite, singleton, zero-coordinate, and limit-coordinate cases used above are included.