How to formally define this language of hereditarily finite sets?

Question

Suppose we have an alphabet of three characters, which are the left brace, the right brace, and the comma. I want to define a language over this alphabet which corresponds to the hereditarily finite sets. So, for example, the word $\{\}$ would be in the language, and it corresponds to the empty set. Also, the word $\{\{\},\{\}\}$ would be in the language, and it corresponds to the singleton containing the empty set. As you can see, I allow duplications of sets in my language. That is, every word in my language corresponds to a hereditarily finite set, but this correspondence is not injective. Also, the commas are essential in my language, so something like $\{\{\} \{\}\}$ would not be in my language. What is the formal definition of my intuitive notion of this language?

Answer 1

You can define a formal grammar for your language simply as $$S\to \{\}\ |\ \{L\}\\ L\to S\ |\ \{L,\,S\}$$ where $S$ represents your hereditary finite lists and $L$ represents the list contents.