# Aspero Schindler result
$\mathrm{MM}^{++} \implies(*)$
Can be shown that it boils down to adding a satisfying assignment to an infinitary formula via stationary set preserving forcing. This uses universally-Bair sets.
# Side conditions
General method for building and iterating nicely behaved ([[proper forcing|proper]]/[[Semiproper forcing|semiproper]]) forcing notions.
## Pure side conditions
Fix $\theta>\omega_{1}$ regular,
finite $\in$ chains of countable models $M\prec H_{\theta}$.
extension by adding models.
![[Strongly proper forcing#Definition]]
>[!info] Definition
> Let $\mathbb{P}$ be a poset, $\mathcal{S}$ a collection of subsets of $\mathbb{P}$, $A \in \mathcal{S}$. $q$ is *$(A,\mathbb{P})$-strongly generic* if for every $r\leq q$ there is a condition $r|A\in A$ such that if $u\in A$ and $u\leq r|A$ then $u \parallel r$.
>
> Let $\mathbb{P}$ be a poset $\mathbb{P}\in M\prec H_{\theta}$. $q$ is *$(M,\mathbb{P})$-strongly generic* if for every $r\leq q$ there is $r|M\in \mathbb{P}\cap M$ such that if $u\in M$ and $u\leq r|M$ then $u\parallel r$.
> Equivalently $q$ forces that $\dot{G}\cap M$ is **$V$-generic** for $\mathbb{P}\cap M$.
> >[!note] Remark
>$q$ is $(M,\mathbb{P})$-generic if it forces that $\dot{G}\cap M$ is **$M$-generic** for $M\cap \mathbb{P}$.
>
>A poset $\mathbb{P}$ is *strongly proper* if for every $p \in \mathbb{P}$, every sufficiently large $\lambda$ ($\lambda>\left( 2^{|\mathbb{P}|} \right)^{+}$) and every countable $M \prec\left(H_\lambda, \in,<\right)$ containing $\mathbb{P}$ and $p$, there exists a $q \leq p$ that is $(M, \mathbb{P})$-generic.
>[!example] Scaffolding
> $\mathbb{P}\in H_{\theta}$ proper ($\theta\gg|\mathbb{P}|$)
> $\mathbb{S}(\mathbb{P})$ scaffolding of $\mathbb{P}$
> conditions $(\mathcal{M}_{p},w_{p})$ where $w_{p}$ is $(M,\mathbb{P})$-generic for all $M\in \mathcal{M}_{p}$ . Order is extension on both coordinates.
> **Proposition.** the scaffolding is proper.
>[!info] Definition
>$\mathbb{P}$ poset, $\mathbb{P}\in M\prec H_{\theta}$.
>$q$ is $(M,\mathbb{P})$-semigeneric if $\forall r\leq q \forall D\in M$ dense $\exists u\in D$ s.t. $Hull(M,\{u\})\cap \omega_{1}=M\cap \omega_{1}$ s.t. $u\parallel r$
>Where $Hull(M,\{u\})=\{f(u)\mid f\in M, u\in \mathrm{dom}(f)\}$
> Equivalently: $q\Vdash M[\dot{G}\cap\omega_{1}]=M\cap\omega_{1}$
>
> $\mathbb{P}$ is semiproper for $M$ if $\forall p\in M\cap \mathbb{P}\exists q\leq q$ which is $(M,\mathbb{P})$-semigeneric
# General framework
A problem is infinitary propositional formula in variables $\mathcal{V}$
A solution is an assignment $\mu:\mathcal{V}\to \{0,1\}$
One can translate many first order problems to this context.
The question is - can we add a solution by (nice) forcing.
>[!example]
>A formula stating "$\omega_{1}$ is countable".
## CNF formulas in propositional logic
Herbrandt - take a first order formula and convert to a propositional theory.
>[!note] Notation
> An infinitary *CNF formula* is, formally, a set of *clauses* where each clause is a set of *literals* - propositional variables or their negations. We consider clauses as disjunctions and the formula as the conjunction of the clauses.
### Possible satisfaction game
Let $\varphi$ be an infinitary CNF formula Define a game $\mathcal{G}(\varphi)$.
Player I picks $C_{1}\in \varphi$
Player II pick $l_{1}\in C_{1}$ (which we think of as true)
continue with $C_{i}$ and $l_{i}$.
Player II cannot pick $l_{i}$ and $\neg l_{i}$
Closed for player II so determined.
If player I has a winning strategy, there is no assignment satisfying $\varphi$ in any forcing extension.
If player II has a winning strategy, then by collapsing the size of the literal set we get a satisfying assignment.
We can also start with some finite partial assignment.
If $p:\mathrm{dom}(p)\subseteq \mathcal{V}\to \{0,1\}$ is finite partial assignment, we can define the game $\mathcal{G}(\varphi,p)$ where we think of the first moves as done according to $p$.
Define a [[Forcing|poset]] $\mathbb{H}(\varphi)$ (Herbrand's poset):
- Conditions are finite assignments $p$ s.t. player II has a winning strategy in $\mathcal{G}(\varphi,p)$ - the possible satisfaction game starting from $p$.
- $q\leq p \iff q \supseteq p$.
### Adding models - intuitive version
Let $M\prec H_{\theta}$, $\varphi$ a CNF formula and $w\in \mathbb{P}_{0}=\mathbb{H}(\varphi)$. Define the game $\mathcal{G}_{1}(\varphi,M,w)$ where the players choose a descending sequence in $\mathbb{P}_{0}$. First state is $w$. There are two types of moves in state $q$:
1. A move of $\mathcal{G}(\varphi,q)$
2. Player I plays $D\in M$ dense in $\mathbb{P}_{0}$, and player II responds with $u\in D$ such that $Hull(M,\{u\})\cap \omega_{1}=M\cap \omega_{1}$ and there is $q'\leq q,u$. Next state is $q'$.
>[!info] Definition
> $M$ is *1-good* if $\forall w\in \mathbb{P}_{0}\cap M$, $II\uparrow \mathcal{G}_{1}(\varphi,M,w)$
Define $\mathbb{P}_{1}$ such that conditions are $p=(w_{p},\mathcal{M}_{p})$ where
- $w_{p}\in \mathbb{P}_{0}$
- $\mathcal{M}_{p}$ is either $\varnothing$ or $\{M\}$ such that $M$ is $1$-good and $II\uparrow \mathcal{G}(\varphi,M,w_{p})$.
$q\leq p$ if $w_{q}\leq w_{p}$ and $M_{q} \supseteq M_{p}$ but $M_{q}\cap \omega_{1}=M_{p}\cap \omega_{1}$.
We can keep defining $\mathbb{P}_{n}$ in order to add more and more models as side conditions. But then at every step we need to get a larger $\theta'$ from which we take elementary models, and then we might have to go to models which are "too high". We take a different approach.
## Virtual models
Fix $\kappa$ inaccesible.
>[!note] Notation
>$\mathcal{E}=\{ \lambda<\kappa \mid V_{\lambda}\prec V_{\kappa} \}$
>If $M$ is a model, $\hat{M}=$ transitive closure of $M$.
>[!info] Definition
> For $\lambda\in \mathcal{E}$, a *$\lambda$-model* is a countable $M\vDash \mathrm{ZFC}^{-}$ s.t.
>1. $M\prec \hat{M}$
>2. $V_{\lambda}\in M$
>3. $\hat{M}=\mathrm{Hull}(M,V_{\lambda})=\{ f(\bar{x}) \mid f\in M,\bar{x}\in V_{\lambda}\}$
>[!note] Remark
>3. implies that there is at most one $\lambda$ such that a model is a $\lambda$-model.
>[!note] Notation
>$\mathcal{C}_{\lambda}$ - the collection of $\lambda$-models.
>$M\in \bigcup_{\lambda\in \mathcal{E}}\mathcal{C}_{\lambda}$ is called a *virtual model*. For such $M$:
>- $\lambda_{M}$ is the unique $\lambda$ such that $M\in \mathcal{C}_{\lambda}$.
>- $\delta_{M}=\omega_{1}\cap M$.
### Preconditions
Let $\mathbb{P}_{0}=\mathbb{H}(\varphi)$ for some CNF $\varphi$, and define $\mathbb{P}^{*}_{\lambda}$ for $\lambda\in \mathcal{E}\cup \{\kappa\}$. $\mathbb{P}^{*}:=\mathbb{P}^{*}_{\kappa}$.
- Conditions are $p=(\mathcal{M}_{p},w_{p})$ where:
- $w_{p}\in \mathbb{H}(\varphi)$
- $\mathcal{M}_{p}=\{M_{0}\in \dots \in M_{n-1}\}$
- $M_{i}$ is a virtual model
- $\lambda_{M_{0}}<\dots < \lambda_{M_{n-1}}<\lambda$
- $q\leq p$ iff
- $w_{q} \supseteq w_{p}$
- $\forall M\in \mathcal{M}_{p}\exists N\in \mathcal{M}_{q}(M \prec N \land \delta_{M}=\delta_{N})$
For $p\in \mathbb{P}_{\kappa},\lambda\in \mathcal{E}$ denote $p {\restriction} \lambda=(w_{p},\{ M\in \mathcal{M}_{p} \mid \lambda_{m}<\lambda\})$
### Actual conditions
Inductively define $\mathbb{P}_{\lambda}\subseteq \mathbb{P}^{*}_{\lambda}$.
We assume inductively that $\left< \mathbb{P}_{\xi}\mid \xi\in \lambda\cap \mathcal{E} \right>$ is uniformly defined so that $\mathbb{P}_{\xi}\subseteq \mathbb{P}^{*}_{\xi}$.
Given $p \in \mathbb{P}^{*}_{\lambda}$ define a game $\mathcal{G}_{\lambda}(p)$:
- Starting state is $p$.
- At state $q$ there are two possible moves:
- **Working part move:**
- Player I chooses $C\in \varphi$;
- Player II chooses $l\in C$ (such that $\neg l$ wasn't chosen earlier);
- Next state is $q':=(w_{q}\cup \{l\},\mathcal{M}_{q})$.
- **Side condition move:**
- Player I chooses $Q=(M,D)$ where $D\in M\in \mathcal{M}_{q}$, $D\subseteq \mathbb{P}_{\lambda_{M}}$ dense;
- Player II chooses $q'\in D$ compatible with $q$ such that $\mathrm{Hull}(M,\{q'\})\cap \omega_{1}=M\cap \omega_{1}$, and some $q''\leq q,q'$
- Next state is $q''$.
Define $\mathbb{P}_{\lambda}:=\{ p\in \mathbb{P}^{*}_{\lambda} \mid II\uparrow \mathcal{G}_{\lambda}(p)\}$.
>[!note] Remark
>Every $\mathbb{P}_{\lambda}$ adds a satisfying assignment to $\varphi$.
>If $p\leq q$ are in $\mathbb{P}_{\lambda}^{*}$ then $p \in \mathbb{P}_{\lambda}\implies q\in \mathbb{P}_{\lambda}$
>$p\in \mathbb{P}_{\beta}\land \alpha<\beta \implies p{\restriction}\alpha\in\mathbb{P}_{\alpha}$
>$\mathbb{P}_{\beta}\cap \mathbb{P}^{*}_{\alpha}=\mathbb{P}_{\alpha}$
>[!question]
> Is there $\lambda$ which is stationary set preserving?
**The AS condition**. $\varphi$ is *AS-consisnent* if $\forall S \subseteq \omega_{1}$ stat in $V$, the following holds in $V^{\mathrm{Coll}(\omega,<\kappa)}$: $\forall \mu \vDash \varphi$ $\exists j:V\to W$ $crit(j)=\omega_{1}^{V}\in j(S)$, $\exists \hat{\mu} \vDash j(\varphi)$ s.t. $j[\mu]\subseteq \hat{\mu}$.
>[!note] Remark
>Note that $\mu\notin V$ so we can't apply $j$ to it, only take the pointwise image.
**Theorem.** The AS condition implies that $\mathbb{P}_{\kappa}$ is stationary set preserving.
*Sketch.*
>[!info] Definition
>A countable $M\prec H_{\theta}$, $\mathbb{P}_{\kappa}\in M$ is *good* if $\forall p\in \mathbb{P}_{\kappa}\cap M \exists q\leq p \exists \lambda\in \mathcal{E} \ \text{ s.t. } M{\restriction}\lambda\in \mathcal{M}_{q}$ and $\pi(\kappa)=\lambda$ where $\pi:M\to M{\restriction}\lambda$.
>Where $M{\restriction}\lambda$ is the transitive collapse of $M$.
**Proposition.** If $M$ is good then $\mathbb{P}_{\kappa}$ is semiproper for $M$.
*Idea.* The $q$ from the definition will be $(M,\mathbb{P}_{\kappa})$-semigeneric.
**Proposition.** AS condition implies that the set $X:=\{ M\prec H_{\theta} \mid M \text{ is good} \}$ is *projective stationary* i.e. $\forall S \subseteq \omega_{1}$ stationary and $\forall f:H_{\theta}^{<\omega}\to H_{\theta}$, $\exists M\in X (\mathrm{cl}_{f}(M)=M)\land M\cap \omega_{1}\in S$.