Writing the power set of a power set in logic notation I'm new to set theory and math proofs, but I enjoy converting stuff into primitive notation i.e. with only the membership predicate. I’m familiar with basic logic. But am confused about something; namely what happens when we treat propositions as individuals. (Can we? ) i.e. ‘Mary believes that ‘Joe is happy’’, where we might denote it as ‘Bm(Hj). (Is that legitimate?)
what if we want to write $\mathcal{P}\left(\mathcal{P}(A)\right)$?
I’m lost when trying to translate it;
I start with
$$\exists \mathcal{P}(A) \forall x \forall y \left[y \in x \implies x \in A \iff x \in \mathcal{P}(A)\right]$$
but am unsure where to go from there. A power set is contained within a power set and I don't know how to handle that.
 A: There is a formula $\varphi(x,y)$ that holds iff $x=\mathcal P(y)$. 
Any statement involving a power set, say $\psi(\mathcal P(t))$, can be rewritten by saying $\forall z\,(\varphi(z,t)\to\psi(z))$ or, equivalently, $\exists z\,(\varphi(z,t)\land\psi(z))$. You can iterate this, so any statement $\psi$ involving $\mathcal P(\mathcal P(t))$ can be expressed by saying that for any $x$ and $y$, if $x=\mathcal P(y)$ and $y=\mathcal P(t)$, then $\psi$ holds of $x$ (or that there are $x$ and $y$ such that ...). 
[One can do similarly with statements involving $\mathcal P^n(x)$ for a fixed $n$. If we have a statement where $n$ itself changes, then some additional work is required. But the solution is similar: We would state that there is a sequence of length $n+1$, and each term is the power set of the previous one, and the first term is $x$, and the $(n+1)$-st has whatever property it is we actually wanted to discuss. Or, if we prefer, we could say that for any sequence of length $n+1$ such that its first term is $x$ and each term is the power set of the previous one, the $(n+1)$-term has the desired property.]
Beyond this, which of the two statement one means (the universal or the existential one) is pretty much a matter of taste. Naturally, this can only be done with an unambiguous outcome in a theory powerful enough to establish existence and uniqueness of power sets. (That the outcome is unambiguous means that the two statements, the universal and the existential one, are provably equivalent.)
A: To answer only the part about the double power set, you're not going to have a lot of luck translating $\mathcal{P}(\mathcal{P}(A))$ into a primitive FOL formula because it's a term and not a formula. If you wanted to translate something like $x\in\mathcal{P}(\mathcal{P}(A))$, just take it one step at a time. It expands to $x\in\{y:y\subseteq\mathcal{P}(A)\}$, which expands to $\exists z(x\in z\wedge\forall y(y\in z\Leftrightarrow y\subseteq\mathcal{P}(A)))$, etc. There's nothing special going on in a double power set.
As for the first part, in FOL predicates of a language are not terms of the language, so predicating things of them is gibberish. I'm sure you can design some formalism to let you do something like that, but it would be something beyond standard logic.
