Notation for well formed formulas I have two indexed families of sets $\{A_i\}_{i\in I}$ and $\{B_j\}_{j\in J}$ and want to describe all the formulas that can be formed with conjugations, disjunctions, negations, or implications using propositions of the form $A_p=A_q$ or $A_{r}\in B_s$ for arbitrary $p,q,r\in I$ and any $s\in J$. Or in a slight abuse of notation if I define a set of propositions by $P=\small\{(A_r\in B_s):(r,s)\in I\times J\}\cup \{(A_p=A_q):(p,q)\in I\times I\}$ then in equivalent terms I want to describe all the formulas formed in the following manner: All $p_1\in P$ are formulas I want, also if $p_2$ is one of these formulas then so is $\neg p_2$ and if $p_3$ is another one of these formulas then $p_1\land p_2$ and $p_1\lor p_2$ as well as $p_1\to p_2$ are formulas I want. Without diving into too much mathematical logic how could I best formally describe all these different propositions? To me it seems it would be something like "the well formed formulas over $P$" but I'm not sure and want to make sure that I am being clear here, as right now I'm not even sure the way I wrote $P$ is acceptable for I've never had to construct a set where the elements were logical statements like this.
 A: Begin by letting: $A = \{a_{1},a_{2},\dots, a_{i} \}$ and $B = \{b_{1},b_{2},\dots,b_{j} \}$.
Now define $
f_{=}(x,y)$ as the operation that returns the expression $(x = y)$
and $f_{\in}(x,y)$ as the operation which returns the expression ($x \in y$). Now we can specify the two sets you unioned to make $P$:
$$ 
{AA}^{=} = \{f_{=}(x,y)\mid x \in A \land y \in A\} 
\\
{AB}^{\ \in} = \{f_{\in}(x,y)\mid x ∈ A \land y \in B\}
$$
So we can write $P = {AA}^{=} \cup {AB}^{\ \in}$ and then all that is left to do is close $P$ under $\land, \lor, \lnot,$ and $\rightarrow$. We can do this by defining the operations by the following equations:
$$
\\
f_{\lor}(x,y)  = (x \lor y)
\\
f_{\land}(x,y)  = (x \land y)
\\
f_{\rightarrow}(x,y)  = (x \rightarrow y)
\\
f_{\lnot}(x)  = ( \lnot x )
$$
And defining $P^{*}$ to be the closure of $P$ under $f_{\lor}, f_{\land},f_{\rightarrow},$ and $f_{\lnot}$, meaning:


*

*$P \subseteq P^{*}$, and

*$\forall x,y \in P^{*} (f_{\lor}(x,y),f_{\land}(x,y),f_{\rightarrow}(x,y),f_{\lnot}(x)  \in P^{*})$

The only real subtle business comes in not confusing expressions with propositions; if we did not define $f_{\lor}, f_{\land},f_{\rightarrow},f_{\lnot}, f_{=},$ and $f_{\in}$ it would be a bit hand-wavey since, for example, $\land$ operates on propositions whereas $f_{\land}$ operates on expressions and we wouldn't want those to be used interchangeably. 
