I am confirming whether my proof is correct or not and need help. If $ A \subseteq 2^A , $ then $ 2^A \subseteq 2^{2^A} $


Given: $ \forall x ($ $ x\in A \rightarrow \exists S $ where $ S \in 2^A \wedge x \in S )$ --($0$)

Goal: $ \forall S \forall x ( $ $ S\in 2^A \wedge x \in S \rightarrow \exists F $ such that $F \in 2^{2^A} \wedge \exists S' $ such that $ S' \in$ $F \wedge x \in S')$

$ \forall S \forall x \text { }S \in 2 ^A \wedge x \in S $ adding to the given. -(1)

New Goal: $\exists F $ such that $F \in 2^{2^A} \wedge \exists S' $ such that $ S' \in$ $F \wedge x \in S' $

By universal instantiation (1) , $ A \in 2 ^A \wedge x \in A $

From the above step we have $x \in A$, Hence,

By existential instantiation ($0$) , $ A \in 2 ^A \wedge x \in A $

Now I am taking negation of the new goal. (Proof by contradiction)

$\exists F \text { such that } F \in 2^{2^A} \rightarrow \exists S ' \text { such that } S' \in F \rightarrow x \not \in S' $ --($2$)

By existential instantiation of $F$ and $S'$ in ($2$) $F_0 \in 2^{2^A} \rightarrow A \in F_0 \rightarrow x \not\in A $

S' should be A.

How would I prove that $F_0 \in 2^{2^A}$

PS: Guidance using rule of inference is much appreciated.

  • $\begingroup$ Are you actually required to cite the specific rules of inference that you’re using? The proof itself in more readable form takes only about two lines. $\endgroup$ May 2, 2015 at 18:53
  • $\begingroup$ No. just two lines? $\endgroup$
    – Badri
    May 2, 2015 at 18:55
  • $\begingroup$ See the answer that I just posted. But note that I omitted most of the business about goals and all of the technical logical terminology. $\endgroup$ May 2, 2015 at 18:56
  • $\begingroup$ Now I am curious, how would you prove it logically $\endgroup$
    – Badri
    May 2, 2015 at 18:58
  • $\begingroup$ I wouldn’t. :-) Seriously, it would depend on the specific logical formalism that I was using, and it’s hard to think of a context other than an exercise or working in an unusual system in which there would be any reason to do such a thing. I don’t know exactly what system you’re working in, so I’m not at all sure that I can make the translation into it. $\endgroup$ May 2, 2015 at 19:01

2 Answers 2


Here’s how I would write up a proof of this result.

Suppose that $X\in 2^A$; I need to show that $X\in 2^{2^A}$. Since $X\in 2^A$, I know that $X\subseteq A$. Let $x\in X$; then $x\in A\subseteq 2^A$, so $x\in 2^A$. Thus, $X\subseteq 2^A$, and hence by definition $X\in 2^{2^A}$.

In your argument I would first, for the sake of clarity, say that the initial goal is to show that for each $S\in 2^A$, $S\in 2^{2^A}$. This translates to showing that for each $S\in 2^A$, $S\subseteq 2^A$, or

$$\forall S\,\forall x\Big(S\in 2^A\land x\in S\to x\in 2^A\Big)\;.$$

Use univeral instantiation to get $S\in 2^A\land x\in S$. Your goal now is to show that $x\in 2^A$, which can be rewritten as $x\subseteq A$, or

$$\forall y\Big(y\in x\to y\in A\Big)\;.\tag{1}$$

Universal instantiation lets you write $y\in x$. From $S\in 2^A$ we get $\forall z(z\in S\to z\in A)$ which, when combined with $x\in S$, yields $x\in A$. Now recall that we were given $A\subseteq 2^A$, i.e., $\forall z(z\in A\to z\in 2^A)$, and we have $x\in A$, so $x\in 2^A$, which is essentially the new goal $(1)$.

Not being familiar with the specific system of inference that you’re using, I’ve left a lot of the logical details to you, but perhaps this is enough of a semi-formal expansion to point you in the right direction.


Here is how I would write down this proof, in a way which makes clear the inherent symmetry. (Ignore the red coloring for now, I will use that below.)$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\followsfrom}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}} \newcommand{\P}[1]{2^{#1}} $

For every $\;X\;$, we have $$\calc X \in \P{A} \op\equiv\hint{definition $\ref 0$ of $\;\P{\cdots}\;$} X \subseteq A \op\then\hint{using assumption $\;A \subseteq \color{red}{\P{A}}\;$, since $\;\subseteq\;$ is transitive $\ref 1$} X \subseteq \color{red}{\P{A}} \op\equiv\hint{definition $\ref 0$ of $\;\P{\cdots}\;$} X \in \P{\color{red}{\P{A}}} \endcalc$$ By the definition of $\;\subseteq\;$, this proves that $\;\P{A} \subseteq \P{\color{red}{\P{A}}}\;$.

Above I used the definition of $\;\P{\cdots}\;$ in the following form: for all $\;X\;$ and $\;A\;$ we have $$ \tag 0 X \in \P{A} \;\equiv\; X \subseteq A $$ And transitivity of $\;\subseteq\;$ is just $$ \tag 1 A \subseteq B \;\land\; B \subseteq C \;\then\; A \subseteq C $$ for all $\;A,B,C\;$.

The nice thing is that the above proof does not use the internal structure of the right hand side $\;\color{red}{\P{A}}\;$. Therefore we can replace it with $\;\color{red}{B}\;$ throughout, resulting in a proof of the following more general theorem: $$ \tag 2 A \subseteq \color{red}{B} \;\color{green}{\then}\; \P{A} \subseteq \P{\color{red}{B}} $$ Finally, note that we also can prove the even stronger $$ \tag 3 A \subseteq B \;\color{green}{\equiv}\; \P{A} \subseteq \P{B} $$ but let me leave that as an exercise for the reader.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .