# Comptes Rendus
Mathématique

Rodrigo A. Freire

An axiomatic approach to forcing and generic extensions

Volume 358, issue 6 (2020), p. 757-775

Published online: 2 October 2020

https://doi.org/10.5802/crmath.97

<figure><img src="image_1.png" /></figure>

This article is licensed under the

CREATIVE COMMONS ATTRIBUTION 4.0 INTERNATIONAL LICENSE.

http://creativecommons.org/licenses/by/4.0/

<figure><img src="image_2.png" /></figure>
Logic / Logique

# An axiomatic approach to forcing and generic extensions

Une approche axiomatique du forcing et des extensions génériques

Rodrigo A. Freire<sup>a</sup>

<sup>a</sup> Department of Philosophy, University of Brasília, Brasil

E-mail: rodrigofreire@unb.br

**Abstract.** This paper provides a conceptual analysis of forcing and generic extensions. Our goal is to give general axioms for the concept of standard forcing-generic extension and to show that the usual (poset) constructions are unified and explained as realizations of this concept. According to our approach, the basic idea behind forcing and generic extensions is that the latter are uniform adjunctions which are ground-controlled by forcing, and forcing is nothing more than that ground-control. As a result of our axiomatization of this idea, the usual definitions of forcing and genericity are derived.

**Résumé.** Cet article présente une analyse conceptuelle du forcing et des extensions génériques. Notre objectif est de donner des axiomes généraux pour le concept d'extension forcing-générique standard, et de montrer que les constructions habituelles sont unifiées et expliquées comme étant des réalisations de ce concept. Selon notre approche, l'idée-clé sous-tendant le forcing et les extensions génériques est que ces dernières sont des adjonctions uniformes qui sont contrôlées par le forcing, ainsi le forcing n'est rien de plus que ce contrôle. Comme conséquence de notre axiomatisation de cette idée, on dérive les définitions habituelles du forcing et de la généricité.

**Funding.** This research was partially supported by fapesp, proccess 2016/25891-3.

Manuscript received 10th April 2020, revised and accepted 17th July 2020.

## 1. Preliminary Remarks

Forcing and generic extensions are usually not given as realizations of a concept, rather they are presented as specific constructions serving a specific purpose. Indeed, there are many different constructions with the same effect and differing on technical minutiae which obfuscate its essential components. If we want to make explicit what is this specific purpose, we must first capture the general idea avoiding inessential variations. In order to accomplish that, we turn towards an axiomatic approach. The situation is analogous to that of the real number system up to isomorphism: There are many different constructions of this system, but the axiomatic
approach gives us a concept behind those constructions. We wish to capture a conceptual basis for forcing and generic extensions.

Our aim is to characterize forcing and generic extensions through properties (axioms) that are common to all explicit constructions of forcing predicates and generic extensions. For example, textbook definitions of forcing relation in the ground model (which is customarily denoted by $|\vdash^*$), generic filter, $\mathbb{P}$-name and evaluation of a $\mathbb{P}$-name may vary widely, but there are common properties shared by the whole variety of constructions of forcing and generic extensions. The truth lemma and the definability lemma, for instance, hold in all constructions, independently of one's choice of basic definitions. It is important to keep in mind the analogous case of the axiomatization of the real number system. Traditional constructions of real numbers and their operations from rational numbers may vary widely, but all given constructions satisfy the characterizing axioms of complete ordered fields. We wish to achieve the same thing with our axiomatization of forcing and generic extensions.

However, axioms are not chosen at random. We need a guiding idea, which can be roughly explained as follows. First of all, our strategy is to understand forcing and genericity as the main components of a single concept, the concept of forcing-generic extension. Then, to understand that a forcing-generic extension of a transitive model $M$ given by a generic filter $G$ is a uniform adjunction of $G$ to $M$ which is controlled from the ground by forcing. The notion of being ground-controlled by forcing is made precise by the fundamental duality:

$$M \models p \Vdash \phi \iff \forall G \exists p; M[G] \models \phi$$

and

$$M[G] \models \phi \iff \exists p \in G; M \models p \Vdash \phi.$$

It may be helpful to think about the above duality in informal terms, considering the slogan "generic extensions are those which are controlled from the ground by forcing, and forcing is the ground control of generic extensions". According to our abstract account, the association of forcing and genericity is not accidental, and the conceptual core of this subject is this undissociated forcing-generic compound.

The development of the axiomatic approach to forcing and generic extensions presented here parallels the exposition of the subject given in the classic paper *Unramified Forcing*, by Joseph Shoenfield. However, our approach is very different. Indeed, we have, in some sense, reversed the traditional approach: Axioms constitute our point of departure, and the traditional definitions of generic filters and forcing predicates in the ground model are derived from them. Most of our axioms can be found as relevant theorems in all variations of the traditional approach, such as the truth lemma, the definability lemma, the generic existence theorem, etc, and we shall briefly recall how they are proved in that approach along the way. Furthermore, Section 9 provides a construction of a standard forcing-generic extension, followed by a verification that the axioms hold in that construction, which amounts to an exposition of all those relevant theorems. Nevertheless, our axioms *qua* axioms are not proved in our approach.

The moral of our work is that if we want the fundamental duality (axioms (7) and (8)), the uniform adjunction of $G$ to $M$ (axioms (5) and (6)), the generic existence (axiom (4)), and the basic properties of our control apparatus (axioms (1), (2) and (3)), then forcing and genericity must be defined in the usual way. If we also adopt the universality of $\mathbb{P}$-membership (axiom (9)), then we achieve a categoricity result. Subsequently, a construction of the standard forcing-generic extension uniquely determined by the ground model and the generic filter is accomplished as a natural outcome of our development. We should prove all that, but first we must provide a framework in which the axioms can be stated. All axioms are common to all variations of the traditional approach and can be explained in simple terms, thus showing that the whole
subject rests on a very general idea, instead of being a cluster of particular, ad hoc technical
constructions.

## 2. The Notion of Forcing-Generic Framework

Assume that we are given the following basic data: A transitive model $M$, the elements of which are called individuals and denoted by $a, b, c$ and $d$, and an absolute partial order $\mathbb{P}$ with greatest element 1. The domain of $\mathbb{P}$ is an individual of $M$ and its elements, called conditions, are denoted by $p, q, r, s$ and $t$. The absolute order relation is denoted by $\le$. If $p \le q$, we say that $p$ is a condition stronger than $q$. Individuals can be used as parameters in formulas.

**Remark 1.** We deal with the usual caveat about transitive models in the way Azriel Levy did in [3], which means that we work in a conservative extension of ZFC given by an additional constant $M$, an axiom saying that $M$ is transitive and an axiom schema saying that it reflects every sentence of the original language. The role of the *set* model $M$ is to allow generic filters, but this is not strictly necessary. Since the generic extension must be controlled from the ground, we could stay in the ground and dispense the extension as a fiction. Accordingly, we could do forcing over $V$, in which

(i) a choice of correct conditions is given by a unary predicate symbol satisfying some axioms (see [4, p. 282]) and

(ii) the statements forced from V interpret statements about a fictitious generic extension (see [4, p. 285]).

In addition to our basic data, we need the control apparatus. We need to control membership in $M[G]$ from the ground $M$. In order to accomplish that, $M[G]$ must be obtained as the transitive collapse of a binary relation in $M$, so that we can pull-back membership in $M[G]$ to a relation in $M$. This relation, given by the additional data explained in the next paragraph, is denoted by $∃p∈G; M|=a∈_p b$, and it means that the collapsed $a$ is an element of the collapsed $b$ according to a correct condition.

Therefore, we need a ternary relation $R$ in $M$ which we require to be definable and absolute for transitive models. This relation is called the $\mathbb{P}$-membership relation and its satisfaction by the triple $(p, a, b)$ is represented by $M|=a \in_p b$. Roughly, this is a "membership according to $p$" relation, and it is the first step towards a control apparatus. However, since the corresponding collapse fails to be injective, we shall adjust our membership control through the forcing predicates.

As we have just mentioned, the control apparatus needs to be refined and completed, which gives rise to the forcing predicates. They are intended to be the ultimate control apparatus, given as follows. For each formula $\phi$ with $n$ free variables, a definable $n+1$-ary predicate $\|\phi$ in $M$ called the forcing predicate corresponding to $\phi$. The satisfaction of the predicate $\|\phi$ by the condition $p$ and the $n$-tuple of individuals $\bar{a}$ is represented by $M|=(p\|\phi)[\bar{a}]$. These predicates constitute the ultimate control of $M[G]$. If $p$ is a correct condition, that is one which is in $G$, and $M|=(p\|\phi)[\bar{a}]$, then the formula $\phi$ is satisfied by the corresponding sequence of elements in $M[G]$.

The final ingredient of our framework is the genericity property C. We think of a set satisfying C as a subset of $\mathbb{P}$ embodying a choice of conditions which are then considered to be correct. These sets are required to be filters of $\mathbb{P}$ which are called generic and denoted by $G$ and $H$. Why are sets determined by conditions which are subsequently considered to be correct required to form filters? Because

(i) if $p$ is considered to be a correct condition and $q$ is weaker than $p$, then $q$ must be considered correct since it is "contained in $p$", and

(ii) if $p$ and $q$ are considered to be correct conditions, then they must be considered compatibly correct, that is, there must be condition $r$ considered to be correct and "encompass passing both $p$ and $q"".
The weakest condition 1 is always considered to be correct.

Our axioms can now be stated. We say that the above data constitute a forcing-generic framework if the axioms (1)–(8) below are satisfied. The first two are called the downward closedness axioms of our control apparatus. Basically, they say that a stronger condition exerts at least the same control as a weaker condition. In the traditional approach, the first three axioms are immediate consequences of the corresponding definitions.

(1) Given a formula $\phi$, for all $\bar{a}$, $p$ and $q$, if $M \models (p \Vdash \phi)[\bar{a}]$ and $q \le p$, then $M \models (q \Vdash \phi)[\bar{a}]$.

(2) For all $p$, $q$, $a$ and $b$, if $M \models a \in_p b$ and $q \le p$, then $M \models a \in_q b$.

(3) 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,

$$ \{a : \exists p; M \models a \in_p b\} $$

is a set in $M$.

(4) For each $p \in \mathbb{P}$, there is a generic filter $G$ containing $p$ as an element.

The fourth property above informally says that no condition in $\mathbb{P}$ is a priori incorrect. We call it the generic existence axiom. This axiom is an important theorem in the traditional approach, in which it is proved under the countability assumption on $M$. In fact, one just enumerates $M$ and defines $G$ to be the filter generated by conditions inductively selected as follows: $p_0 = p$, and $p_{n+1}$ is any condition stronger than $p_n$ which is an element of $a_n$ if such a condition exists; otherwise, $p_{n+1} = p_n$. The well-foundedness axiom is required because, in order to be controlled, $M[G]$ is obtained as the transitive collapse of the binary relation represented by $\exists p \in G; M \models a \in_p b$, and such a collapse is defined for well-founded relations only.

Before giving the remaining axioms, it is convenient to establish some notation. Let $\in_G$ denote the well-founded relation between individuals $a$ and $b$ given by $\exists p \in G; M \models a \in_p b$. For each generic filter $G$ we can define the transitive collapse $F_G$ of the well-founded relation $\in_G$ as usual. Let $F$ denote the function which associates $F_G$ with $G$, and let $M[G]$ denote the range of $F_G$, that is, $F_G[M]$. If $\bar{a}$ is an $n$-tuple, then $F_G(\bar{a})$ denotes the $n$-tuple obtained from $\bar{a}$ by the pointwise application of $F_G$. We remark that elements of $M[G]$ can be used as parameters in formulas.

We say that $F$ is a forcing-generic evaluation map if it satisfies the canonical naming axioms below and the fundamental duality.

(5) $\forall a \in M; \exists b \in M; \forall G; F_G(b) = a$.

(6) $\exists c \in M; \forall G; F_G(c) = G$.

The above axioms guarantee the extension of $M$ through the adjunction of $G$, and it is important to notice the uniformity in them. These existential conditions are obtained by the canonical names in the usual constructions of generic extensions. $F_G(a)$ is said to be the $G$-value of $a$. Accordingly, the fundamental duality can be stated:

(7) $M[G] \models \phi[F_G(\bar{a})]$ iff $\exists p \in G; M \models (p \Vdash \phi)[\bar{a}]$, for all $\phi, \bar{a}, G$.

(8) $M \models (p \Vdash \phi)[\bar{a}]$ iff $\forall G \exists p; M[G] \models \phi[F_G(\bar{a})]$, for all $\phi, \bar{a}, p$.

The above equivalences constitute the fundamental duality of genericity and forcing, and show how these concepts are tied together. It is time to recall our slogan: “Generic extensions are those which are controlled from the ground by forcing, and forcing is the ground control of generic extensions”. That is the informal reading of the fundamental duality. Axioms (7) and (8) collectively correspond to the truth lemma and the definability lemma in the traditional approach.
### 3. The Notion of Forcing-Generic Extension

We can proceed to the definition of the forcing-generic extension concept. In Section 7 the concept of standard forcing-generic extension is defined, which requires an additional axiom and is categorical in the appropriate sense.

A forcing-generic extension is represented by a forcing-generic framework endowed with a generic filter. The forcing-generic extension represented by $(M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G)$ is identified with the direct image of $M$ through the associated collapse $F_G$, and it is said to represent a forcing-generic extension of $M$ given by the generic filter $G$.

That is, a forcing-generic extension is an equivalence class of the form $[(M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G)]$. The appropriate equivalence relation between an unprimed sextuple and a primed one is given by the equality $F_G[M] = F'_{G'}[M']$.

The role of $F$ is important:

$$(M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G) \quad \text{and} \quad (M, \mathbb{P}', R', \{\Vdash' \phi : \phi \in L(\epsilon)\}, C', G)$$

represent the same forcing-generic extension if and only if $F_G[M] = F'_{G'}[M]$. For the time being, the notation $M[G]$ is ambiguous. In Section 6 we shall prove that if these sextuples satisfy axioms (1)–(9), then $F_G[M] = F'_{G'}[M]$.

In summary, we say that a ground model $M$, a partial order $\mathbb{P}$, a $\mathbb{P}$-membership relation, a collection of forcing predicates for the formulas $\phi$ in the language of set theory, a genericity predicate and a generic filter $G$ represent a forcing-generic extension if and only if they satisfy the downward closedness axioms, the well-foundedness axiom, the generic existence axiom, the canonical naming axioms and the fundamental duality. That is all. Notice that we have not given ostensive constructions for the ingredients of a forcing-generic extension. For example, we have not said what formulas define the $\mathbb{P}$-membership and the forcing predicates, nor have we said that generic filters are those intersecting the dense sets in $M$.

### 4. Forcing a Negation and Intersecting Dense Sets

From the given axiomatization of the forcing-generic extension concept, we can recover usual defining clauses of forcing predicates, as they are given in the traditional approach. This section and the next one are dedicated to this task, which is central in our approach. It is interesting to compare the clauses derived here with those found in [2], for example. We start with the forcing of a negation.

* $M \models (p \Vdash \neg \phi)[\bar{a}] \text{ iff}$

* $\forall G \ni p; M[G] \models \neg \phi[F_G(\bar{a})] \text{ iff}$

* $\forall G \ni p; M[G] \not\models \phi[F_G(\bar{a})] \text{ iff}$

* $\forall G \ni p; \neg \exists q \in G; M \models (q \Vdash \phi)[\bar{a}] \text{ iff}$

* $\forall G \ni p; \forall q \in G; M \not\models (q \Vdash \phi)[\bar{a}] \text{ iff}$

* $\forall G \ni p; \forall q \in G; M \models (q \Vdash \phi)[\bar{a}] \text{ iff}$

* $\forall q \le p; M \models (q \Vdash \phi)[\bar{a}] \text{ iff}$

* $M \models \forall q \le p; (q \Vdash \phi)[\bar{a}]$.

Let us prove the next to last equivalence above, through which quantification over generic filters can be eliminated. Assume that

$$\forall G \ni p; \forall q \in G; M \models (q \Vdash \phi)[\bar{a}]$$

Let $q$ be a condition stronger than $p$. From the generic existence axiom, there is a generic filter $G$ containing $q$. Since $G$ is a filter, $p \in G$. From our premise, $M \models (q \Vdash \phi)[\bar{a}]$, as desired. Conversely, assume that

$$\forall q \le p; M \models (q \Vdash \phi)[\bar{a}]$$
Let $G$ be a generic filter containing $p$ and assume, contrary to the desired conclusion, that there is an $r \in G$ such that $M \models (r \Vdash \phi)[\bar{a}]$. Since $G$ is a filter, there is a condition $q \in G$ such that $q \le p, r$. From the downward closedness axiom (1), we would have that $M \models (q \Vdash \phi)[\bar{a}]$, which is a contradiction with our premise.

There is an important consequence of the law of excluded-middle applied to $M[G]$ for gener-
icity. Since $M[G] \models \phi[F_G(\bar{a})]$ or $M[G] \models \neg\phi[F_G(\bar{a})]$, it follows that $\exists p \in G; M \models (p \Vdash \phi)[\bar{a}]$ or $\exists p \in G; M \models (p \Vdash \neg\phi)[\bar{a}]$. Therefore,

$$
\exists p \in G; M \models (p \Vdash \phi \lor \forall q \le p; q \Vdash \phi)[\bar{a}],
$$

which means that $G$ intersects sets in $M$ of the form

$$
\{p : M \models (p \Vdash \phi \lor \forall q \le p; q \Vdash \phi)[\bar{a}]\}.
$$

These sets have the property of being dense. In fact, we can show that generic filters intersect all
dense sets in M as follows.

**Lemma 2.** Let $D \subseteq \mathbb{P}$ be a dense set in $M$, that is, $D$ is an individual in $M$ and for all $p \in \mathbb{P}$ there is $a \ q \le p$ such that $q \in D$. Every generic filter intersects $D$.

**Proof.** Let $a$ be such that for every generic filter $G$ we have $F_G(a) = D$, and let $c$ be such that for every generic filter $G$ we have $F_G(c) = G$. Let $H$ be a generic filter. Assume that $D \cap H = \emptyset$.

If $D \cap H = \emptyset$, then $M[H] \models \neg \exists x; (x \in F_G(a) \cap F_G(c))$. So,

$$
\exists p \in H; M \models (p \Vdash \neg \exists x; (x \in a \cap c)).
$$

Fix such a $p \in H$. We have that

$$
M \models (\forall q \le p; q \Vdash \exists x; (x \in a \cap c)).
$$

Since *D* is dense, there is a *q* ≤ *p* such that *q* ∈ *D*. Fix such a *q*.

Now, $q \in D$ and if $b$ is such that $q = F_G(b)$ for every generic filter $G$, then $\forall G \ni q; M[G] \models F_G(b) \in F_G(a) \cap F_G(c)$. Therefore,

$$
\forall G \ni q; M[G] \models (\exists x; x \in F_G(a) \cap F_G(c))
$$

and $M \models (q \Vdash \exists x; x \in a \cap c)$, a contradiction.

<figure><img src="image_3.png" /></figure>

These results can be used to eliminate quantification over generic filters, which, in turn, can
be used to recover the usual defining clauses for forcing predicates.

**Lemma 3.** For every downward closed $A \subseteq \mathbb{P}$ which is in $M$,

$$
\forall G \ni p; \exists q \in G; q \in A \quad \text{iff} \quad \forall r \le p; \exists q \le r; q \in A.
$$

**Proof.** The important notion of incompatibility is applied in the proof of this equivalence. Two conditions are said to be incompatible if there is no condition which is simultaneously below them.

On the one hand, assume that $\forall G \ni p; \exists q \in G; q \in A$. We know that for every $r \le p$ there is a generic $G \ni r$. If $r \in G$, then $p \in G$ and, from the assumption, there is an $s \in G$ such that $s \in A$. Since $A$ is downward closed and $G$ is a filter, there is a $q \le r, s$ in $G$ such that $q \in A$.

On the other hand, let $G \ni p$ be a generic filter and $D$ be the set of all conditions which are either in $A$ or are incompatible with $p$. If

$$
\forall r \le p; \exists q \le r; q \in A,
$$

then $D$ is dense and $G \cap D \neq \emptyset$. Moreover, if $s \in G$, then $s$ is compatible with $p$. Therefore, $G \cap A \neq \emptyset$, which completes the proof of the equivalence.
$\square$

<figure><img src="image_4.png" /></figure>
**5. The Inductive Forcing Definition Recovered**

Along with the usual defining clause of forcing a negation from our axioms, given in the preceding section, we have obtained a very important consequence for genericity. Let us return to the task of recovering defining clauses of forcing predicates, forcing a disjunction being the simplest case.

* $M \models (p \Vdash \phi \lor \psi)[\bar{a}]$ iff

* $\forall G \exists p; M[G] \models \phi \lor \psi[F_G(\bar{a})]$ iff

* $\forall G \exists p; (M[G] \models \phi[F_G(\bar{a})] \lor M[G] \models \psi[F_G(\bar{a})])$ iff

* $\forall G \exists p; ((\exists q \in G; M \models (q \Vdash \phi)[\bar{a}]) \lor (\exists q \in G; M \models (q \Vdash \psi)[\bar{a}]))$ iff

* $\forall G \exists p; \exists q \in G; (M \models (q \Vdash \phi)[\bar{a}] \lor M \models (q \Vdash \psi)[\bar{a}])$ iff

* $\forall G \exists p; \exists q \in G; M \models (q \Vdash \phi \lor q \Vdash \psi)[\bar{a}]$ iff

* $\forall r \le p; \exists q \le r; M \models (q \Vdash \phi \lor q \Vdash \psi)[\bar{a}]$ iff

* $M \models \forall r \le p; \exists q \le r; (q \Vdash \phi \lor q \Vdash \psi)[\bar{a}]$.

It is also easy to recover the usual clause of forcing an existential.

* $M \models (p \Vdash \exists x; \phi)[\bar{a}]$ iff

* $\forall G \exists p; M[G] \models \exists x; \phi[F_G(\bar{a})]$ iff

* $\forall G \exists p; \exists a \in M; M[G] \models \phi[F_G(\bar{a}, a)]$ iff

* $\forall G \exists p; \exists a \in M; \exists q \in G; M \models (q \Vdash \phi)[\bar{a}, a]$ iff

* $\forall G \exists p; \exists q \in G; \exists a \in M; M \models (q \Vdash \phi)[\bar{a}, a]$ iff

* $\forall G \exists p; \exists q \in G; M \models \exists x; (q \Vdash \phi)[\bar{a}]$ iff

* $\forall r \le p; \exists q \le r; M \models \exists x; (q \Vdash \phi)[\bar{a}]$ iff

* $M \models \forall r \le p; \exists q \le r; \exists x; (q \Vdash \phi)[\bar{a}]$.

**Remark 4.** The double-negation applied to $M[G]$ has an important consequence for forcing:

* $M \models (p \Vdash \phi)[\bar{a}]$ iff

* $M \models (p \Vdash \neg \neg \phi)[\bar{a}]$ iff

* $M \models (\forall q \le p; q \Vdash \neg \neg \phi)[\bar{a}]$ iff

* $M \models (\forall q \le p; \exists r \le q; r \Vdash \phi)[\bar{a}]$.

This remark is useful to derive the clause of forcing a conjunction.

* $M \models (p \Vdash \phi \land \psi)[\bar{a}]$ iff

* $M \models (p \Vdash \neg (\neg \phi \lor \neg \psi))[\bar{a}]$ iff

* $M \models \forall q \le p; (q \Vdash \neg \neg \phi \lor \neg \neg \psi)[\bar{a}]$ iff

* $M \models \forall q \le p; \neg (q \Vdash \neg \neg \phi \lor \neg \neg \psi)[\bar{a}]$ iff

* $M \models \forall q \le p; \neg (\forall r \le q; \exists s \le r; (s \Vdash \neg \neg \phi \lor s \Vdash \neg \neg \psi))[\bar{a}]$ iff

* $M \models \forall q \le p; \exists r \le q; \forall s \le r; \neg (\forall t \le s; t \Vdash \phi \lor \forall t \le s; t \Vdash \psi)[\bar{a}]$ iff

* $M \models \forall q \le p; \exists r \le q; \forall s \le r; (\exists t \le s; t \Vdash \phi \land \exists t \le s; t \Vdash \psi)[\bar{a}]$ iff

* $M \models \forall q \le p; \exists r \le q; (\forall s \le r; \exists t \le s; t \Vdash \phi \land \forall s \le r; \exists t \le s; t \Vdash \psi)[\bar{a}]$ iff

* $M \models \forall q \le p; \exists r \le q; (r \Vdash \phi \land r \Vdash \psi)[\bar{a}]$ iff

* $M \models (p \Vdash \phi \land p \Vdash \psi)[\bar{a}]$.

Among the above equivalences, only the last one is nontrivial. The last clause implies the next to last clause using the downward closedness of forcing. Conversely, the next to last clause implies that

$$M \models (\forall q \le p; \exists r \le q; r \Vdash \phi \land \forall q \le p; \exists r \le q; r \Vdash \psi)[\bar{a}],$$

which, from Remark 4 is equivalent to the last clause

Let us proceed to the atomic cases, membership and equality. Recall that, since the transitive collapse which generates $M[G]$ is not injective, we must adjust our control of membership in $M[G]$. The adjusted control is made explicit by the clause of forcing a membership. The more delicate case of forcing an equality is taken care next.
• $M \models (p \Vdash a \in b)$ iff

• $\forall G \exists p; F_G(a) \in F_G(b)$ iff

• $\forall G \exists p; \exists c \in M; (F_G(a) = F_G(c) \land (\exists q \in G; M \models c \in_q b))$ iff

• $\forall G \exists p; \exists c \in M; (\exists r \in G; M \models r \Vdash a = c) \land (\exists q \in G; M \models c \in_q b)$ iff

• $\forall G \exists p; \exists q \in G; \exists r \in G; \exists c \in M; (M \models r \Vdash a = c) \land (M \models c \in_q b)$ iff

• $\forall G \exists p; \exists s \in G; \exists c \in M; M \models (s \Vdash a = c) \land M \models (c \in_s b)$ iff

• $\forall r \le p; \exists s \le r; \exists c \in M; M \models (c \in_s b \land s \Vdash a = c)$ iff

• $M \models \forall r \le p; \exists s \le r; \exists x; (x \in_s b \land s \Vdash a = x)$.

In order to derive the clauses for all forcing predicates, it is easier to deal primarily with the inequality, rather than equality. This can be explained by the distributivity and commutativity laws for the logical operations. Commutativity holds between two quantifiers of the same type, and distributivity holds between the pairs existential quantifier and disjunction and universal quantifier and conjunction. Using extensionality, inequality has the suitable logical form, whereas equality has not. Fortunately, we can obtain the forcing of an equality from that of an inequality.

• $M \models (p \Vdash a = b)$ iff

• $M \models (p \Vdash \neg a \neq b)$ iff

• $M \models (\forall q \le p; q \Vdash a \neq b)$.

Using the double-negation law, we can see the coherence of the forcing relations for equality and inequality.

• $M \models (p \Vdash \neg a = b)$ iff

• $M \models (\forall q \le p; q \Vdash a = b)$ iff

• $M \models (\forall q \le p; \exists r \le q; r \Vdash a \neq b)$ iff

• $M \models (p \Vdash a \neq b)$.

The clause of forcing an inequality can be recovered.

• $M \models (p \Vdash a \neq b)$ iff

• $\forall G \exists p; (F_G(a) \neq F_G(b))$ iff

• $\forall G \exists p; \exists c \in M; (F_G(c) \in F_G(a) \setminus F_G(b)) \lor (F_G(c) \in F_G(b) \setminus F_G(a))$ iff
(from axiom (7) with the formula $x \in y \setminus z$)

• $\forall G \exists p; \exists c \in M; \exists q \in G; M \models (q \Vdash c \in a \setminus b) \lor \exists q \in G; M \models (q \Vdash c \in b \setminus a)$ iff

• $\forall G \exists p; \exists q \in G; \exists c \in M; M \models (q \Vdash c \in a \setminus b) \lor M \models (q \Vdash c \in b \setminus a)$ iff

• $\forall r \le p; \exists q \le r; \exists c \in M; M \models (q \Vdash c \in a \setminus b) \lor M \models (q \Vdash c \in b \setminus a)$.

Now, the analysis of $M \models (q \Vdash c \in a \setminus b)$ requires some attention. This is not a case of forcing a membership. In fact, $x \in y \setminus z$ is an abbreviation of the complex formula $x \in y \land x \notin z$. If we use the clause of forcing a conjunction, we get that $M \models (q \Vdash c \in a \land c \notin b)$ is equivalent to

$$M \models (q \Vdash c \in a) \land (q \Vdash c \notin b).$$

If we replace $M \models (q \Vdash c \in a \setminus b)$ by the above clause in

$$\forall r \le p; \exists q \le r; \exists c \in M; M \models (q \Vdash c \in a \setminus b) \lor M \models (q \Vdash c \in b \setminus a),$$

replace $M \models (q \Vdash c \in b \setminus a)$ similarly, we obtain the following clause:

$$\forall r \le p; \exists q \le r; \exists c \in M; (M \models (q \Vdash c \in a) \land (q \Vdash c \notin b)) \lor (M \models (q \Vdash c \in b) \land (q \Vdash c \notin a)).$$

This must be further simplified in order to show that a definition for the atomic cases could be accomplished by transfinite induction, as usual. We begin by using the clause of forcing a membership we have obtained.

• $\forall r \le p; \exists q \le r; \exists c \in M; (M \models (q \Vdash c \in a) \land (q \Vdash c \notin b)) \lor (M \models (q \Vdash c \in b) \land (q \Vdash c \notin a))$ iff
• $\forall r \le p; \exists q \le r; \exists c \in M; (\forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t a \wedge t \models c = d) \wedge (q \models c \notin b)) \lor (\forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t b \wedge t \models c = d) \wedge (q \models c \notin a)) \text{ iff}$

• $\forall r \le p; \exists q \le r; \exists c \in M; (M \models (c \in q a \wedge q \models c \notin b) \lor (M \models (c \in q b \wedge q \models c \notin a}))$

The equivalence between the last and the next to last clauses requires a proof. First, the last clause easily implies the next to last one. For, if $M \models (c \in q a \wedge q \models c \notin b)$, then

$$ \forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t a \wedge t \models c = d) \wedge (q \models c \notin b), $$

and, symmetrically, $M \models (c \in q b \wedge q \models c \notin a)$ implies

$$ \forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t b \wedge t \models c = d) \wedge (q \models c \notin a). $$

Indeed, it is enough to show that $M \models (c \in q a)$ implies

$$ \forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t a \wedge t \models c = d). $$

Given $s \le q$, just take $t \le s$ to be $s$ itself, and $d \in M$ to be $c$ itself. It follows that

$$ M \models (d \in t a \wedge t \models c = d). $$

In fact, from $M \models (c \in q a)$, $d = c$ and $t = s \le q$, it follows that $M \models (d \in t a)$ and $M \models (t \models c = d)$, because $\mathbb{P}$-membership is downward closed and $c = d$ implies $F_G(c) = F_G(d)$, for any $G$.

It remains to prove that the next to last clause implies the last one above. Assume that $r \le p$ is given. From the hypothesis, there are $q \le r$ and $c \in M$ such that

$$ (\forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t a \wedge t \models c = d) \wedge (q \models c \notin b)) \lor (\forall s \le q; \exists t \le s; \exists d \in M; M \models (d \in t b \wedge t \models c = d) \wedge (q \models c \notin a)). $$

Assume, without loss of generality, that the first disjunct is true. Take $s \le q$ to be $q$ itself. There are $t \le q$ and $d \in M$, such that

$$ M \models (d \in t a \wedge t \models c = d) \wedge (q \models c \notin b). $$

So, from the downward closedness of forcing, there are $t \le r$ and $d \in M$ such that

$$ M \models (d \in t a) \wedge (t \models c = d) \wedge (t \models c \notin b). $$

However, from axiom (8), if $M \models (t \models c = d) \wedge (t \models c \notin b)$, then

$$ M \models (t \models d \notin b). $$

Therefore, $M \models (d \in t a) \wedge (t \models d \notin b)$, and we conclude that

$$ \forall r \le p; \exists t \le r; \exists d \in M ; M \models (d \in t a) \wedge (t \models d \notin b). $$

Renaming the quantified variables,

$$ \forall r \le p; \exists q \le r; \exists c \in M; M \models (c \in q a \wedge q \models c \notin b). $$

Since $M \models (c \in q a \wedge q \models c \notin b)$ implies

$$ M \models (c \in q a \wedge q \models c \notin b) \lor M \models (c \in q b \wedge q \models c \notin a), $$

it follows that

$$ \forall r \le p; \exists q \le r; \exists c \in M; M \models (c \in q a \wedge q \models c \notin b) \lor M \models (c \in q b \wedge q \models c \notin a), $$

and this concludes the proof.

Putting everything together, we have that

• $M \models (p \models a \neq b)$ iff

• $M \models \forall r \le p; \exists q \le r; \exists x; ((x \in q a \wedge q \models x \notin b) \lor (x \in q b \wedge q \models x \notin a)).$
A definition for all forcing predicates, by induction on the complexity of the formula, could be easily given from the clauses we have obtained. The only issue is that there seems to be a circularity in the atomic cases: The clause of forcing a membership involves forcing an equality; the clause of forcing an equality is given in terms of forcing an inequality; the clause of forcing an inequality involves forcing negations of membership relations. This circularity is only apparent and can be dealt with a transfinite inductive definition, granted by axiom (3).

Indeed, let $\rho$ be the rank with respect to the relation $\exists t; M \models a \in_t b$, which, from axiom (3), is well-founded and well-founded in $M$. The ordinal function $\rho$ is defined by

$$ \rho(b) = \sup^{+} \{\rho(a) : \exists t; M \models a \in_t b\}, $$

in which $\sup^+$ denotes the least strict upper bound. Since $\exists t; M \models a \in_t b$ is well-founded in $M$ and absolute for $M$, we have $\rho^M$ defined in $M$ and $\rho^M = \rho$. The sequences of equivalences for the cases of forcing atomic formulas just derived are given to lower the value of $\rho$ as we move from forcing $a \neq b$ to forcing $c \notin b$ or $c \notin a$, then to forcing $c \neq d$, thus avoiding circularity.

In fact, following our derivations, as we move from forcing $a \neq b$ to forcing $c \notin b$ or $c \notin a$, we have that $c$ is a $\mathbb{P}$-member of $a$ or of $b$, according to a condition $q$. Then, plugging the clauses of forcing $c \notin b$ and $c \notin a$ into the clause of forcing $a \neq b$ results in a clause involving forcing $c \neq d$, in which $d$ is a $\mathbb{P}$-member of $b$ or a $\mathbb{P}$-member of $a$, according to $s$. The point is that the value of $\rho$ has been lowered as we move from $a$ and $b$ to $c$ and $d$, enabling the transfinite inductive definition. More precisely, $M \models (p \Vdash a \neq b)$ could be defined in terms of $M \models (q \Vdash c \neq d)$, in which $\exists t; M \models c \in_t a$ and $\exists t; M \models d \in_t b$, or $\exists t; M \models c \in_t b$ and $\exists t; M \models d \in_t a$. In any case, the maximum of $\rho(c)$ and $\rho(d)$ is strictly less than the maximum of $\rho(a)$ and $\rho(b)$.

Therefore, the maximum of the corresponding values of $\rho$ is strictly decreasing, and our clauses could be used to define $M \models (p \Vdash a \neq b)$ as a predicate of $(p, a, b)$ by transfinite induction. That is, we could define $M \models (p \Vdash a \neq b)$ as a predicate of $(p, a, b)$, assuming inductively that $M \models (q \Vdash c \neq d)$ has been defined whenever

$$ \max(\rho(c), \rho(d)) < \max(\rho(a), \rho(b)). $$

Since $\max(\rho(c), \rho(d)) < \max(\rho(a), \rho(b))$ defines a relation between triples $(q, c, d)$ and $(p, a, b)$ which is well-founded in $M$, that would be a legitimate transfinite inductive definition within $M$.

Although, in our axiomatic approach, forcing predicates are not defined and we have only proved that they must behave as expected, all the important features of the definitions given in the traditional approach are unveiled by our derivations from the axioms. Furthermore, details involved in those definitions are provided in Section 9, in which the existence of a standard generic extension is proved, finally showing an extensional equivalence between the traditional approach and our axiomatic approach.

# 6. The Categoricity of the Axiomatization

Assume that $M[G]$ is a model of $ZF$. (We shall prove that under a suitable additional axiom on $\mathbb{P}$-membership which is given in Section 7). If $N$ is a model containing $M$ and $G$, then $F_G$ is absolute for $N$. Thus, for every $a \in M$, we have $F_G(a) = F_G^N(a)$. Since $F_G^N(a) \in N$, it follows that $M[G] \subseteq N$. We conclude that $M[G]$ is the least model containing $M$ and $G$.

Therefore, if the sextuples

$$ (M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G) \quad \text{and} \quad (M, \mathbb{P}', R', \{\Vdash' \phi : \phi \in L(\epsilon)\}, C', G) $$

satisfy axioms (1)–(8) and the additional axiom (9) below, then

$$ F_G[M] = F'_G[M], $$
implying that these sextuples represent the same forcing-generic extension unambiguously denoted by $M[G]$. This is the categoricity result we were searching for.

## 7. Standard Forcing-Generic Extensions

We have not yet proved that $M[G]$ is a model of ZF, and we shall use an extra axiom to do that, an axiom on $\mathbb{P}$-membership. Indeed, some special properties of the traditional constructions of $\mathbb{P}$-membership are used in the usual proof that $M[G]$ satisfies the axioms. Although formally similar, our proof must rely on our axioms only. So, in this section, an axiom that plays the role of those special properties in the proof that $M[G]$ is a model is extracted.

Let $a$ be a relation between individuals and conditions, that is, a set of pairs $(b, p)$ in $M$. We say that an individual $c$ is a $\mathbb{P}$-imitation of relation $a$ if $M \models b \in_p c$ iff $(b, p) \in a$, for all $b$ and $p$. If there is a $\mathbb{P}$-imitation of $a$, then the relation is downward closed in the sense that $(b, q) \in a$ whenever $(b, p) \in a$ and $q \le p$. The converse implication is our axiom (9), which means that every downward closed relation between individuals and conditions in $M$ is equivalent to $\mathbb{P}$-membership to an appropriate individual.

(9) Given an individual $a$, if $a$ is a downward closed relation between individuals and conditions, then there is a $\mathbb{P}$-imitation of $c$ of $a$. Every downward closed relation in $M$ is a projection of $\mathbb{P}$-membership.

Finally, we can state the main definition of this paper.

**Definition 5.** A standard forcing-generic extension is a forcing-generic extension satisfying axiom (9). More precisely, a standard forcing-generic extension is represented by a forcing-generic framework satisfying axiom (9) and endowed with a generic filter.

The informal idea behind this is that we do not want the $\mathbb{P}$-membership to an individual to be a particular kind of relation between individuals and conditions. Standard forcing-generic extensions can be proved to satisfy ZFC, as we shall see.

## 8. Completion of The Proof

We are now in position to complete the proof of the adequacy of our axiomatic approach to forcing and generic extensions. It remains only to show that standard forcing-generic extensions are models of ZFC. This section follows Section 6 in [5], pages 364 and 365, closely. We begin with two important lemmas

**Lemma 6 (Boundedness lemma).** Let $A$ be such that $A \subseteq M[G]$. If there is an individual $a$ such that every element of $A$ is $F_G(b)$ for some $b \in a$, then there is an individual $c$ such that $A \subseteq F_G(c)$.

**Proof.** In fact, let $a' = a \times \mathbb{P}$, which is a downward closed relation in $M$ between individuals and conditions, and let $c$ be a $\mathbb{P}$-imitation of $a'$. For every $b \in a$, it holds that $M \models b \in_1 c$, hence $F_G(b) \in F_G(c)$. Therefore, $A \subseteq F_G(c)$. $\square$

**Lemma 7 (Naming of definable subsets lemma).** Given an individual $a$, there is an individual $b$ such that for every definable $A \subseteq F_G(a)$, there is an individual $c \in b$ such that $F_G(c) = A$.

**Proof.** In fact, from the well-foundedness axiom, $\{d : \exists q; M \models d \in_q a\}$ is a set in $M$. Using replacement in $M$, let $b$ be a set containing a $\mathbb{P}$-imitation for each downward closed relation in $\wp^M(\{d : \exists q; M \models d \in_q a\} \times \mathbb{P})$. Let $\phi$ be a formula, and $\bar{a}$ an $n$-tuple such that

$$F_G(d) \in A \quad \text{iff} \quad M[G] \models \phi[F_G(d), F_G(\bar{a})],$$
for all individuals d. Let

$$c' = \{(d, p) : M \models \exists q; (d \in_q a) \wedge (p \Vdash \phi[d, \bar{a}])\}.$$

Notice that $c'$ is downward closed. Since $M$ is a transitive model, $c'$ is an individual in $M$, and $c' \in \wp^M(\{d : \exists q; M \models d \in_q a\} \times \mathbb{P})$. Let $c$ be a $\mathbb{P}$-imitation of $c'$ such that $c \in b$. One can verify that $F_G(c) = A$. □

In conclusion, we have a standard forcing-generic extension

$$[(M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G)]$$

and we want to prove that $M[G]$ is a model of ZF. This is very important, after all there is a problem with the $M[G]$ notation: $M[G]$ denotes $F_G[M]$, which may depend on $F$, that is, it may not be determined by $M$ and $G$ only. In order to remove the ambiguity of the $M[G]$ notation, it is enough to prove that it is a model of ZF, as we have seen in Section 6. This gap is filled by the next result.

**Theorem 8.** $M[G]$ is a transitive model of ZF.

**Proof.** Since $M[G]$ is a transitive $\epsilon$-structure, it satisfies regularity and extensionality. Since it contains $M$, hence $\omega \in M[G]$, it satisfies infinity. From the naming of definable subsets lemma above, separation holds in $M[G]$. For power set, let $F_G(a) \in M[G]$ and $F_G(d) \in \wp(F_G(a) \cap M[G])$. From the naming of definable subsets lemma, there are $b$ and $c$ such that $c \in b$ and $F_G(c) = F_G(d)$. The conditions of the boundedness lemma are, therefore, met and there is an individual $e$ such that $\wp(F_G(a) \cap M[G]) \subseteq F_G(e)$. From separation in $M[G]$, it follows that $\wp(F_G(a) \cap M[G]) \in M[G]$, and we have power set in $M[G]$.

Now, for ZF, it suffices to show that if $H$ is a definable class function in $M[G]$ and $a$ is an individual, then $\cup\{H(F_G(b)) : F_G(b) \in F_G(a)\}$ is included in a set in $M[G]$. Let $\psi$ be a formula defining $H$ in $M[G]$, that is,

$$H(F_G(b)) = F_G(c) \quad \text{iff} \quad M[G] \models \psi[F_G(b), F_G(c), F_G(\bar{a})].$$

Using replacement in $M$, let $d$ be an individual with the following property:

(i) For each condition $p$ and each individual $b$ such that $\exists q; M \models b \in_q a$, if there is a $c$ such that $M \models p \Vdash \psi[b, c, \bar{a}]$, then there is such an individual in $d$.

(ii) If $b \in d$ and $b'$ is such that $\exists q; M \models b' \in_q b$, then $b' \in d$.

In view of the boundedness lemma, we need just to prove that every element of $\cup\{H(F_G(b)) : F_G(b) \in F_G(a)\}$ has a name in $d$. Let

$$F_G(b') \in H(F_G(b)),$$

in which $F_G(b) \in F_G(a)$. We may suppose that $\exists q \in G; M \models b \in_q a$. If $c$ is a name for $H(F_G(b))$, then

$$M[G] \models \psi[F_G(b), F_G(c), F_G(\bar{a})],$$

hence there is a $p$ in $G$ such that $M \models p \Vdash \psi[b, c, \bar{a}]$. From the choice of $d$, for some $c' \in d$ we have that $M \models p \Vdash \psi[b, c', \bar{a}]$, from which, together with $p \in G$, it follows that

$$M[G] \models \psi[F_G(b), F_G(c'), F_G(\bar{a})].$$

Therefore,

$$F_G(c') = H(F_G(b)), \quad \text{so} \quad F_G(b') \in F_G(c') \quad \text{and} \quad F_G(b') = F_G(b''),$$

with $\exists q \in G; M \models b'' \in_q c'$. Finally, we conclude that $b'' \in d$, and every element of $\cup\{H(F_G(b)) : F_G(b) \in F_G(a)\}$ has a name in $d$, as required. □
We have that $M[G]$ is a model of ZF and that there is exactly one standard forcing-generic extension determined by $M$ and $G$, which can be identified with $M[G]$. The principal theorem of forcing, however, is that $M[G]$ is a model of ZFC, and we wish to achieve that with our approach. It only remains to show that the axiom of choice is also satisfied by $M[G]$.

**Lemma 9.** *M[G] satisfies the axiom of choice.*

**Proof.** From choice in $M$, for each $a$ there is, in $M$, a surjective function $f$ from an ordinal onto the individual $\{d : M \models \exists q; d \in_q a\}$. Since $M[G]$ is a model of ZF containing $M$ and $G$, the collapse $F_G^{M[G]}$ of $\epsilon_G^{M[G]}$ is definable in $M[G]$ and coincides with $F_G$ (because $\epsilon_G$ is absolute for $M[G]$). Composing this function with $F_G^{M[G]}$, a surjective function from an ordinal onto a set containing $F_G^{M[G]}(a) = F_G(a)$ is obtained. Therefore, an equivalent form of choice holds in $M[G]$, and $M[G]$ is a model of ZFC. □

**9. Existence of Standard Forcing-Generic Extensions**

We have proved that if we are given a transitive model $M$ of ZFC, an absolute partial ordering $\mathbb{P}$ in $M$, a $\mathbb{P}$-membership relation $R$, a forcing predicate $\Vdash \phi$ for each formula $\phi$ of the basic language of set theory, a genericity predicate $C$, a filter $G$ satisfying the genericity predicate, such that axioms (1)–(9) are valid for these data, then

(1) $G$ intersects all dense sets in $M$;

(2) the forcing predicates satisfy an inductive definition given by familiar inductive clauses;

(3) the image $F_G[M]$ of the transitive collapse of the well-founded relation $\epsilon_G$, defined in terms of $G$ and $R$, is a transitive model of ZFC containing $M$ and $G$, and is uniquely determined by $M$ and $G$ as the least such model.

If the data arranged in the sextuple $(M, \mathbb{P}, R, \{\Vdash \phi : \phi \in L(\epsilon)\}, C, G)$ satisfy axioms (1)–(9), then it is said to represent a standard forcing-generic extension. Relying on what was done so far, a construction of such a sextuple can be given without further ado.

• Let $M$ be a countable transitive model.

• Let $\mathbb{P}$ be an absolute partial ordering in $M$ with greatest element 1.

• Define a $\mathbb{P}$-membership relation $R$ by the following clause.

$$M \Vdash a \in_p b \text{ iff } \forall q \le p; (a, q) \in b.$$

• Define predicates $\Vdash \phi$ inductively by the following clauses.

- $M \Vdash (p \Vdash a \in b)$ iff $M \Vdash \forall r \le p; \exists q \le r; \exists x; (x \in_q b \land q \Vdash a = x)$.

- $M \Vdash (p \Vdash a \neq b)$ iff $M \Vdash \forall r \le p; \exists q \le r; \exists x; (x \in_q a \land q \Vdash x \notin b) \lor (x \in_q b \land q \Vdash x \notin a)$.

- $M \Vdash (p \Vdash a = b)$ iff $M \Vdash \forall q \le p; q \Vdash (a \neq b)$.

- $M \Vdash (p \Vdash \neg\phi)[\bar{a}]$ iff $M \Vdash \forall q \le p; (q \Vdash \neg\phi)[\bar{a}]$.

- $M \Vdash (p \Vdash \phi \lor \psi)[\bar{a}]$ iff $M \Vdash \forall r \le p; \exists q \le r; (q \Vdash \phi \lor q \Vdash \psi)[\bar{a}]$.

- $M \Vdash (p \Vdash \phi \land \psi)[\bar{a}]$ iff $M \Vdash (p \Vdash \phi \land p \Vdash \psi)[\bar{a}]$.

- $M \Vdash (p \Vdash \exists x; \phi)[\bar{a}]$ iff $M \Vdash \forall r \le p; \exists q \le r; \exists x; (q \Vdash \phi)[\bar{a}]$.

• Define a genericity predicate $C$ by stipulating that a filter is generic iff it intersects every dense set which is in $M$.

• Let $G$ be any generic filter.

The above data represent a standard forcing-generic extension. Indeed, this construction of a standard forcing-generic extension is very similar to those found in the usual expositions of the subject. However, in contrast with the traditional approach, the construction we are providing here is entirely suggested by the previous development of our axioms, hence a natural outcome of it.
**Proof.** Given a generic filter $G$, the equivalence between

$$M[G] \models \phi[F_G(\bar{a})]$$

and

$$\exists p \in G; M \models (p \Vdash \phi)[\bar{a}],$$

for all $\phi, \bar{a}$, is proved by induction on the complexity of $\phi$.

We have already proved that our sextuple satisfies several axioms. In particular, the downward closedness axioms are satisfied by our sextuple, a fact which is used throughout the proof.

**Preliminary remark.** For any downward closed set of conditions $A \in M$,

$$\exists p \in G; \forall r \le p; \exists sq \le r; q \in A$$

is equivalent to $\exists p \in G; p \in A$. This equivalence is a direct consequence of Lemma 3, which follows from the definition of genericity and the existence theorem for generic filters.

Our preliminary remark above is extensively used in conjunction with the downward closedness of forcing and $P$-membership.

**Basis step.** We now prove the following statements, for all individuals $a$ and $b$.

(1) $F_G(a) \in F_G(b)$ iff $\exists p \in G; M \models (p \Vdash a \in b)$;

(2) $F_G(a) = F_G(b)$ iff $\exists p \in G; M \models (p \Vdash a = b)$;

(3) $F_G(a) \neq F_G(b)$ iff $\exists p \in G; M \models (p \Vdash a \neq b)$.

**Proof of (1).** The inclusion $F_G(a) \in F_G(b)$ is equivalent to

$$\exists c \in G; F_G(a) = F_G(c).$$

Let us momentarily assume that $F_G(a) = F_G(c)$ is equivalent to

$$\exists p \in G; M \models (p \Vdash a = c).$$

Hence, $F_G(a) \in F_G(b)$ is equivalent to $\exists c \in G; \exists p \in G; M \models (p \Vdash a = c)$, which is equivalent to

$$\exists c \in M; (\exists q \in G; M \models (c \in q \ b \land \exists p \in G; M \models (p \Vdash a = c))).$$

This is equivalent to $\exists p \in G; \exists c \in M; M \models (c \in p \ b \land p \Vdash a = c)$, because $G$ is a filter (so that given $p, q \in G$, there is a condition $r \in G$ such that $r \le p, q$) and the predicates involved are downward closed.

Finally, from our preliminary remark,

$$\exists p \in G; \exists c \in M; M \models (c \in p \ b \land p \Vdash a = c)$$

is equivalent to

$$\exists p \in G; \forall r \le p; \exists q \le r; \exists c \in M; M \models (c \in q \ b \land q \Vdash a = c),$$

which is equivalent to $M \models (p \Vdash a \in b)$.

However, the proof is pending, for equivalence (2) must be verified.

**Proof of (2).** The equation $F_G(a) = F_G(b)$ is equivalent to $\neg(F_G(a) \neq F_G(b))$. Let us momentarily assume that $F_G(a) \neq F_G(b)$ is equivalent to

$$\exists p \in G; M \models (p \Vdash a \neq b),$$

so that $F_G(a) = F_G(b)$ is equivalent to $\forall p \in G; M \models (p \Vdash a \neq b)$.

The set $\{q : M \models (q \Vdash a \neq b) \lor M \models (q \Vdash \neg a \neq b)\}$ is dense, hence it intersects $G$. From this,

$$\forall p \in G; M \models (p \Vdash a \neq b)$$
implies that $\exists p \in G; M \models (p \Vdash \neg a \neq b)$, which is equivalent to

$$ \exists p \in G; M \models (p \Vdash a = b), $$

by definition. Conversely,

$$ \exists p \in G; M \models (p \Vdash a = b) $$

implies that $\forall p \in G; M \models (p \Vdash a \neq b)$. In fact, let $p \in G$ be such that

$$ M \models (p \Vdash a = b). $$

Assume that $r \in G$ is such that $M \models (r \Vdash a \neq b)$. Now, G is a filter, hence there is a $q \in G$ such that $q \leq r, p$. From the downward closedness of forcing, $M \models (q \Vdash a = b)$ and $M \models (q \Vdash a \neq b)$, a contradiction. So,

$$ \forall p \in G; M \models (p \Vdash a \neq b). $$

Therefore, (2) is true, with the proviso that equivalence (3) must now be verified.

**Proof of (3).** The proof is given by transfinite induction on the maximum of the ranks of a and b. So, assume the induction hypothesis. The inequality $F_G(a) \neq F_G(b)$ is equivalent to

$$ \exists c \in M; (F_G(c) \in F_G(a) \setminus F_G(b)) \lor \exists c \in M; (F_G(c) \in F_G(b) \setminus F_G(a)). $$

By symmetry, it is enough to analyze only the first component of this disjunction.

* $\exists c \in M; (F_G(c) \in F_G(a) \land F_G(c) \notin F_G(b))$ iff

* $\exists c \in M; ((\exists d \in G a; F_G(c) = F_G(d)) \land F_G(c) \notin F_G(b))$ iff

* $\exists c \in M; \exists d \in G a; (F_G(c) = F_G(d) \land F_G(c) \notin F_G(b))$ iff

* $\exists d \in G a; \exists c \in M; (F_G(c) = F_G(d) \land F_G(c) \notin F_G(b))$ iff

* $\exists d \in G a; (F_G(d) \notin F_G(b))$ iff

* $\exists c \in G a; (F_G(c) \notin F_G(b))$ iff

* $\exists c \in G a; \forall d \in G b; (F_G(c) \neq F_G(b))$ iff (from the induction hypothesis, since the maximum of the ranks of c and d is strictly less than the maximum of the ranks of a and b)

* $\exists c \in G a; \forall d \in G b; \exists p \in G; M \models (p \Vdash c \neq d)$ iff

* $\exists c \in G a; \exists p \in G; M \models (p \Vdash c \notin b)$.

The last equivalence requires a proof. Before going further into that, let us show that the basis step is then completed. We would have that

* $\exists c \in M; (F_G(c) \in F_G(a) \setminus F_G(b)) \lor \exists c \in M; (F_G(c) \in F_G(b) \setminus F_G(a))$ iff

* $\exists c \in G a; (\exists p \in G; M \models (p \Vdash c \notin b)) \lor \exists c \in G b; (\exists p \in G; M \models (p \Vdash c \notin a))$ iff

* $\exists p \in G; (\exists q \in G; \exists c \in M; M \models (c \in q a \land p \Vdash c \notin b) \lor \exists q \in G; \exists c \in M; M \models (c \in q b \land p \Vdash c \notin a))$ iff

* $\exists p \in G; (\exists c \in M; M \models (c \in p a \land p \Vdash c \notin b) \lor \exists c \in M; M \models (c \in p b \land p \Vdash c \notin a))$.

However, from our preliminary remark,

$$ \exists p \in G; (\exists c \in M; M \models (c \in p a \land p \Vdash c \notin b) \lor (c \in p b \land p \Vdash c \notin a)) $$

is equivalent to

$$ \exists p \in G; M \models (p \Vdash a \neq b), $$

hence we would have achieved the desired conclusion.
So, let us prove what is missing. Assume that

$$ \forall d \in G; \exists p \in G; M \models (p \Vdash c \neq d), $$

in which $c \in_G a$.

Let $D$ be the set

$$ \{q : M \models (q \Vdash c \in b) \lor M \models (q \Vdash c \notin b)\}. $$

Since $D$ is dense, there is a condition $q$ such that $q \in D \cap G$. Suppose that $M \models (q \Vdash c \in b)$. Using the defining clause, one obtains

$$ \exists q \in G; \forall r \leq q; \exists s \leq r; \exists d \in M; M \models (d \in_s b \land s \Vdash c = d). $$

From our preliminary remark,

$$ \exists q \in G; \exists d \in M; M \models (d \in_q b \land q \Vdash c = d). $$

Therefore, there is a $d \in_G b$ such that $M \models (q \Vdash c = d)$, for some $q \in G$. However, from our assumption, for any such $d$, there is a $p \in G$ such that $M \models (p \Vdash c \neq d)$. Let $r \in G$ be stronger than $p$ and $q$. Then we get a contradiction which shows that there is no $q \in G$ such that

$$ M \models (q \Vdash c \in b). $$

Hence, $\exists q \in G; M \models (q \Vdash c \notin b)$, which concludes the proof of the direct implication.

Conversely, assume that there is a $p \in G$ such that $M \models (p \Vdash c \notin b)$, and fix such a condition. Let $d$ be any individual such that $d \in_G b$, and let $q \in G$ be such that $M \models d \in_q b$. The generic filter $G$ intersects the dense set

$$ \{r : M \models (r \Vdash c \neq d) \lor M \models (r \Vdash c = d)\}. $$

Assume, contrary to the desired conclusion, that there is an $r \in G$ such that $M \models (r \Vdash c = d)$. Since $G$ is a filter, we can take $r$ to be stronger than $p$ and $q$. From this, it follows that

$$ M \models (d \in_r b \land r \Vdash c = d) \quad \text{and} \quad M \models (r \Vdash c \notin b), $$

a contradiction, for $M \models (d \in_r b \land r \Vdash c = d)$ implies $M \models (r \Vdash c \in b)$.

Therefore,

$$ \forall d \in_G b; \exists q \in G; M \models (q \Vdash c \neq d). $$

The converse implication is proved and the basis step is done.

**Inductive step.** We say that $\phi$ has the property $T$ if for all $\bar{a}$ and $G$,

$$ M[G] \models \phi[F_G(\bar{a})] \quad \text{iff} \quad \exists p \in G; M \models (p \Vdash \phi)[\bar{a}]. $$

The truth lemma says that property $T$ holds for all $\phi$. We have already proved that property $T$ holds for all atomic formulas. In order to complete the proof of the truth lemma, it is enough to show that $\neg \phi$, $\phi \lor \psi$ and $\exists x; \phi$ have the property, under the inductive assumption that it holds for $\phi$ and $\psi$.

**Proof that $\neg \phi$ has the property.** In this case,

* $M[G] \models (\neg \phi)[F_G(\bar{a})]$ iff

* $M[G] \not\models \phi[F_G(\bar{a})]$ iff

* $\forall p \in G; M \not\models (p \Vdash \phi)[\bar{a}]$.

The last clause implies that

$$ \exists p \in G; M \models (p \Vdash \neg \phi)[\bar{a}], $$

because $\{p : M \models (p \Vdash \phi)[\bar{a}] \lor M \models (p \Vdash \neg \phi)[\bar{a}]\}$ is dense. Conversely,

$$ \exists p \in G; M \models (p \Vdash \neg \phi)[\bar{a}] $$

implies that $\forall p \in G; M \not\models (p \Vdash \phi)[\bar{a}]$, because $G$ is a filter and forcing is consistent.
**Proof that $\phi \lor \psi$ has the property.** In this case,

• $M[G] \models (\phi \lor \psi)[F_G(\bar{a})]$ iff

• $M[G] \models \phi[F_G(\bar{a})] \lor M[G] \models \psi[F_G(\bar{a})]$ iff

• $\exists p \in G; M \models (p \Vdash \phi)[\bar{a}] \lor \exists p \in G; M \models (p \Vdash \psi)[\bar{a}]$ iff

• $\exists p \in G; (M \models (p \Vdash \phi)[\bar{a}] \lor M \models (p \Vdash \psi)[\bar{a}])$ iff

• $\exists p \in G; M \models (p \Vdash \phi \lor p \Vdash \psi)[\bar{a}]$.

From our preliminary remark, the last clause is equivalent to $\exists p \in G; M \models (p \Vdash \phi \lor \psi)[\bar{a}]$.

**Proof that $\exists x; \phi$ has the property.** In this case,

• $M[G] \models (\exists x; \phi)[F_G(\bar{a})]$ iff

• $\exists a \in M; M[G] \models \phi[F_G(\bar{a}, a)]$ iff

• $\exists a \in M; \exists p \in G; M \models p \Vdash \phi[\bar{a}, a]$ iff

• $\exists p \in G; \exists a \in M; M \models p \Vdash \phi[\bar{a}, a]$.

From our preliminary remark, the last clause is equivalent to $\exists p \in G; M \models p \Vdash \exists x; \phi[\bar{a}]$, which
concludes the proof. □

Our construction satisfies all axioms. It represents, therefore, the unique standard forcing-
generic extension determined by *M* and *G*.

**10. Closing Remarks**

Briefly, a forcing-generic extension is a ground-controlled uniform adjunction of a generic filter,
and the forcing predicates constitute the relevant control apparatus. This concept is what we
hopefully have elucidated. Besides that, we have provided an alternative presentation of the
subject. We have first axiomatized the fundamental properties of a forcing-generic extension.
Subsequently, we have inquired into the consequences of these properties, realizing that generic
filters must indeed intersect all dense sets and usual, but apparently ad hoc, clauses for forcing
predicates must hold. Standard forcing-generic extensions were shown to give rise to transitive
models of set theory which are uniquely determined by the ground and the generic filter. Finally,
we have proved that standard forcing-generic extensions do exist, and that a construction of such
an extension can be entirely based on our axiomatic development of the subject.

Some interesting open problems are suggested by our approach, to give a similar treatment
for class forcing is perhaps the most immediate. The general situation of class forcing is not
very clear, at least conceptually speaking, as it does not give rise to models in all cases. Up to
a certain point, our approach can be easily adapted to treat class forcing as well. However, the
proof that $M[G]$ is a model heavily uses that $\mathbb{P}$ is a set in $M$. To treat the case of symmetric
extensions similarly is also suggested. Other problems which may be relevant concern the role
of "nonstandard" forcing-generic extensions (those satisfying axiom (1)–(8) only) and possible
relations to noncommutative forcing.

All important basic theorems of the subject known as forcing with posets can be derived
from the nine axioms, which are formal counterparts of a few general principles behind that
mathematical practice. In particular, some extended definitions and arguments of the subject
which may seem unnatural at first sight are accounted by these few principles worth recalling:
The fundamental duality principle (formalized by axioms (7) and (8)), the uniform adjunction
principle (formalized by axioms (5) and (6)), the generic existence principle (formalized by
axiom (4)), the downward closedness and well-foundedness of forcing principles (formalized by
axioms (1), (2) and (3)) and the universality of $\mathbb{P}$-membership principle (formalized by axiom (9)).
In this sense, through our principles, we have thus accomplished a conceptual foundation of the
subject.
Forcing is a lively subject of which we have covered only the basics in a new fashion. Since it is also a very important area of set theory, it is desirable to enrich the subject with different approaches. A very useful feature is that generic extensions can be iterated. Iterated forcing has amplified the scope of application and has pointed to new directions of research. The approach through boolean-valued models and many classical applications of the method can be found in [1]. Forcing axioms have been very actively researched, with many applications in set theory (see [6], for one important example) and in other branches of mathematics. Yet there is a lot of work to be done.

## Acknowledgement

I am indebted to Boban Velickovic for many suggestions which made the article better.

## References

[1] T. Jech, *Set theory*, Springer Monographs in Mathematics, Springer, 2003.

[2] K. Kunen, *Set theory: An introduction to independence proofs*, Studies in Logic and the Foundations of Mathematics, vol. 102, North-Holland, 1980.

[3] A. Levy, "Definability in axiomatic set theory. I", in *Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress*, Studies in Logic and the Foundations of Mathematics, North-Holland, 1964.

[4] J. R. Shoenfield, *Mathematical logic*, Addison-Wesley Publishing Group, 1967.

[5] —, *Unramified forcing*, Proceedings of Symposia in Pure Mathematics, vol. 13, American Mathematical Society, 1971.

[6] M. Viale, "The proper forcing axiom and the singular cardinal hypothesis", *J. Symb. Log.* **71** (2006), no. 2, p. 473-479.