In Cohen Forcing, "Set Theory and the Continuum Hypothesis" a modified Tarski truth definition is taken in the Metatheory as the Forced Truth Relation "$\Vdash$" in a model N. Only information from a countable model M of Set Theory is used in "$\Vdash$" to create a new set G $\in$ N, but G $\notin$ M. G has the property that G $\subset$ K (K $\in$ M).
G is constructed sequentially from a sequence of increasingly long finite logical 'forcing expressions' P$_1$,P$_2$,… which are consistent and each P$_i$ describes which elements of K are in/not in G (e.g. P$_1$={k1 $\in$ G, k2 $\notin$G, …}) , and P$_{i+1}$ $\supseteq$ P$_i$.
The novel feature of "$\Vdash$" is that it allocates each P$_i$ before the full sequence P$_{i+1}$ , P$_{i+2}$ ,… is created. This is achieved, in essence, by modifying the Tarski Truth Definition to create a consistent sequence G := {P$_1$ , P$_2$ , ..} with associated consistent set of expressions A$_r$ describing the model N, True(N) := {A$_1$, A$_2$, .., A$_r$, …} by checking all possible future P$_j$ via "For All P$_j$.." as follows:
P$_i$ $\Vdash$ $\neg$ A$_r$ $\;$ iff $\;$ For all P$_{j}$ $\supseteq$ P$_i$ $\;$ $\;$ P$_j$ $\nVdash$ A$_r$ …………………(1)
and
P$_i$ $\Vdash$ $\;$ A$_r$ $\;$ iff $\;$$\;$ For all P$_{j}$ $\supseteq$ P$_i$ $\;$ $\;$ P$_j$ $\Vdash$ A$_r$ ………………..(2)
To allow the full sequence of P$_i$'s and therefore G:={P$_1$ , P$_2$ , …} <-> {k$_1$ , k$_2$ , …} to be sequentially created, equations (1) & (2) then imply :
For All P$_i$ and A$_r$ there exists a P$_{j}$ $\supseteq$ P$_i$ : Either P$_j$ $\Vdash$ A$_r$ or P$_j$ $\nVdash$ A$_r$ …………………(3)
$\mathbf{My}$ $\mathbf{Questions}$ $\mathbf{Are:}$
(a) The Truth Definition for Forcing looks to have the same overall definition of Tarski Truth. However the "For all P$_j$ $\supseteq$ P$_i$" calculation, which is intended to stop any future elements P$_j$ in G from being inconsistent with earlier elements P$_i$, looks to be a transfinite calculation and not finite or computable. So is the forcing relation computably definable? If 'looking into the future' via equations (1) & (2) was not done, presumably the method would be OK, but just more complicated, but it could be computable ?
(b) The expression "For all P$_{j}$ $\supseteq$ P$_i$ $\;$ P$_j$ $\Vdash$ A$_r$" looks to be equivalent to the infinite expression (the kj aren't in P$_i$, and suppressing the P$_i$ for visual clarity) :
(k1 $\Vdash$ A$_r$ AND $\neg$ k1 $\Vdash$ A$_r$) AND (k2 $\Vdash$ A$_r$ AND $\neg$ k2 $\Vdash$ A$_r$) AND ….. …………………(4)
This means that for any countable (in the Metatheory) X, whether X$\in$M or not, when A$_r$ is the expression "X=G", then the expression would be false, since in effect Equation (4) means that the set X would need to be inconsistent i.e. X = (ki from P$_i$) AND (k1 AND $\neg$k1) AND (k2 AND $\neg$k2)…..}. So for each P$_i$ the equation (4) means that no X can equal G. However, strangely, in the limit as i becomes infinite there will no longer be any inconsistent expressions, so X = G only in this case ?
Best Answer
I think a substantial chunk of your question can be rephrased as follows (and the rest is clarified by the answer to this rephrasing):
Rougly speaking, the point is that they don't - it's only in the presence of a genericity assumption on $G$, which is itself a "global" fact about $G$.
Incidentally, this is closely related to the "Generic Comments" section of my answer to an earlier question, to which I've just made some minor edits for readability (and corrected one major typo).
A good first step towards demystify this is to first think about rather concrete properties - e.g. if we force with finite binary sequences in the usual way, just thinking about the definition of genericity it's clear that we'll have infinitely many $1$s in $G$: for each $k$, the set $D_k$ of conditions which already have at least $k$ many $1$s is dense, so by genericity $G$ has to meet each $D_k$ and hence have infinitely many $1$s.
Phrased in terms of the forcing relation, we've shown that $$\emptyset\Vdash\forall k(\vert G^{-1}(1)\vert\ge k)).$$ So there's an example of some "local" information - in this case, no information at all! - determining some "global" fact about $G$.
The above example probably feels like cheating at first: it wasn't really an individual condition, but rather the genericity requirement, which was doing the heavy lifting. But this is exactly the point! When we say $p\Vdash\varphi$ we don't really mean that the "local" fact that $p\in G$ on its own tells us that $\varphi$ will be true, but rather that this local fact together with the "global" fact that $G$ is sufficiently generic tells us that $\varphi$ will be true.
So we're not magically deducing "global" information from "local" information; rather, we're identifying a certain kind of global information which reduces all information to local information, in the following rough sense:
This kind of "local-to-global-given-global" mechanism is actually something we see all the time - once we replace "global" with "future". For example:
If I'm playing chess, the "local" fact that I have a king and a rook against a king and it's my turn tells me the "global/future" fact that I'm going to win - given the "global/future" fact that I'm going to play optimally.
Suppose I'm seeing, digit-by-digit, the decimal expansion of some number $\theta$. Then I know right away (the "trivial" amount of "local" information) the "global/future" fact that I'll eventually see a digit which is not $3$ ... given the "global/future" fact that $\theta$ is guaranteed to be irrational.
The "global-from-local" principle in forcing (which is one of the two forcing theorems) is really just another example this phenomenon. It is more mysterious at first for two reasons:
The relevant kind of "global guarantee" is $(i)$ rather technical (genericity) and $(ii)$ surprisingly uniform (it works for all appropriately-expressible global questions).
Related to point $(ii)$ above, the global facts we're reducing to local facts via a global guarantee (genericity) are in general very complicated. In the example above, it was obvious how even a little genericity guaranteed that $G$ had infinitely many $1$s; the connection between genericity and the continuum hypothesis is much less clear.
But the underlying nature of the situation is the same.
The above directly answers your first question. It also points the way towards the answer to the second: it's hidden in my observation that
(changed emphasis mine). The point is that the question of whether the generic literally is a given specific thing is not so expressible, so the paradox you describe doesn't occur: for general $X$ (e.g. $X\not\in M$), the fact "$G$ is fully $M$-generic" is not enough to reduce the question "Is $G=X$?" to a local question about $G$.
The forcing theorem doesn't say that genericity reduces all global information to local information; it only applies to some things, namely those expressible in the forcing language.
Let me end with a largely-unrelated but perhaps worthwhile minor point: when you write
the phrasing is ambiguous in a way which might be adding confusion (and even if you're not having an issue at this point, another reader might). So let me clarify: each individual fact about $G$ winds up being determined at some stage during the construction of $G$ (and in particular before $G$ is "completed"), but there is no stage during the construction where all facts about $G$ have been determined.