4 deleted 6 characters in body

Any positive integer can be written uniquely as a sum of distinct powers of 2. PA knows this, in the sense that one can write down a formula $\phi(x,y)$ meaning in the standard model that the $x$-th bit in the binary expansion of $y$ is 1. Moreover we can construct $\phi$ so that PA will prove all the expected facts about the $x$-th bit in the binary expansion of $y$.

If $M$ is any model of PA, then by taking $\phi(x,y)$ as the membership relation "$x\in y$" we get a model of ZF-Inf. This is worked out in loving detail in Chapter 1 of "Metamathematics of First Order Arithmetic" by Hajek and Pudlak. In fact the authors carry this out not just for PA but for the subtheory $\text{I}\Sigma_0(\text{exp})$.

(Added) I expected that every model $M$ of ZF-Inf would arise in this way, by applying the above construction to the model of PA consisting of the ordinals of $M$. But it seems this is not so... See Ali's answer below.

3 added 61 characters in body

Any positive integer can be written uniquely as a sum of distinct powers of 2. PA knows this, in the sense that one can write down a formula $\phi(x,y)$ meaning in the standard model that the $x$-th bit in the binary expansion of $y$ is 1. Moreover we can construct $\phi$ so that PA will prove all the expected facts about the $x$-th bit in the binary expansion of $y$.

If $M$ is any model of PA, then by taking $\phi(x,y)$ as the membership relation "$x\in y$" we get a model of ZF-Inf. This is worked out in loving detail in Chapter 1 of "Metamathematics of First Order Arithmetic" by Hajek and Pudlak. In fact the authors carry this out not just for PA but for the subtheory $\text{I}\Sigma_0(\text{exp})$.

(Added) I expect expected that every model $M$ of ZF-Inf arises would arise in this way, by applying the above construction to the model of PA consisting of the ordinals of $M$. But it seems this is not so... See Ali's answer below.

2 added 46 characters in body

Any positive integer can be written uniquely as a sum of distinct powers of 2. PA knows this, in the sense that one can write down a formula $\phi(x,y)$ meaning in the standard model that the $x$-th bit in the binary expansion of $y$ is 1. Moreover we can construct $\phi$ so that PA will prove all the expected facts about the $x$-th bit in the binary expansion of $y$.

If $M$ is any model of PA, then by taking $\phi(x,y)$ as the membership relation "$x\in y$" we get a model of ZF-Inf. This is worked out in loving detail in Chapter 1 of "Metamathematics of First Order Arithmetic" by Hajek and Pudlak. In fact the authors carry this out not just for PA but for the subtheory $\text{I}\Sigma_0(\text{exp})$. Therefore, insofar as one "knows" what a

(Added) I expect that every model $M$ of PA looks likeZF-Inf arises in this way, one also knows what a by applying the above construction to the model of ZF-Inf looks like.PA consisting of the ordinals of $M$.

1