Informally the axiom *schema* of accessibility states that for each unary function $F$ that is definable over the whole universe of discourse "in the language of set theory", like the powerset function $P$, or the singleton function $\iota$, or the set Union function $\bigcup$, etc.. for each such a function $F$ we can coin an accessibility notion [dependent on $F$] whereby a set $x$ is said to be reached (i.e. is accessible) from a set $\alpha$ if and only if there is a set $\beta$ that is hereditarily strictly subnumerous to $x$ such that $F(\beta)$ is supernumerous to $x$ and $\alpha \subseteq \beta$; or otherwise $x$ is hereditarily subnumerous to $\alpha$ . Now the scheme states that per each definable unary function $F$ for every set $x$ there exists a set of all sets that are hereditarily $F$ accessible from $x$. The real intention is to have a theory that can prove the existence of large cardinals. Infinity is provable since all hereditarily finite sets are seen as hereditarily power accessible from the set $\emptyset$. Now it can be proved that the set of all cardinals that are hereditarily Power (of Set Union) accessible from $\omega_0$ exists and this would be a regular limit of regular cardinals, i.e. the first inaccessible cardinal, and from that one can prove the existence of a set of all sets that are hereditarily strictly subnumerous to this first inaccessible, and this would serve as a domain of a model of $\text{ZF}$. To get to that, we only need to add this axiom scheme on top of axioms of Zermelo set theory minus infinity and add an axiom of Transitivity that asserts that every set is a subset of some transitive set, this way we can define transitive closures and define the hereditary notions. The issues are: what would be the consistency strength of this theory? how much this theory is stronger than the theory with the $F$ function fixed to be the Power of union set function, i.e. $\forall x,y \ [F(x)=y \leftrightarrow y=P(\bigcup(x))]$? what kinds of inaccessible cardinals can this theory prove? Would this theory prove Replacement?

Formal workup:

$\text{Axiom schema of Accessibility:}$ if $``F"$ is a symbol that denotes a unary function that is ** definable** in the language of set theory over the whole universe of discourse, and if $\phi(Y)$ is a formula in which $X$ doesn't occur free and $Y$ occurs free and only free, then all closures of:

$$[\exists \alpha \forall Y (\phi(Y) \to Y \ ..ACC^F \ \alpha)] \to \exists X \forall Y (Y \in X \leftrightarrow \phi(Y))$$ are axioms.

Where $ACC^F$ is defined as:

$$Y \ ACC^F \ \alpha \iff Y\ ..\leq \ \alpha \lor \exists \beta \ [\beta \ ..< \ Y \wedge \alpha \subseteq \beta \wedge F(\beta) \geq Y] $$

Where generally $``..R"$ denotes "hereditarily $R$" relation defined as:

$$ X \ ..R \ \ Y \iff X \ R \ Y \wedge \forall m \in TC(X) [m \ R \ Y]$$

Where $TC(X)$ is defined in the customary manner as the minimal transitive superset of $X$.

Where: $ x < y \iff \exists f (f:x\to y \wedge f \text{ is an injection}) \wedge \not \exists g (g: y \to x \wedge g \text{ is an injection})$

and: $ x \geq y \iff \exists f (f: y \to x \wedge f \text { is an injection} )$;

and: $ x \leq y \iff y \geq x$

Now the question is:

What is the consistency strength of the theory whose axioms are the axioms of $[\text{Z} - \text{INF.}] + \text{Transitivity} + \text{Accessibility}?$

Where Axiom of Transitivity is the axiom stating that every set is a subset of some transitive set.

In particular would Replacement be provable in this theory?