A better way to explain forcing? Let me begin by formulating a concrete (if not 100% precise) question, and then I'll explain what my real agenda is.
Two key facts about forcing are (1) the definability of forcing; i.e., the existence of a notion $\Vdash^\star$ (to use Kunen's notation) such that $p\Vdash \phi$ if and only if $(p \Vdash^\star \phi)^M$, and (2) the truth lemma; i.e., anything true in $M[G]$ is forced by some $p\in G$.
I am wondering if there is a way to "axiomatize" these facts by saying what properties forcing must have, without actually introducing a poset or saying that $G$ is a generic filter or that forcing is a statement about all generic filters, etc.  And when I say that forcing "must have" these properties, I mean that by using these axioms, we can go ahead and prove that $M[G]$ satisfies ZFC, and only worry later about how to construct something that satisfies the axioms.

Now for my hidden agenda.  As some readers know, I have written A beginner's guide to forcing where I try to give a motivated exposition of forcing.  But I am not entirely satisfied with it, and I have recently been having some interesting email conversations with Scott Aaronson that have prompted me to revisit this topic.
I am (and I think Scott is) fairly comfortable with the exposition up to the point where one recognizes that it would be nice if one could add some function $F : \aleph_2^M \times \aleph_0 \to \lbrace 0,1\rbrace$ to a countable transitive model $M$ to get a bigger countable transitive model $M[F]$.  It's also easy to grasp, by analogy from algebra, that one also needs to add further sets "generated by $F$."  And with some more thought, one can see that adding arbitrary sets to $M$ can create contradictions, and that even if you pick an $F$ that is "safe," it's not immediately clear how to add a set that (for example) plays the role of the power set of $F$, since the "true" powerset of $F$ (in $\mathbf{V}$) is clearly the wrong thing to add.  It's even vaguely plausible that one might want to introduce "names" of some sort to label the things you want to add, and to keep track of the relations between them, before you commit to saying exactly what these names are names of. But then there seems to be a big conceptual leap to saying, "Okay, so now instead of $F$ itself, let's focus on the poset $P$ of finite partial functions, and a generic filter $G$.  And here's a funny recursive definition of $P$-names."  Who ordered all that?
In Cohen's own account of the discovery of forcing, he wrote:

There are certainly moments in any mathematical discovery when the resolution of a problem takes place at such a subconscious level that, in retrospect, it seems impossible to dissect it and explain its origin. Rather, the entire idea presents itself at once, often perhaps in a vague form, but gradually becomes more precise.

So a 100% motivated exposition may be a tad ambitious.  However, it occurs to me that the following strategy might be fruitful.  Take one of the subtler axioms, such as Comprehension or Powerset.  We can "cheat" by looking at the textbook proof that $M[G]$ satisfies the axiom.  This proof is actually fairly short and intuitive if you are willing to take for granted certain things, such as the meaningfulness of this funny $\Vdash$ symbol and its two key properties (definability and the truth lemma).  The question I have is whether we can actually produce a rigorous proof that proceeds "backwards": We don't give the usual definitions of a generic filter or of $\Vdash$ or even of $M[G]$, but just give the bare minimum that is needed to make sense of the proof that $M[G]$ satisfies ZFC.  Then we "backsolve" to figure out that we need to introduce a poset and a generic filter in order to construct something that satisfies the axioms.
If this can be made to work, then I think it would greatly help "ordinary mathematicians" grasp the proof.  In ordinary mathematics, expanding a structure $M$ to a larger structure $M[G]$ never requires anything as elaborate as the forcing machinery, so it feels like you're getting blindsided by some deus ex machina.  Of course the reason is that the axioms of ZFC are so darn complicated.  So it would be nice if one could explain what's going on by first looking at what is needed to prove that $M[G]$ satisfies ZFC, and use that to motivate the introduction of a poset, etc.
By the way, I suspect that in practice, many people learn this stuff somewhat "backwards" already.  Certainly, on my first pass through Kunen's book, I skipped the ugly technical proof of the definability of forcing and went directly to the proof that $M[G]$ satisfies ZFC.  So the question is whether one can push this backwards approach even further, and postpone even the introduction of the poset until after one sees why a poset is needed.
 A: I have proposed such an axiomatization. It is published in Comptes Rendus: Mathématique, which has returned to the Académie des Sciences in 2020 and is now completely open access. Here is a link:
https://doi.org/10.5802/crmath.97
The axiomatization I have proposed is as follows:
Let $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C)$ be a quintuple such that:

*

*$M$ is a transitive model of $ZFC$.


*$\mathbb P$ is a partial ordering with maximum.


*$R$ is a definable in $M$ and absolute ternary relation (the $\mathbb P$-membership relation, usually denoted by $M\models a\in_p b$).


*$\Vdash\phi$ is, if $\phi$ is a formula with $n$ free variables, a definable $n+1$-ary predicate in $M$ called the forcing predicate corresponding to $\phi$.


*$C$ is a predicate (the genericity predicate).
As usual, we use $G$ to denote a filter satisfying the genericity predicate $C$.
Assume that the following axioms hold:
(1) The downward closedness of forcing: Given a formula $\phi$, for all $\overline{a}$, $p$ and $q$, if $M\models (p\Vdash\phi)[\overline{a}]$ and $q\leq p$, then $M\models (q\Vdash\phi)[\overline{a}]$.
(2) The downward closedness of $\mathbb P$-membership: For all $p$, $q$, $a$ and $b$, if $M\models a\in_p b$ and $q\leq p$, then $M\models a\in_q b$.
(3) The well-foundedness axiom: The binary relation $\exists p; M\models a\in_p b$ is well-founded and well-founded in $M$. In particular, it is left-small in $M$, that is,
$\left\{a : \exists p; M\models a\in_p b\right\}$ is a set in $M$.
(4) The generic existence axiom: For each $p\in \mathbb P$, there is a generic filter $G$ containing $p$ as an element.
Let $F_G$ denote the transitive collapse of the well-founded relation $\exists p\in G; M\models a\in_p b$.
(5) The canonical naming for individuals axiom: $\forall a\in M;\exists b\in M; \forall G; F_G(b)=a$.
(6) The canonical naming for $G$ axiom: $\exists c\in M;\forall G; F_G(c)= G$.
Let $M[G]$ denote the direct image of $M$ under $F_G$. The next two axioms are the fundamental duality that you have mentioned:
(7) $M[G]\models \phi[F_G(\overline{a})]$ iff $\exists p\in G; M\models (p\Vdash\phi)[\overline{a}]$, for all $\phi$, $\overline{a}$, $G$.
(8) $M\models (p\Vdash\phi)[\overline{a}]$ iff $\forall G\ni p; M[G]\models \phi[F_G(\overline{a})]$, for all $\phi$, $\overline{a}$, $p$.
Finally, the universality of $\mathbb P$-membership axiom.
(9) Given an individual $a$, if $a$ is a downward closed relation between individuals and conditions, then there is a $\mathbb P$-imitation $c$ of $a$, that is, $M\models b\in_p c$ iff $(b,p)\in a$, for all $b$ and $p$.
It follows that $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C, G)$ represent a standard forcing-generic extension: The usual definitions of the forcing predicates can be recovered, the usual definition of genericity can also be recovered ($G$ intersects every dense set in $M$), $M[G]$ is a model of $ZFC$ determined by $M$ and $G$ and it is the least such model. (Axiom $(9)$ is used only in the proof that $M[G]$ is a model).
A: This is an expansion of David Roberts's comment.  It may not be the sort of answer you thought you were looking for, but I think it is appropriate, among other reasons because it directly addresses your question

if there is a way to "axiomatize" these facts by saying what properties forcing must have.

In fact, modern mathematics has developed a powerful and general language for "axiomatizing properties that objects must have": the use of universal properties in category theory.  In particular, universal properties give a precise and flexible way to say what it means to "freely" or "generically" add something to a structure.
For example, suppose we have a ring $R$ and we want to "generically" add a new element.  The language of universal properties says that this should be a ring $R[x]$ equipped with a homomorphism $c:R\to R[x]$ and an element $x\in R[x]$ with the following universal property: for any ring $S$ equipped with a homomorphism $f:R\to S$ and an element $s\in S$, there exists a unique homomorphism $h:R[x]\to S$ such that $h\circ c = f$ and $h(x) = s$.
Note that this says nothing about how $R[x]$ might be constructed, or even whether it exists: it's only about how it behaves.  But this behavior is sufficient to characterize $R[x]$ up to unique isomorphism, if it exists.  And indeed it does exist, but to show this we have to give a construction: in this case we can of course use the ring of formal polynomials $a_n x^n + \cdots + a_1 x + a_0$.
From this perspective, if we want to add a function $F : \aleph_2\times \aleph_0 \to 2$ to a model $M$ of ZFC to obtain a new model $M[F]$, the correct thing to do would be to find a notion of "homomorphism of models" such that $M[F]$ can be characterized by a similar universal property: there would be a homomorphism $c:M\to M[F]$ and an $F : \aleph_2\times \aleph_0 \to 2$ in $M[F]$, such that for any model $N$ equipped with a homomorphism $f:M\to N$ and a $G : \aleph_2\times \aleph_0 \to 2$ in $N$, there is a unique homomorphism $h:M[F]\to N$ such that $h\circ c = f$ and $h(F) = G$.
The problem is that the usual phrasing of ZFC, in terms of a collection of things called "sets" with a membership relation $\in$ satisfying a list of axioms in the language of one-sorted first-order logic, is not conducive to defining such a notion of homomorphism.  However, there is an equivalent formulation of ZFC, first given by Lawvere in 1964, that works much better for this purpose.  (Amusingly, 1964 is exactly halfway between 1908, when Zermelo first proposed his list of axioms for set theory, and the current year 2020.)  In Lawvere's formulation, there is a collection of things called "sets" (although they behave differently than the "sets" in the usual presentation of ZFC) and also a separate collection of things called "functions", which together form a category (i.e. functions have sets as domain and codomain, and can be composed), and satisfy a list of axioms written in the language of category theory.  (A recent short introduction to Lawvere's theory is this article by Tom Leinster.)
Lawvere's theory is usually called "ETCS+R" (the "Elementary Theory of the Category of Sets with Replacement"), but I want to emphasize that it is really an entirely equivalent formulation of ZFC.  That is, there is a bijection between models of ZFC, up to isomorphism, and models of ETCS+R, up to equivalence of categories.  In one direction this is exceedingly simple: given a model of ZFC, the sets and functions therein as usually defined form a model of ETCS+R.  Constructing an inverse bijection is more complicated, but the basic idea is the Mostowski collapse lemma: well-founded extensional relations can be defined in ETCS+R, and the relations of this sort in any model of ETCS+R form a model of ZFC.
Since a model of ETCS+R is a structured category, there is a straightforward notion of morphism between models: a functor that preserves all the specified structure.  However, this notion of morphism has two defects.
The first is that the resulting category of models of ETCS+R is ill-behaved.  In particular, the sort of "free constructions" we are interested in do not exist in it!  However, this is a problem of a sort that is familiar in modern structural mathematics: when a category is ill-behaved, often it is because we have imposed too many "niceness" restrictions on its objects, and we can recover a better-behaved category by including more "ill-behaved" objects.  For instance, the category of manifolds does not have all limits and colimits, but it sits inside various categories of more general "smooth spaces" that do.  The same thing happens here: by dropping two of the axioms of ETCS+R we obtain the notion of an elementary topos, and the category of elementary toposes, with functors that preserve all their structure (called "logical functors"), is much better-behaved.  In particular, we can "freely adjoin a new object/morphism" to an elementary topos.
(I am eliding here the issue of the replacement/collection axiom, which is trickier to treat correctly for general elementary toposes.  But since my main point is that this direction is a blind alley for the purposes of forcing anyway, it doesn't matter.)
The second problem, however, is that these free constructions of elementary toposes do not have very explicit descriptions.  This is important because our goal is not merely to freely adjoin an $F:\aleph_2\times \aleph_0 \to 2$, but to show that the existence of such an $F$ is consistent, and for this purpose we need to know that when we freely adjoin such an $F$ the result is nontrivial.  Thus, in addition to characterizing $M[F]$ by a universal property, we need some concrete construction of it that we can inspect to deduce its nontriviality.
This problem is solved by imposing a different niceness condition on the objects of our category and changing the notion of morphism.  A Grothendieck topos is an elementary topos that, as a category, is complete and cocomplete and has a small generating set.  But, as shown by Giraud's famous theorem, it can equivalently be defined as a cocomplete category with finite limits and a small generating set where the finite limits and small colimits colimits interact nicely.  This suggests a different notion of morphism between Grothendieck toposes: a functor preserving finite limits and small colimits.  Let's call such a functor a Giraud homomorphism (it's the same as a "geometric morphism", but pointing in the opposite direction).
The category of Grothendieck toposes and Giraud homomorphisms is well-behaved, and in particular we can freely adjoin all sorts of structures to a Grothendieck topos -- specifically, any structure definable in terms of finite limits and arbitrary colimits (called "a model of a geometric theory").  (To be precise, this is a 2-category rather than a category, and the universal properties are up to isomorphism, but this is a detail, and unsurprising given the modern understanding of abstract mathematics.)  Moreover, the topos $M[G]$ obtained by freely adjoining a model $G$ of some geometric theory to a Grothendieck topos $M$ -- called the classifying topos of the theory of $G$ -- has an explicit description in terms of $M$-valued "sheaves" on the syntax of the theory of $G$.  This description allows us to check, in any particular case, that it is nontrivial.  But for other purposes, it suffices to know the universal property of $M[G]$.  In this sense, the universal property of a classifying topos is an answer to your question:

when I say that forcing "must have" these properties, I mean that by using these axioms, we can go ahead and prove that $M[G]$ satisfies ZFC, and only worry later about how to construct something that satisfies the axioms.

Only one thing is missing: not every Grothendieck topos is a model of ETCS+R, hence $M[G]$ may not itself directly yield a model of ZFC.  We solve this in three steps.  First, since ZFC satisfies classical logic rather than intuitionistic logic (the natural logic of categories), we force $M[G]$ to become Boolean.  Second, by restricting to "propositional" geometric theories we ensure that the result also satisfies the axiom of choice.  Finally, we pass to the "internal logic" of the topos, which is to say that we allow "truth values" lying in its subobject classifier rather than in the global poset of truth values $2$.  We thereby get an "internal" model of ETCS+R, and hence also an "internal" model of ZFC.
So where does the complicated machinery in the usual presentation of forcing come from?  Mostly, it comes from "beta-reducing" this abstract picture, writing out explicitly the meaning of "well-founded extensional relation internal to Boolean sheaves on the syntax of a propositional geometric theory".  The syntax of a propositional geometric theory yields, as its Lindenbaum algebra, a poset.  The Boolean sheaves on that poset are, roughly, those that satisfy the usual "denseness" condition in forcing.  The "internal logic" valued in the subobject classifier corresponds to the forcing relation over the poset.  And the construction of well-founded extensional relations translates to the recursive construction of "names".
(Side note: this yields the "Boolean-valued models" presentation of forcing.  The other version, where we take $M$ to be countable inside some larger model of ZFC and $G$ to be an actual generic filter living in that larger model, is, at least to first approximation, an unnecessary complication.  By comparison (and in jesting reference to Asaf's answer), if we want to adjoin a new transcendental to the field $\mathbb{Q}$, we can simply construct the field of rational functions $\mathbb{Q}(x)$.  From the perspective of modern structural mathematics, all we care about are the intrinsic properties of $\mathbb{Q}(x)$; it's irrelevant whether it happens to be embeddable in some given larger field like $\mathbb{R}$ by setting $x=\pi$.)
The final point is that it's not necessary to do this beta-reduction.  As usual in mathematics, we get a clearer conceptual picture, and have less work to do, when working at an appropriate level of abstraction.  We prove the equivalence of ZFC and ETCS+R once, abstractly.  Similarly, we show that we have an "internal" model of ETCS+R in any Grothendieck topos.  These proofs are easier to write and understand in category-theoretic language, using the intrinsic characterization of Grothendieck toposes rather than anything to do with sites or sheaves.  With that done, the work of forcing for a specific geometric theory is reduced to understanding the relevant properties of its category of Boolean sheaves, which are simple algebraic structures.
A: Great Question! Finally someone asks the simplest questions, which almost invariably are the real critical ones (if I cannot explain a great idea to an intelligent person in minutes, it simply means I do not understand it).
In this case, the idea is one of the greatest in modern history.
Let me start with a historical background: in the  90s I talked with Stan Tennenbaum about Forcing, hoping to (finally!)  understand it (did not go too far) . Here is what he told me (not verbatim): during those times,late 50s and very early 60s,  several folks were trying their hand to prove independence.
What did they know? They certainly knew that they had to add a set G to the minimal model, and then close up with respect to  Godel constructibility operations. So far nothing mysterious: it is a bit like adding a complex number to Q and form an algebraic field.
First blocker: if I add a set G which certainly exists to construct the function you described above, how do I know that M[G] is still a model of ZF?
In algebraic number theory I do not have this issue, I simply take the new number , and throw it into the pot, but here I do. Sets carry along information, and some of this information can be devastating (simple example: suppose that G is gonna tell that the first ordinal outside of  M is in fact reachable, that would be very bad news.
All this was known to the smart folks at the time. What they did not know is: very well, I am in a mine field, how then I select my G so it does not create trouble and do what is supposed to do? That is the fundamental question.
They wanted to find G,  describe it, and then add it.
Enter Cohen. In a majestic feat of mathematical innovation, Cohen, rather than going into the mine field outside of M searching for the ideal G, enters M. He looks at the world outside, so to speak, from inside (I like to think of him looking at the starry sky, call it  V, from his little M).
Rather than finding the mysterious G which floats freely  in the hyperspace outside M, he says: ok, suppose I wanted to build G, brick by brick, inside M. After all, I know what is supposed to do for me, right? Problem is,  I cannot, because if I could it would be constructible in M, and therefore part of M. Back to square one.
BUT: although G is not constructible in M, all its finite portions are, assuming such a G is available in the outer world. It does not exist in M, but the bricks which make it (in your example all the finite approximation of the function), all of them,  are there. Moreover, these finite fragments can be partially ordered, just like little pieces of information: one is sometimes bigger than the other, etc
Of course this order is not total. So, he says, let us describe that partial order, call it P. P is INSIDE M, all of it. Cohen has the bricks, and he knows which brick fit others, to form some pieces of walls here and there, but not the full house, not  G. Why? because the glue which attach these pieces all together in a coherent way is not there. M does not know about the glue. Cohen is almost done: he steps out of the model, and bingo! there is plenty of glue.
If I add an ultrafilter, it will assemble consistently all the pieces of information, and I have my model. I do not need to explicitly describe it, it is enough to know that the glue is real (outside). Now we go back to the last insight of Cohen. How does he know that glueing all pieces along the ultrafilter  will not "mess things up"? Because, and the funny thing is M knows it, all information coming with G is already reached at some point of the glueing process, so it is available in  M.
Finale
What I just said about the set of fragments of information, is entirely codable in M. M knows everything, except the glue. It even knows the "forcing relation", in other words it knows that IF M[G]  exists, then truth in M[G] corresponds to some piece of information from within forcing it.
LAST NOTE One of my favorite books in Science Fiction was written by the set theorist converted to writer, Dr. Rudy Rucker. The book is called White Light, and is a big celebration of Cantorian Set Theory written by an insider. It just misses one pearl, the most glorious one: Forcing. Who knows, someone here, perhaps you, will write the sequel to White Light and show the splendor of Cohen's idea not only to "ordinary mathematicians" but to everybody...
ADDENDUM: SHELAH's LOGICAL DREAM (see commentary of Tim Chow)
Tim, you have no idea how many thoughts your  fantastic post has generated in my mind in the last 20 hours.  Shelah's dream can be made reality, but it ain't easy, though now at least I have some clue as to how to begin.
It is the "virus control method": suppose you take M and throw in some G
which is living in the truncated V cone where M lives. Add G. The very moment you add it, you are forced to  add all sets which are G-constructibles in  alpha steps, where alpha is any  ordinal in M. Now, let us say that the most lethal viral attack perpetrated by G is that one of these new sets is exactly alpha_0,
the first ordinal not in M, in other words G or its definable sets code a
well order of type alpha_0.
If one carries out the analysis I have just sketched, the conjecture would be that a G which does not cause any damage is a set which is as close as possible to be definable in M already,  in some sense to be made precise,but that goes along Cohen's intuition, namely that although G is not M-constructible, all its fragments  are.
If this plan can be implemented, it would show that forcing is indeed unique, unless.... unless some other crazy idea come into play
A: This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.
Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.
Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.
Let's assume we have a collection $M^P$ of terms for elements of $M[G]$. So for each good $G$, we will have a surjection $i_G : M^P\to M[G]$, interpreting the terms. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.
If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$ with $p\in G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.
Definability Hypothesis: for any formula $\varphi$, the class
$\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.
Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$,  then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.
Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)
Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.
One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.
Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.
A: I think there are a few things to unpack here.
1. What is the level of commitment from the reader?
Are we talking about a casual reader, say someone in number theory, who is just curious about forcing? Or are we talking about someone who is learning about forcing as a blackbox to use in some other mathematical arguments? Or are we talking about a fledgling set theorist who is learning about forcing so they can use it later?
The level of commitment from the reader dictates the clarity of the analogy, and the complexity of the details.

*

*To someone just wanting to learn about forcing, understanding what is "a model of set theory" and what are the basic ideas that genericity represent, along with the fact that the generic extension has some sort of a blueprint internal to ground model, are probably enough.


*To someone who needs to use forcing as a blackbox, understanding the forcing relation is probably slightly more important, but the specific construction of $\Bbb P$-names is perhaps not as important.


*Finally, to a set theorist, understanding the ideas behind $\Bbb P$-names is perhaps the biggest step in understanding forcing. From their conception, to their interactions with the ground model, and their interpretation.
These different levels would necessitate different analogies, or perhaps omitting the analogies completely in favour of examples.
2. Some recent personal experience
Just before lockdown hit the UK, I had to give a short talk about my recent work to a general audience of mathematicians, and I had to make the first part accessible to bachelor students. If you're studying some easily accessible problems, that's great. If your recent work was developing iterations of symmetric extensions and using that to obtain global failures of the axiom of choice from known local failures. Not as easy.
I realised when I was preparing for this, that there is an algebraic analogy to forcing. No, not the terrible "$\sqrt2$ is like a generic filter". Instead, if we consider subfields between $\Bbb Q$ and $\Bbb R$, to understand $\Bbb Q(\pi)$ we need to evaluate rational functions in $\Bbb Q(x)$ with $\pi$ in the real numbers.
When developing this analogy I was trying it out on some of the postdocs from representation theory, and two things became apparent:

*

*People in algebra very much resisted the idea that $\Bbb Q(\pi)$ is a subfield of $\Bbb R$. To then it was an abstract field, and it was in fact $\Bbb Q(x)$. It took some tweaking to the exposition to make sure that everyone is on board.


*The words "model of set theory" can kill the entire exposition, unless we explain what it is immediately after, or immediately before. Because the biggest problem with explaining forcing to non-experts is that people see set theory as "the mathematical universe", and when you're forcing you suddenly bring in new objects into the universe somehow. And even people who say that they don't think that way, it is sometimes apparent from their questions that they are kind of thinking that way.
There are still problems with the analogy, of course. It is only an analogy after all. For one, the theory of ordered fields is not a particularly strong theory—foundationally speaking—and so it cannot internalise everything (like the polynomials and their fraction field) inside the field itself, this is a sharp contrast to set theory. So what is a model of set theory? It's a set equipped with a binary relation which satisfy some axioms, just like a model of group theory is a set equipped with a binary operator which satisfy some axioms.
But now we can use the idea that every real number in $\Bbb Q(\pi)$ has a "name" of some rational function evaluated with $\pi$. It helps you understand why $\Bbb Q(e)$ and $\Bbb Q(\pi)$ are both possible generic extensions, even though they are very different (one contains $\pi$ and the other does not), and it helps you understand why $\Bbb Q(\pi)$ and $\Bbb Q(\pi+1)$ are both the same field, even though we used a different generic filter, because there is an automorphism moving one generic to the other.
Here is where we can switch to talk about genericity, give example of the binary tree, and what does it mean for a branch to be generic over a model, and how density plays a role.
So in this case, we did not go into the specifics. We only talked about the fact that there is a blueprint of the extension, which behaves a bit like $\Bbb Q(x)$, but because set theory is a more complicated theory, this blueprint is found inside the model rather than a "derivable object from our model".
3. What to do better?
Well, the above analogy was developed over a short period of time, and I will probably continue developing it in the next few years every time I explain someone what is forcing.
Where can we do better? Well, you want to talk about the forcing relation. But that's a tricky bit. My advisor, who is by all accounts a great expositor, had a story about telling some very good mathematician about forcing. Once he uttered "a formula in the language of forcing" the other party seemingly drifted off.
And to be absolutely fair, I too drift off when people talk to me about formulas in the language of forcing. I know the meaning of it, and I understand the importance of it, but just the phrase is as off-putting to the mind as "salted apples cores dinner".
I am certain that for the casual reader, this is unnecessary. We don't need to talk about the language of forcing. We simply need to explain that in a model some things are true and others are false. And the blueprint that we have of the model can determine some of that, but that the elements of the binary tree, or as they are called the conditions of the forcing, can tell us more information. They can give us more information on how the names inside the blueprint behave. Couple this with the opposite direction, that everything that happens in the generic extension, happens for a reason, and you got yourself the fundamental theorem of forcing. Without once mentioning formulas and the language of forcing, or even the forcing relation, in technical terms.
Yes, this is still lacking, and yes this is really just aimed at the casual reader. But it's a first step. It's a way to bring people into the fold, one step at a time. First you have an idea, then you start shaping it, and then you sand off the rough edges, oil, colour, and lacquer, and you've got yourself a cake.
