From what I gather from your question, your "natural formulas" would form a complete set of distinct representatives for definable subsets of N under the equivalence relation $X \mathrel{E}_0 Y$ defined by $|(X \setminus Y) \cup (Y \setminus X)| < \aleph_0$. Unfortunately, there is no simple way to do this; such a system of distinct representatives necessarily has very high complexity. In fact, finding a system of distinct representative for $E_0$ over all subsets of N is precisely the same as Vitali's construction of a non-measurable set!

In your phrasing, you talk about formulas rather than the sets they define, but this is not much different (the difference is known as "lightface vs boldface" in the literature). Problems of this type are extensively studied in Descriptive Set Theory, under the heading of Borel Equivalence Relations. The relation $E_0$ is in a very precise sense the simplest Borel equivalence for which has no simple system of distinct representatives, it thus plays a very important role in this theory.

A good place to get started with Descriptive Set Theory is Kechris' Classical Descriptive Set Theory. For your particular problem, you want to look at the "lightface theory," for which the standard reference is Moschovakis' Descriptive Set Theory. There are a few good surveys and books on Borel equivalence relations, but most require a fair amount of familiarity with the subject.

From what I gather from your question, your "natural formulas" would form a complete set of distinct representatives for definable subsets of N under the equivalence relation $X \mathrel{E}_0 Y$ defined by $|(X \setminus Y) \cup (Y \setminus X)| < \aleph_0$. Unfortunately, there is no simple way to do this; such a system of distinct representatives necessarily has very high complexity. In fact, finding a system of distinct representative for $E_0$ over all subsets of N is precisely the same complexity as Vitali's construction of a non-measurable set!

In your question, you talk about formulas rather than the sets they define, but this is not much different (the difference is known as "lightface vs boldface" in the literature). Problems of this type are extensively studied in Descriptive Set Theory, under the heading of Borel Equivalence Relations. The relation $E_0$ is in a very precise sense the simplest Borel equivalence for which has no simple system of distinct representatives, it thus plays a very important role in this theory.

A good place to get started with Descriptive Set Theory is Kechris's Classical Descriptive Set Theory. For your particular problem, you want to look at the "lightface theory," for which the standard reference is Moschovakis's Descriptive Set Theory. There are a few good surveys and books on Borel equivalence relations, but most require a fair amount of familiarity with the subject.