I'm trying to understand a small part of the definition of forcing on Wikipedia. I'm trying to tackle the parts of (the definition of) forcing that are easiest to understand first. I know what a countable, standard, transitive model of $\mathsf{ZFC}$ is, but not much beyond that. (For example, I know why we have a countable model of $\mathsf{ZFC}$, but not why we're promised a standard, transitive one).
The definition makes reference to a class that's like an expanded version of $V$, called $V(P)$. What is $V(P)$?
Also, if we remove the restrictions on $P$ being atomless and thereby permit $P$ to be finite, what do we get when $P$ is a singleton poset or a two element poset $\{\top, \bot\}$?
Also, are there application of a class like $V(P)$ that are easier to understand than forcing itself?
In the notation $\{ f(x, y, z) : (y, z) \mathop. \varphi(z) \}$, I am using $y$ and $z$ as the variables being quantified over inside the set builder expression. In the above example $x$ is a free variable.
In particular, I'm confused about $V(P)$, $V^{(\mathbb{P})}$ in Wikipedia's notation, where $\mathbb{P}$ is an atomless partial order.
$V(P)$ is defined as follows.
$$ V(P) = \bigcup \{ \text{Name}_P(\alpha) : \alpha \mathop. \alpha \;\; \text{is an ordinal} \} $$
First we have a transfinite recursive definition of $\text{Name}_P$.
$$\text{Name}_P(0) = \varnothing $$ $$\text{Name}_P(\alpha + 1) = 2^{\text{Name}_P(\alpha) \times P}$$ $$\text{Name}_P(\lambda) = \bigcup_{\alpha < \lambda} \text{Name}_P(\alpha)$$
From this definition, we can look at two special cases
- $\text{Name}_P(1) = \{ \varnothing \}$, so $\varnothing$ will eventually end up in $V(P)$.
- $\text{Name}_P(2) = 2^{\{ (\varnothing, p) : p \mathop. p \in P \}} = \{ \{ (\varnothing, p) : p \mathop. p \in P' \land P' \subset P \} : P' \mathop. P' \subset P \} $
And this kind of makes sense.
Based on this answer, I get the intuitive sense that $V(P)$ can be thought of as kind of like an expanded version of $V$ the universe of sets.
At this point I'm going out on a limb and seeing if I can define some elementary set-theoretic stuff in $V(P)$ that looks like familiar stuff like $\in$ and $\cup$ and $\setminus$.
So, a universe of sets has an elementhood relation, and I'd really like to define the analog of that so that $V(P)$ has a little bit more structure to it.
If I squint a little, $P$ is a partial order and kind of feels like a set of truth values.
The first problem that I run in to with that approach is that an element of $V(P)$, interpreted as a relation, associated with more than one element of the poset $P$.
That's okay, $2^P$ kind of looks like a set of truth values too.
I can now define $E : V(P) \times V(P) \to 2^P$ as follows.
$$ E(y, x) \;\;\text{probably should be}\;\; \{ p : (z, p) \mathop. (z, p) \in x \land x = y \} $$
So, the intuition is, when $y$ does occur explicitly in some pairs in $x$, and the truth value we get back is a subset of $P$.
This feels wrong somehow and it feels like I'm not asking the right questions.