Dropping "generic" from the definition of forcing Back when I was first learning about forcing and trying to understand the need to consider generic filters, I came up with the following question.  Suppose we have a countable transitive model $M$.  Let's say that "$p$ pseudoforces $\phi$" if for every filter (not necessarily generic) $G\in P$, $p\in G$ implies that $\phi$ is true in $M[G]$.  Is pseudoforcing definable in $M$?  I'll allow a little wiggle room about what $M[G]$ means when $G$ is not generic, but I suspect that the answer is no, regardless.  Is that correct?
The reason I was led to ask this was that one intuitive justification for why forcing (as standardly defined) is definable in $M$  is that one doesn't need to know anything "specific" about any particular $G$ to decide whether $p$ forces $\phi$.  But this level of handwaving would seem to apply to pseudoforcing as well, so I think would be illuminating to understand exactly how genericity comes into play here.

EDIT in response to Joel David Hamkins's request that I clarify what I mean by $M[G]$ when $G$ is not generic: I'm going to forget about Boolean-valued models and follow the approach in Kunen's textbook.  We have an arbitrary poset $P$ in our countable transitive model $M$ of ZFC.  We take the usual definition of a $P$-name: $\tau$ is a $P$-name if and only if $\tau$ is a relation and for all $\langle \sigma,p\rangle \in \tau$, $\sigma$ is a $P$-name and $p\in P$.  Next we have define how to evaluate $\tau$ at $G\subseteq P$, but again we can just use the standard definition:
$$\tau_G = \{ \sigma_G \mid \exists p\in G : \langle\sigma,p\rangle \in \tau\}.$$
Then $M[G]$ is defined to be the set of all $\tau_G$ as $\tau$ ranges over all $P$-names in $M$.  This is already a non-trivial construction because Kunen shows that if $G$ is any nonempty filter then $M[G]$ satisfies Extensionality, Foundation, Pairing, and Union.
Now it seems to me that I can define $p \mathrel{?\mathord{\vdash}} \phi$ (read "$p$ pseudoforces $\phi$") analogously to $p\Vdash\phi$ simply by dropping the word "generic" from the definition—instead of "for all generic filters $G$" we say "for all filters $G$." What goes wrong? My guess, based on something Andreas Blass once told me, is that we run into trouble when we try to prove the definability of pseudoforcing.
A related question is this. Kunen proves two crucial facts about forcing; (1) it's definable, and (2) every $\phi$ that is true in $M[G]$ is forced by some $p\in G$. Suppose I formulate the conjecture that these two facts are also true of pseudoforcing.  Could I then deduce that $M[G]$ satisfies ZFC from this conjecture?  Since the conjecture is false (see Goldstern's comment about part (2)), the answer to this question is yes for trivial reasons, but what I'm trying to get at is whether the genericity of $G$ is primarily needed in order to prove these two crucial facts, and that the rest of the proof that $M[G]$ satisfies ZFC follows "formally" from them.
 A: If you use all ultrafilters instead of all filters, then the pseudo-forcing relation is definable because it will be the same as the usual forcing relation. 
Specifically, I am referring to ultrafilters on the Boolean algebra, but if you want to use partial orders, then I am talking about the filters on the partial order that generate ultrafilters on the Boolean completion. With these filters, you get a sensible meaning for  $M[G]$ simply as the quotient of the space of the set of $P$-names, and this is the usual concept of the Boolean ultrapower. If I recall correctly, I believe you undertook this quotient construction in your (excellent) notes Beginner's guide to forcing. 
The main point is that the quotient construction works regardless of whether the filter is generic, provided only that it is an ultrafilter on the Boolean completion. The property of a filter that it generates an ultrafilter on the Boolean algebra can be viewed as a weak form of genericity, and we discuss this with several examples and a characterization in the Boolean ultrapower paper. 
Indeed, being an ultrafilter is itself a kind of genericity, since a filter is an ultrafilter on a Boolean algebra just in case it meets all maximal antichains of size $2$. 
If you define pseudo-forcing using ultrafilters in this way, then it will agree completely with the usual genericity notion, since a condition $p$ forces $\varphi$ in $M[G]$ in the ultrafilter sense just in case the Boolean value of $\varphi$ is at least $p$. This is a consequence of the  Łoś theorem for Boolean ultrapowers, namely, that $M[G]=M^B/G\models\varphi$ just in case $[\![\varphi]\!]\in G$, whenever $G\subset B$ is any ultrafilter. 
In particular, the pseudo-forcing relation will be definable this way, since the Boolean values $[\![\varphi]\!]$ are definable in $M$.
Meanwhile, one can characterize the genericity of the ultrafilter $G\subset B$ as equivalent to the assertion that the ground model of $M[G]$ is precisely $M$: the Boolean ultrapower of $M$ is the isomorphism. This is theorem 16 in my Boolean ultrapower paper linked above.
A: In a way what I am going to say here echoes what Joel has already mentioned in his comments above (*I suppose in that case one would want M[F] to be some kind of reduced power, analogous to what you get with ultrapowers by a filter in place of an ultrafilter. Thus, one might take M[F] naturally as a B/F-valued model), but with some twist.
Let us start at 10000 feet: set theorists use boolean valued models, to expand their universe with "fictional sets", and then use the  ultrafilter to "mod-out" and get back a "real universe" (ie a $2$-valued boolean model), which happens to contain the original one.
Nothing wrong with that, of course, but  (quoting Tim) " to make sure that the usual semantics aren't giving us tunnel vision and preventing us from seeing alternative possibilities", we need to take a slightly different stance, namely this principle:
        ALL BOOLEAN  MODELS ARE CREATED EQUAL

all boolean valued models ARE models, albeit not necessarily 2-valued
(this perspective is in fact the one that a topos approach to set theory can easily accomodate: each boolean valued model is a Boolean Topos (see here), which in turn is a perfectly legitimate universe of sets, and moreover is a universe of sets whose internal logic is boolean (so essentially classic).
Now, start with a ordinary 2-valued model $M$. Let us denote by $BOOL(M)$ the boolean multiverse grounded in M, ie the category of boolean valued models built from  every complete boolean algebra in $M$ ( I said it is a category, because you can define maps between them that preserve the evaluation, details are missing in action, but it can be done).
$BOOL(M)$ is a lovely (multi) place to be: for instance, it contains an initial universe, namely $M$ itself, as the initial object of the category.
Now, onto Tim's question: what happens to the filters of a specific algebra $B$ ? Well, every filter corresponds to  an algebra surjection, from $B$ to $B/F$, and  that in turn maps $U_1 = M^{\mathbb B}$ to  $U_2 =\frac{ M^{\mathbb B}} {F}$ (for a definition see addendum point 3).
So, in a way, the universe $U_1$  contracts to $U_2$, much the same way as with original forcing, with one big difference: the resulting $U_2$ is not 2-valued, unless $F$ is an ultrafilter.
Now, what shall we do with $U_2$? We can do model theory, just like with all others, no more no less.
But perhaps more interesting is this view:  we can have several ultrafilters completing $F$, each of them being a "Cohen extension " of the new "ground model" . It is as if $F$ is a tree and the ultrafilters are the leaves.
Conjecture: what is true in $U_2 =\frac{ M^{\mathbb B}} {F}$. is the common denominator of all Cohen universes which are its leaves. In this respect this model is exactly like $M$, except that it is a boolean version of $M$: all Cohen universes in the category are extensions of $M$ but only some are of $U_2 =\frac{ M^{\mathbb B}} {F}$.
ADDENDUM (as a long back and forth between your truly and Gabe Goldberg asks for some additional clarifications)

*

*As noted by Gabe, I need more than any filter F to do the trick. F must be such that moding out by it we still get a complete boolean algebra. F must be closed with respect to arbitrary infs

*Gabe also asked several questions about $BOOL(M)$ and how it is defined. Now, the first thing to understand is that there are TWO such categories (they are actually 2-cats, because each object is a boolean topos): the first is the one whose objects are $M^{\mathbb B}$ where $B \epsilon M$ and the maps are also in $M$. This cat I call VBOOL(M), for visible (from M) boolean multiverse. Then there is also a 2-cat whose objects are the same but maps exists outside of $M$, you can call it as you like, say FBOOL(M), for the full boolean M- grounded multiverse.

*IMPORTANT  Gabe has also objected to my former notation above:  $M^{\mathbb B/F}$ . HE IS RIGHT: that notation makes it look as if I take M and I create the boolean universe on the boolean algebra $B/F$, which is patently wrong (else in the case of an ultrafilter I would end up where I started, namely M. Please replace that notation with this: $\frac{ M^{\mathbb B}} {F}$. The intended meaning is the obvious one: make all the sentences in $M^{\mathbb B}$ which happen to be forced by element of F true.

Incidentally, for the category minded folks, both cats are presheaves over the small category of boolean algebras in M, but that is another story.
So, VBOOL(M) is a sub-cat of  FBOOL(M), and in the larger cat there are all the maps one needs to talk about forcing extensions, and also for Tim's poor man version of forcing using a filter.
A: Your setting is not completely clear to me, but I claim that the truth lemma fails. Here is the argument:
Let $H$ be a filter which is not generic and let $D$ be a dense set in $M$ not intersecting $H$. Let $a$ be the canonical name for $D$, and let $c$ be the canonical name usually given for the (generic) filter.
Then, $M[H]\models \neg\exists x; (x\in D\cap H)$.
So, assuming the truth lemma,
$\exists p\in H; p\Vdash \neg\exists x; (x\in a\cap c)$.
Fix such a $p\in H$.
Since the definition of forcing a negation can be easily recovered, we have that
$\forall q\leq p; q\not\Vdash\exists x;(x\in a\cap c)$.
Since $D$ is dense, there is a $q\leq p$ such that $q\in D$. Fix such a $q$.
Now, $q\in D$, so
$\forall F\ni q; M[F]\models q\in D\cap F$.
Therefore,
$\forall F\ni q; M[F]\models \exists x; (x\in D\cap F)$
and $q\Vdash \exists x; x\in a\cap c$, a contradiction.
