Forcing in other axiomatic systems [closed]

Question

What axioms do you need before you can use forcing? Does forcing use the axiom of infinity? Is there forcing in geometry as opposed to set theory?

Answer 1

Whoops, thought I was on MSE! I can't delete this now since the OP has accepted it, but I would like to acknowledge that this should be on MSE rather than here.

Actually to be honest I shouldn't have answered at all - the question is not suitable for any SE site in its current form - but this was what I happened to be thinking about at the moment, so I did so reflexively. And again, I can't delete since this has been accepted. I've made this CW to avoid rep gain.

---

"Forcing" is a rather vague term. In one sense it describes an incredibly broad idea which can be applied to almost any situation, while in another it is highly specific.

Here's the ultra-broad version. Suppose I have a structure X (= a set X equipped with some functions and relations). I can look, for example, at all possible expansions of X by a new unary predicate naming some subset of the underlying set; these expansions correspond to elements of the set P(X) (an expansion is determined by the value of its new predicate). Now the twist is that P(X) is nicely topologized via the product topology coming from the discrete topology on X; basically, a basic open set in P(X) corresponds to finitely many facts ("a_1,...,a_m are in U, b_1,...,b_k are not in U") about the new unary predicate U.

Assuming X is infinite to avoid trivialities, we can now ask which facts hold of "most" expansions: specifically, say that a sentence p in the language of X + the new predicate symbol U is generically true iff the subset of P(X) corresponding to the expansions satisfying p is comeager. Since the intersection of countably many comeager sets is comeager, and in particular nonempty, we get a well-behaved theory: the theory of generically true properties of expansions of X. And we can get variations on this idea by topologizing P(X) differently.

Now if our structure X happens to be a countable model of ZFC, things are particularly nice: for each poset A in X there will be a topology t_A on X and a t_A-comeager set C such that whenever U is a point in C, we can "convert" the expansion X(U) into a new model of set theory Y. Basically, we absorb the change-in-language via a change-in-structure. This isn't something which can be done in general - it's specifically permitted by the details of ZFC. That said, much less than ZFC is required; Adrian Mathias has written a lot about this, and generally advances the claim that the right minimal setting for forcing is provident set theory.