4
$\begingroup$

$\require{AMScd}$ I am studying the proof that the ordering principle does not imply the axiom of choice in Jech's book "The Axiom of Choice" (Section 5.5). Let $P$ be the set of finite partial functions $\omega\times\omega\longrightarrow 2$ and let $B$ be its completion. We consider the symmetric extension $\mathcal N$ obtained from a countable transitive model $M$ of ZFC (+ $V=L$ if you wish) determined by the group all permutations of $\omega$ in $M$ and the finite support filter.

For each finite set $e\subset \omega$, Jech defines a map $u\mapsto u:e$ on $B$ whose algebraic meaning is clear: taking $\bar e = \omega\setminus e$, we have $P\cong P_e\times P_{\bar e}$, where $P_e$ is the set of finite partial functions $e\times\omega\longrightarrow 2$ given by $p\mapsto (p:e,p:\bar e)$, where $p:e = p\cap (e\times\omega\times 2)$, and we have a commutative diagram $$ \begin{CD} B@>>> B_e\times B_{\bar e}\\ @AAA @AAA\\ P@>>> P_e\times P_{\bar e} \end{CD} $$ where $B_e$ y $B_{\bar e}$ are the completions of $P_e$ and $P_{\bar e}$, respectively. Then, the first row isomorphism is denoted by $u\mapsto (u:e,u:\bar e)$, and so the map $u\mapsto u:e$ is the unique complete homomorfism $B\longrightarrow B_e$ extending the restriction map $p\mapsto p:e$ defined on $P$.

However, I have no insight at all about the meaning of $u\mapsto u:e$ with regard to forcing. For instance, in the proof of Lemma 5.23, Jech reduces the proof of equation (5.33) to prove (under suitable hypotheses):

$$ p\cdot (\|\underline v\in \underline x\|: e) = p\cdot (\|\underline v\in \pi\underline x\|:e).\hspace{2cm}(*) $$

My question is: do $\|\phi\|:e$ have any "natural" meaning making equations like this "plausible"? or in other words: Why an equation like $(*)$ should be expected to be true (when the context is known, of course)? Can such equations be translated in a standard way in terms of $\Vdash$?

In fact, Jech says:

Since $\|\underline v\in \underline x\|:e\in B_e$, it suffices to show: For every $q\leq p$ such that support$(q\setminus p)\subseteq e$,

\begin{array}{lrl} (5.36)&(i)& \mbox{if }q\Vdash \underline v\in \underline x, \mbox{ then } (\exists r\leq q)r\Vdash \underline v\in \pi\underline x,\\ &(ii)&\mbox{if }q\Vdash \underline v\notin \underline x, \mbox{ then }(\exists r\leq q)r\Vdash \underline v\notin \pi\underline x. \end{array}

But I cannot see the connection between (5.36) and equation $(*)$ from the algebraic definition of $u\mapsto u:e$. In fact, this is the only step of the whole Section 5.5 that I have not been able to fill myself.

Is there any reason or procedure by which one sees $(*)$ and comes to say "in practice, this means (5.36)"?

Of course, I am interested in this concrete case, but my question is more general than that. For instance, at a previous step, Jech reduces (5.26) to (5.27). In this case I have had no trouble in proving that (5.27) implies (5.26), but still I have the same question: How does one realizes that, in practice, (5.26) means (5.27)? How shoud an equation like (5.27) be thought?

$\endgroup$
8
  • 3
    $\begingroup$ I have to admit that in the three years that I have been constructing symmetric extensions, I have never once computed Boolean values of statements directly. I should also say that I never found the approach via $L(X)$ and $\mathsf{HOD}(X)$ more intuitive than defining an automorphism group and a filter of subgroups. $\endgroup$
    – Asaf Karagila
    Commented Jan 8, 2014 at 14:04
  • 4
    $\begingroup$ Think of $P$ (and therefore $B$) as adjoining an $\omega$-sequence of Cohen reals $a_i$. Then $P_e$ and $B_e$ adjoin just those $a_i$'s for which $i\in e$; I'll call these the $e$-reals. The truth values in $B_e$ are those that depend only on the $e$-reals. Also, $u:e$ is the smallest element of $B_e$ that is $\geq u$ in $B$. So I would think of $\Vert\phi\Vert:e$ as the truth value of the strongest fact that follows from $\phi$ but is only about $e$-reals. $\endgroup$ Commented Jan 8, 2014 at 15:26
  • $\begingroup$ I succeeded in proving the step I mentioned, so please do not worry about it. @Andreas Blass Thank you for the idea. I will try to work it with some examples. $\endgroup$
    – Carlos
    Commented Jan 9, 2014 at 0:24
  • $\begingroup$ By the way, you can (and perhaps should?) use AMScd for drawing diagrams, rather than "by hand arrays". $\endgroup$
    – Asaf Karagila
    Commented Jan 11, 2014 at 14:03
  • $\begingroup$ @AsafKaragila : I tried to do it, but I did not know how to load the package. Now I have consulted the MO meta and I have edited the diagram. Thanks. $\endgroup$
    – Carlos
    Commented Jan 11, 2014 at 16:37

0

You must log in to answer this question.

Browse other questions tagged .