If set-intersection corresponds to conjunction, set-union corresponds to disjunction, does the power set have something it corresponds to? I was reading Susanna Epp's Discrete Mathematics with Applications 3rd Edition and then she started talking about Boolean Algebras at page 289 and I feel I sort of understand it, but not really? which is why I am going to ask this question.
Also I know I'm probably using "corresponds" in the not-correct way or something... like there's an official meaning? Uh, to explain that, I mean that it acts on sets in the same way as whatever its analog is acts on statement forms...?
also, if I am correct, does set-inclusion correspond to implication, and set-equality to the biconditional? otherwise, please let me know if there are... things that you know about that I don't where you can see I have the wrong... kind of understanding.
 A: Yes there is! Fix some set $X$ and let $\mathbb{B} := \{ \mathsf{true}, \mathsf{false} \}$, then every subset $A \in \mathcal{P}(X)$ can be put into correspondence with a function, namely $f_A : X \rightarrow \mathbb{B}$ which has to satisfy $f_A (x) = \mathsf{true} \Leftrightarrow x \in A$. This gives us a function
$$
 F : \mathcal{P}(X) \rightarrow \mathbb{B}^X ~~~;~~~F(A)
:= f_A
$$
which has an inverse
$G : \mathbb{B}^X \rightarrow \mathcal{P}(X)$ defined by
$G(f) := \{ x \in X \mid f(x) = \mathsf{true} \}$.
So we essentially have that $\mathcal{P}(X) \equiv \mathbb{B}^X$ i.e. it corresponds to the set of functions $X \rightarrow \mathbb{B}$ and that arrow there does look oddly familiar to implication, doesn't it?
And I am not making anything up here. This is an important observation that lays at the foundation of

*

*some things in logic; where implication is sometimes actually defined as a function between propositions. The tl;dr is that you can think of a proof for $A \rightarrow B$ as a construction of a function $A \rightarrow B$. (Here is another answer of mine with more on this)

*Concepts such as the subobject classifier in category theory. Here, the idea is that we can replace the set of booleans $\mathbb{B}$ in the above by some other suitable object $\Omega$ to give a more general notion of subsets. These are called subobjects and are now morphisms $X \rightarrow \Omega$ pretty much by definition.

A: "Set intersection corresponds to conjunction" can be made precise as follows: For any one-place properties $P_0$, $P_1$, and $P_2$ and sets $S_0$, $S_1$, and $S_2$ such that $P_i$ has extension $S_i$, $S_2 = S_0 \cap S_1$ if and only if $\forall x, P_2(x) \leftrightarrow P_0(x) \land P_1(x)$; and similarly for union and disjunction.
In the same way, as you suggest, "$S_1 \subset S_0$" corresponds to "$\forall x, P_1(x) \rightarrow P_0(x)$".  Then, for any one-place properties $P_0$ and $P_1$ with extensions $S_0$ and $S_1$, $S_1 \in \mathcal{P}(S_0)$ if and only if $\forall x, P_1(x) \rightarrow P_0(x)$.  This is a correspondence between a set-theoretic and a logical statement, but not the same kind of correspondence as the earlier ones, since the set-theoretic statement is "$S_1 \in \mathcal{P}(S_0)$" not "$S_1 = \mathcal{P}(S_0)$".
You could also say that $\mathcal{P}(S_0)$ corresponds to the class of one-place properties $P$ such that $\forall x, P(x) \rightarrow P_0(x)$.  Again, this is not the same kind of correspondence as the earlier ones.
To get a correspondence of the earlier kind, you have to allow quantification over properties.  Then you might be able to say something like "'$S_1 = \mathcal{P}(S_0)$' corresponds to '$\forall P, P_1(P) \leftrightarrow (\forall x, P(x) \rightarrow P_0(x))$'".  You probably shouldn't try saying anything like that though unless you've gone deeper into logic than Epps will take you (and certainly deeper than I've gone).
More broadly, the case of power sets is different from that of conjunction and disjunction because it involves explicitly forming a set of sets; but whereas forming sets of sets is possible in the simplest forms of set theory, forming properties of properties is not possible in the simplest forms of mathematical logic.
