How to define a recursively defined set properly? We can define sets recursively. For example we can say 
$x\in S\iff x=1 \vee \exists y\in S: y+2=x$
But how can we write $S$ ?
I.e. how can we describe $S$ in a way we are normaly used to describe a set. I.e. extensionaly or intensionaly?
In the form $S=\{x\in\mathbb{N}|\phi(x)\}$ (intensionaly)? Because I think that that recursively defining a set S implies a intensional definition of a subset of the superset of $S$ (The subset is $S$) in this case it is $\mathbb{N}$.
(Reasonably the set can also be written extensionally $S=\{1,3,5,....\}$ but this is not the point of my question I am interested in the implicit  intensional definition given by the recursion)
I have made a previous example with propositional formulas in a language, 
A language consists of an ALPHABET and a GRAMMAR.
An alphabet $\mathcal{A}$ is a union of three different sets, we will call the element of an alphabet symbols. The first set are the symbols for the propositional variables like $A,B,C....$, the second set is the set of logical symbols $T,F,\wedge,\vee,\implies,\iff$ and the third set are non-logical symbols like $(,)$
The set of all propositional formulas  is similair to the set $S$ above because there are some initial elements and some elements we can derive from the initial elements recursively. 

Let $\mathcal{F}$ be the set of all propositional formulas. We want
  to define this set in such a way if we take a element from
  it:$\phi\in\mathcal{F}$ then we want to say that this is equivalent
  to the desired statement: $\phi\in \{1\}\times V\vee \exists!
 \psi_1,\psi_2\in\mathcal{F},a\in\{\vee,\implies,\wedge,\iff\}: \phi=(a,\psi_1,\psi_2)$. $V$ is the set of all propositional variables
  we have defined extensionaly in beforehand: $V=\{A,B,C,D,E,...\}$.

For the sake of simplicity I have just looked at the set of binary operators but one can also do the same for other operators and also can use another symbols like $\{1,2,3,4\}$. The important thing is that we can distinguish in this case the triples from one another. I have simplified even further and assumed in the following that $\implies$ is the only logical operator we have to consider and which happens to be a binary logical operator.
$$\mathcal{F}=\bigcup_{n\in\mathbb{N_0}}T_n$$
$$T_0= \{1\}\times V\quad\text{and}\quad T_n=\bigcup_{(j,k)\in\{1,...,n-1\}^{2}}\{2\}\times T_{n-1}\times T_j\cup \{2\}\times T_k\times T_{n-1}$$

My question is first of all whether my definition of $\mathcal{F}$
  makes sense, i.e. whether I actually have defined all propositional
  formulas? 
Whether there is alternative that is so general that it does not make
  use of the natural numbers because this definition was motivated by
  someone elses answer to an old question of mine and I am not sure if
  his understanding of $\mathcal{F}$ matches my definition and
  unfortunately this person does not react to my comment anymore (link
  to the question:
  Induction over propositional formulas).
  And he seems to make no use of natural numbers. He explicitly said
  structural induction and not induction over the natural numbers. 
Whether taking an element from this defined set is equivalent to the
  desired statement and how I can prove it, especialy the uniqueness.
Finally I want to ask whether I can somehow derive a general
  definition of all inductively defined sets from this example.
  Because every inductively defined set in its nature has initial
  elements which could be described with a generl $T_0$ and some
  advanced elements which are in some $T_n$ and deduced from the initial
  elements.

 A: This isn't fully an answer to the question, since it doesn't address the OP's idea of using propositional logic, but I think it may still be useful to them and it's certainly too long for a comment.

What you're looking for is the general notion of definition by (possibly transfinite) recursion, and in particular of least fixed points of (monotone) operators on sets.


*

*Pet peeve: induction is a proof technique, recursion is a construction method. We prove by induction but build by recursion. 



A "definition" like  $$x\in S\iff x=1 \vee \exists y\in S: y+2=x$$ can be thought of as describing an operator $\mathcal{O}$ on sets of natural numbers given by $$\mathcal{O}(X)=X\cup\{1\}\cup\{a: \exists y\in X(y+2=x)\}.$$
Now the important thing to note is that $\mathcal{O}$ has fixed points - for example, $\mathcal{O}(\mathbb{N})=\mathbb{N}$. The idea of iterating $\mathcal{O}$ until some "completed" set appears corresponds to looking for the least fixed point of $\mathcal{O}$:

If $I$ is some "base set" and $\mathcal{O}:\mathcal{P}(I)\rightarrow\mathcal{P}(I)$ is some operator on subsets of $I$, the least fixed point of $\mathcal{O}$ is the unique (if it exists) set $S\subseteq I$ satisfying $(1)$ $\mathcal{O}(S)=S$ and $(2)$ for every $S'\subseteq I$ with $\mathcal{O}(S')=S'$ we have $S\subseteq S'$.

Not every operation on sets has fixed points at all: for example, consider the complement operation $\mathcal{C}: X\mapsto I\setminus X$ on any nonempty "base set" $I$. However, there are conditions which guarantee the existence of fixed points, and indeed least fixed points, the most common of which is monotonicity: $\mathcal{O}$ is monotonic iff $\mathcal{O}(X)\supseteq X$ for all $X\subseteq I$. Given a monotonic operator $\mathcal{O}$ we can "iterate it through the ordinals" as follows: $$A_0=\emptyset, \quad A_{\alpha+1}+\mathcal{O}(A_\alpha), \quad A_\lambda=\bigcup_{\alpha<\lambda}A_\alpha\mbox{ for $\lambda$ limit}.$$ Eventually this process stabilizes: there is some ordinal $\eta$ such that $A_\eta=A_\theta$ for all $\theta\ge\eta$. Using monotonicity we can prove that $A_\eta$ is indeed the least fixed point of $\mathcal{O}$.
Additional properties of $\mathcal{O}$ can make this process simpler. Some operations, for example, are finitely based - they satisfy $\mathcal{O}(X)=\bigcup_{F\subseteq X\mbox{ finite}}\mathcal{O}(F)$. Such an $\mathcal{O}$ (if also monotonic) stabilizes at level $\omega$, that is, we just need to iterate through the natural numbers. Bt in general larger ordinals may be needed, and it's a good exercise to construct an example of this.
