"Only if" in the set of proposition definition In my mathematical logic book, the language of propositional logic and the set of well formed formulas are defined with the following definitions:
Language of propositional logic

The language of propositional logic has an alphabet consisting of
  
  
*
  
*proposition symbols: $p_0, p_1, p_2, \ldots$,
  
*connectives: $\land, \lor, \to, \neg, \leftrightarrow, \bot$, 
  
*auxiliary symbols: $(, )$.
  
  
  The proposition symbols and $\bot$ stand for the indecomposable
  propositions, which we call atoms or atomic propositions.

Set of proposition

The set $\mathit{PROP}$ of proposition is the smallest set $X$ with
  the properties
  
  
*
  
*$p_i \in X \, (i \in \mathbb{N})$, $\bot \in X$,
  
*$\varphi, \psi \in X \implies (\varphi\:\square\:\psi) \in X$ where $\square$ is a connective,
  
*$\varphi \in X \implies (\neg \varphi) \in X$.
  

I was wondering if in the second and in the third properties of the last definition the only if implication holds, i.e., would it be correct conclude that


*$\varphi, \psi \in X \iff(\varphi\:\square\:\psi) \in X$ where $\square$ is a connective and

*$\varphi \in X \iff(\neg \varphi) \in X$


from the definitions above? The last case would be trivial by exploiting the semantics of $\neg$ connective, but we are still on a syntactic level where the semantics of connectives is not defined yet.

Question that could be related: Are "if" and "iff" interchangeable in definitions?
I'm aware that definition expresses an "is" relationship, not an "is equivalent to" relationship (see Carl Mummert answer), but in this case the set of proposition is already defined in the term of an "is" relationship: The set $\mathit{PROP}$ of proposition is...
 A: Yes, it is the case that, following the definition in the post, $\phi, \psi \in \text{PROP}$ if and only if $(\phi \mathbin{\Box} \psi) \in \text{PROP}$. That is, PROP satisfies the converses of clauses 2 and 3 in the definition. 
This takes proof, however, and is not a very trivial consequence of the way the definition is phrased. One proof is at the end of this post.  The key point is that $\text{PROP}$ is defined to be the smallest set which satisfies the three clauses of the definition.
(Note that we cannot talk about "$X$" outside the definition, because there is a quantifier in the definition over $X$. PROP is just one set of the many sets that satisfy the three clauses. So the part of the question after the definition should say PROP rather than $X$.)
There are other sets which strictly contain PROP and for which the converses of 2 and 3 do not hold.  For example, we could begin with $\text{PROP} \cup \{\Box\Box\Box\}$ and then add any more elements necessary for the resulting set to satisfy clauses 2 and 3 of the definition. The resulting set will contain all of PROP along with more, and will not satisfy the converse of clause 2.
So the key to understanding PROP is not just that it satisfies the three clauses, but also that an expression is in PROP only if that expression must be in PROP (in a certain sense) in order to satisfy the three clauses. 
The reason for not including the "if and only if" in the three clauses is that it makes the three clauses easier to work with, in actual proofs, if they are just implications rather than bi-implications. 
Finally, to prove that the equivalences hold in PROP, let $Y$ be any set which satisfies the three clauses. Then let $Z$ be the collection of elements $\rho$ in $Y$ such that:


*

*$\rho$ is of the form $p_i$ or $\bot$, or

*$\rho$ is of the form $(\phi \mathbin{\Box} \psi)$ where $\phi, \psi \in Y$, or

*$\rho$ is of the form $(\lnot \phi)$ where $\phi \in Y$.


Then $Z$ also satisfies all three clauses, as you can check. If we apply this argument with $Y = \text{PROP}$ we end up with a set $Z \subseteq PROP$ satisfying the three clauses. Because PROP is the smallest set satisfying the three clauses, this means $Z = \text{PROP}$. But then, by the definition of $Z$, we see that PROP satisfies the converse of clauses 2 and 3, as desired. 
A: 
$\varphi \in X \iff(\neg \varphi) \in X$ …
  The last case would be trivial by exploiting the semantics of $\lnot$
  connective, but we are still on a syntactic level where the semantics
  of connectives is not defined yet.

You are right. $\varphi$ is a list of symbols, and its semantics, however defined, is not relevant.

Question that could be related: Are "if" and "iff" interchangeable in
  definitions?

I doubt that it is related. The definition of the set PROP is an inductive definition, a special kind of definitions, and $\implies$ here is a usual implication, not an “iff”. The facts you are asking about follow from the remark “the smallest set”, but their proof is not at all obvious. I suggest that you learn about inductive definitions. I will prove a part of the facts you are asking about; it will be just an application of the principle of induction to your case. Other facts are proved similarly. In what follows, $X=\mathrm{PROP}$ .
Theorem. For every list of symbols $\varphi$, if $\lnot\varphi\in X$, then $\varphi\in X$.
Proof. Let $Y$ be the set of all lists of symbols $\varphi$ such that $\varphi\in X$ and if $\varphi$ has form $\lnot\psi$, then $\psi\in X$. $Y$ has the properties described in the definition of PROP because:


*

*For all $i \in \mathbb{N}$, $p_i\in Y$ because $p_i\in X$ and $p_i$ does not have form $\lnot\psi$. $\bot\in Y$ because $\bot\in X$ and $\bot$ does not have form $\lnot\psi$.

*If $\varphi \in Y$ and $\psi \in Y$, $(\varphi\:\square\:\psi) \in Y$ because $(\varphi\:\square\:\psi) \in X$ (because $\varphi\in X$ and $\psi \in X$) and $\varphi\:\square\:\psi$ does not have form $\lnot\alpha$.

*If $\varphi \in Y$, the $(\neg \varphi) \in Y$ because $(\neg \varphi) \in X$ and $\varphi\in X$.
As $X$ is the smallest set with these properties, $X\subseteq Y$. Hence for every $\varphi\in X$, if $\varphi$ has form $\lnot\psi$, then $\psi\in X$. $\square$
