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...
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:
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.