I have proposed such an axiomatization. It is to appear in comptes rendus: mathematique. Here is a link to the preprint version:

https://www.researchgate.net/publication/343774583_AN_AXIOMATIC_APPROACH_TO_FORCING_AND_GENERIC_EXTENSIONS

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).

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).

I have proposed such an axiomatization. It is to appear in comptes rendus: mathematique. Here is a link to the preprint version:

https://www.researchgate.net/publication/343774583_AN_AXIOMATIC_APPROACH_TO_FORCING_AND_GENERIC_EXTENSIONS

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$ a predicate (the genericity predicate).

As usual, we use $G$ to denote a filter satisfying the genericity predicate $C$. Let $F_G$ denote the trnsitive collapse of

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).

I have proposed such an axiomatization. It is to appear in comptes rendus: mathematique. Here is a link to the preprint version:

https://www.researchgate.net/publication/343774583_AN_AXIOMATIC_APPROACH_TO_FORCING_AND_GENERIC_EXTENSIONS

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).