Assertion $A^*$ is strictly stronger than assertion $A$.

Denote by $Z$ the theory with axioms Extensionality, Empty Set, Pairing, Union, Power Set, Infinity, Separation Schema, Foundation. Adding Choice is yields a theory which is essentially your $T$ but for an important fine point, namely, the precise formulation of the Axiom of Infinity. My own preference is for the Axiom of Infinity to be the assertion of the existence of a Kuratowski infinite set. This assertion is provably weaker than both Zermelo's original formulation and the customary formulation in terms of inductive sets (see Slim Models of Zermelo Set Theory by Mathias).

Let $F$ be the theory obtained from $Z$ by replacing my preferred Axiom of Infinity by its negation. In this theory, Replacement is a theorem schema and Choice is a theorem: thus, $F$ is a reformulation of the finite theory of Enayat-Schmerl-Visser's article $\omega$-models of finite set theory.

Let ${\bf M}=(X,\lhd)$ be an $\omega$-model of $F+ \exists \phi(x)$ where $\phi(x)$ is the assertion "every element of the transitive closure of {$x$} is a singleton". Note that membership in this transitive closure is expressible by a first-order formula. There is no requirement that this transitive closure exist as a set: indeed it cannot, since $\bf M\models$ Foundation. There are various ways to obtain such a model. One method is to apply the Rieger-Bernays permutation procedure to the standard model $(V_\omega\in)$ and a cleverly chosen permutation $\sigma:V_\omega\rightarrow V_\omega$ to obtain ${\bf M}=(V_\omega,\in_\sigma)$ where $x \in_\sigma y\Leftrightarrow x\in \sigma(y)$: see Section 3 of A note on recursive models of set theory by Mancini-Zambella. Another is to construct $\bf M$ directly by starting with a linear order $\ldots < x_{n+1}< x_n\ldots< x_0$ and iterating $\omega$ many times the procedure of formally adjoining power sets of finite subsets (taking care to e.g. identify {$x_{n+1}$} with $x_n$). For details, see the paper of Enayat-Schmerl-Visser.

In work in progress addressed at my own Math Overflow question Can one exhibit an explicit Kuratowski infinite set without invoking Replacement? I've been adapting this idea of formally adjoining power sets to the setting where one is given an $\omega$-model of $F$ and an appropriate collection of (external) infinite subsets of its underlying set, and where one wishes to produce a suitably minimal $\omega$-model of $Z$ whose "hereditarily finite" sets are those of the original model, and which has members with the specified infinite extensions. Given ${\bf M}=(X,\lhd)$ as in the previous paragraph, for every $x$ such that $\phi(x)$ we formally adjoin an element with extension {$x$,{$x$},{{$x$}},$\ldots$}, then formally adjoin any missing elements with finite extension in this augmented domain (taking due care as alluded to previously) and iterate $\omega$-many times. The resulting structure $\widehat{\bf M}$ will be a model of $Z$ (including the Axiom of Infinity) with the property that the class $V_\omega$ has no infinite subset.

For reasons of symmetry, $\widehat{\bf M}$ has no definable infinite sets. While this responds to the question I originally posed, the fact that Transitive Containment is violated feels a bit like cheating. I have another construction for that, but I am digressing far too much already.

My proposal would be to modify the recipe by also formally adjoining an element with extension $V_\omega$ at the first stage, then proceeding as indicated above, i.e. lather, rinse and repeat $\omega$ many times.

Assertion $A^*$ is strictly stronger than assertion $A$.

Denote by $Z$ the theory with axioms Extensionality, Empty Set, Pairing, Union, Power Set, Infinity, Separation Schema, Foundation. Adding Choice is yields a theory which is essentially your $T$ but for an important fine point, namely, the precise formulation of the Axiom of Infinity. My own preference is for the Axiom of Infinity to be the assertion of the existence of a Kuratowski infinite set. This assertion is provably weaker than both Zermelo's original formulation and the customary formulation in terms of inductive sets (see Slim Models of Zermelo Set Theory by Mathias).

Let $F$ be the theory obtained from $Z$ by replacing my preferred Axiom of Infinity by its negation. In this theory, Replacement is a theorem schema and Choice is a theorem: thus, $F$ is a reformulation of the finite theory of Enayat-Schmerl-Visser's article $\omega$-models of finite set theory.

Let ${\bf M}=(X,\lhd)$ be an $\omega$-model of $F+ \exists \phi(x)$ where $\phi(x)$ is the assertion "every element of the transitive closure of {$x$} is a singleton". Note that membership in this transitive closure is expressible by a first-order formula. There is no requirement that this transitive closure exist as a set: indeed it cannot, since $\bf M\models$ Foundation. There are various ways to obtain such a model. One method is to apply the Rieger-Bernays permutation procedure to the standard model $(V_\omega\in)$ and a cleverly chosen permutation $\sigma:V_\omega\rightarrow V_\omega$ to obtain ${\bf M}=(V_\omega,\in_\sigma)$ where $x \in_\sigma y\Leftrightarrow x\in \sigma(y)$: see Section 3 of A note on recursive models of set theory by Mancini-Zambella. Another is to construct $\bf M$ directly by starting with a linear order $\ldots < x_{n+1}< x_n\ldots< x_0$ and iterating $\omega$ many times the procedure of formally adjoining power sets of finite subsets (taking care to e.g. identify {$x_{n+1}$} with $x_n$). For details, see the paper of Enayat-Schmerl-Visser.

In work in progress addressed at my own Math Overflow question Can one exhibit an explicit Kuratowski infinite set without invoking Replacement? I've been adapting this idea of formally adjoining power sets to the setting where one is given an $\omega$-model of $F$ and an appropriate collection of (external) infinite subsets of its underlying set, and where one wishes to produce a suitably minimal $\omega$-model of $Z$ whose "hereditarily finite" sets are those of the original model, and which has members with the specified infinite extensions. Given ${\bf M}=(X,\lhd)$ as in the previous paragraph, for every $x$ such that $\phi(x)$ we formally adjoin an element with extension {$x$,{$x$},{{$x$}},$\ldots$}, then formally adjoin any missing elements with finite extension in this augmented domain (taking due care as alluded to previously) and iterate $\omega$-many times. The resulting structure $\widehat{\bf M}$ will be a model of $Z$ (including the Axiom of Infinity) with the property that the class $V_\omega$ has no infinite subset.

For reasons of symmetry, $\widehat{\bf M}$ has no definable infinite sets. While this responds to the question I originally posed, the fact that Transitive Containment is violated feels a bit like cheating. I have another construction for that, but I am digressing far too much already.

My proposal would be to modify the recipe by also formally adjoining an element with extension $V_\omega$ at the first stage, then proceeding as indicated above, i.e. lather, rinse and repeat $\omega$ many times.

Assertion $A^*$ is strictly stronger than assertion $A$.

Denote by $Z$ the theory with axioms Extensionality, Empty Set, Pairing, Union, Power Set, Infinity, Separation Schema, Foundation. Adding Choice is yields a theory which is essentially your $T$ but for an important fine point, namely, the precise formulation of the Axiom of Infinity. My own preference is for the Axiom of Infinity to be the assertion of the existence of a Kuratowski infinite set. This assertion is provably weaker than both Zermelo's original formulation and the customary formulation in terms of inductive sets (see Slim Models of Zermelo Set Theory by Mathias).

Let $F$ be the theory obtained from $Z$ by replacing my preferred Axiom of Infinity by its negation. In this theory, Replacement is a theorem schema and Choice is a theorem: thus, $F$ is a reformulation of the finite theory of Enayat-Schmerl-Visser's article $\omega$-models of finite set theory.

Let ${\bf M}=(X,\lhd)$ be an $\omega$-model of $F+ \exists \phi(x)$ where $\phi(x)$ is the assertion "every element of the transitive closure of {$x$} is a singleton". Note that membership in this transitive closure is expressible by a first-order formula. There is no requirement that this transitive closure exist as a set: indeed it cannot, since $\bf M\models$ Foundation. There are various ways to obtain such a model. One method is to apply the Rieger-Bernays permutation procedure to the standard model $(V_\omega\in)$ and a cleverly chosen permutation $\sigma:V_\omega\rightarrow V_\omega$ to obtain ${\bf M}=(V_\omega,\in_\sigma)$ where $x \in_\sigma y\Leftrightarrow x\in \sigma(y)$: see Section 3 of A note on recursive models of set theory by Mancini-Zambella. Another is to construct $\bf M$ directly by starting with a linear order $\ldots < x_{n+1}< x_n\ldots< x_0$ and iterating $\omega$ many times the procedure of formally adjoining power sets of finite subsets (taking care to e.g. identify {$x_{n+1}$} with $x_n$). For details, see the paper of Enayat-Schmerl-Visser.

In work in progress addressed at my own Math Overflow question Can one exhibit an explicit Kuratowski infinite set without invoking Replacement? I've been adapting this idea of formally adjoining power sets to the setting where one is given an $\omega$-model of $F$ and an appropriate collection of (external) infinite subsets of its underlying set, and where one wishes to produce a suitably minimal $\omega$-model of $Z$ whose "hereditarily finite" sets are those of the original model, and which has members with the specified infinite extensions. Given ${\bf M}=(X,\lhd)$ as in the previous paragraph, for every $x$ such that $\phi(x)$ we formally adjoin an element with extension {$x$,{$x$},{{$x$}},$\ldots$}, then formally adjoin any missing elements with finite extension in this augmented domain (taking due care as alluded to previously) and iterate $\omega$-many times. The resulting structure $\widehat{\bf M}$ will be a model of $Z$ (including the Axiom of Infinity) with the property that the class $V_\omega$ has no infinite subset.

For reasons of symmetry, $\widehat{M}$ has no definable infinite sets. While this responds to the question I originally posed, the fact that Transitive Containment is violated feels a bit like cheating. I have another construction for that, but I am digressing far too much already.

My proposal would be to modify the recipe by also formally adjoining an element with extension $V_\omega$ at the first stage, then proceeding as indicated above, i.e. lather, rinse and repeat $\omega$ many times.

Assertion $A^*$ is strictly stronger than assertion $A$.

Denote by $Z$ the theory with axioms Extensionality, Empty Set, Pairing, Union, Power Set, Infinity, Separation Schema, Foundation. Adding Choice is yields a theory which is essentially your $T$ but for an important fine point, namely, the precise formulation of the Axiom of Infinity. My own preference is for the Axiom of Infinity to be the assertion of the existence of a Kuratowski infinite set. This assertion is provably weaker than both Zermelo's original formulation and the customary formulation in terms of inductive sets (see Slim Models of Zermelo Set Theory by Mathias).

Let $F$ be the theory obtained from $Z$ by replacing my preferred Axiom of Infinity by its negation. In this theory, Replacement is a theorem schema and Choice is a theorem: thus, $F$ is a reformulation of the finite theory of Enayat-Schmerl-Visser's article $\omega$-models of finite set theory.

Let ${\bf M}=(X,\lhd)$ be an $\omega$-model of $F+ \exists \phi(x)$ where $\phi(x)$ is the assertion "every element of the transitive closure of {$x$} is a singleton". Note that membership in this transitive closure is expressible by a first-order formula. There is no requirement that this transitive closure exist as a set: indeed it cannot, since $\bf M\models$ Foundation. There are various ways to obtain such a model. One method is to apply the Rieger-Bernays permutation procedure to the standard model $(V_\omega\in)$ and a cleverly chosen permutation $\sigma:V_\omega\rightarrow V_\omega$ to obtain ${\bf M}=(V_\omega,\in_\sigma)$ where $x \in_\sigma y\Leftrightarrow x\in \sigma(y)$: see Section 3 of A note on recursive models of set theory by Mancini-Zambella. Another is to construct $\bf M$ directly by starting with a linear order $\ldots < x_{n+1}< x_n\ldots< x_0$ and iterating $\omega$ many times the procedure of formally adjoining power sets of finite subsets (taking care to e.g. identify {$x_{n+1}$} with $x_n$). For details, see the paper of Enayat-Schmerl-Visser.

In work in progress addressed at my own Math Overflow question Can one exhibit an explicit Kuratowski infinite set without invoking Replacement? I've been adapting this idea of formally adjoining power sets to the setting where one is given an $\omega$-model of $F$ and an appropriate collection of (external) infinite subsets of its underlying set, and where one wishes to produce a suitably minimal $\omega$-model of $Z$ whose "hereditarily finite" sets are those of the original model, and which has members with the specified infinite extensions. Given ${\bf M}=(X,\lhd)$ as in the previous paragraph, for every $x$ such that $\phi(x)$ we formally adjoin an element with extension {$x$,{$x$},{{$x$}},$\ldots$}, then formally adjoin any missing elements with finite extension in this augmented domain (taking due care as alluded to previously) and iterate $\omega$-many times. The resulting structure $\widehat{\bf M}$ will be a model of $Z$ (including the Axiom of Infinity) with the property that the class $V_\omega$ has no infinite subset.

For reasons of symmetry, $\widehat{\bf M}$ has no definable infinite sets. While this responds to the question I originally posed, the fact that Transitive Containment is violated feels a bit like cheating. I have another construction for that, but I am digressing far too much already.

My proposal would be to modify the recipe by also formally adjoining an element with extension $V_\omega$ at the first stage, then proceeding as indicated above, i.e. lather, rinse and repeat $\omega$ many times.