The syntactic method is simply to work inside the forcing relation, by looking at what is forced by which conditions. That is, rather than actually building the forcing extension V[G], you reason as though you were inside it, by means of the forcing relation. For example, if you have condition p forcing various statements varphi1, ... varphin, and from those statements you can deduce psi, then you can conclude that p also forces psi. In particular, note that any condition p forces that dotGsubsetcheckP is checkV-generic and contains checkp, so syntactically, you have the filter you want in the sense I described. The point is that you don't actually need to build an actual model using an actually generic filter to gain insight into what is true there, because you have the forcing relation telling you what is forced to be true there.
If you want to build an actual model by forcing over V, then the thing to do is to use Boolean-valued models VB, where there is Boolean-valued truth. You can quotient this B-valued structrue by an ultrafilter U (no need for any genericity) to arrive at an actual first order 2-valued structure VB/U, which satisfies a version of Los' theorem: VB/Umodelsphi if and only if [phi]inU.
For question 2, if you make your choice of b(a) p(a) inside M, then of course f is a function in M. But there is little reason to expect that this function f has much relation to the function in M[G] named by r, since the conditions p(a) might be incompatible. If you can choose a single p=p(a), then it follows that p forces r=checkf.
No comments:
Post a Comment