The security level of double encryption Let PKE $\Pi' = (Gen', Enc', Dec')$ and it is secure in the sense of $S'$.
Let PKE $\Pi'' = (Gen'', Enc'', Dec'')$ and it is secure in the sense of $S''$.
$S'$ and $S''$ may be separation which means that $S' \not\Rightarrow S''$ and $S'' \not\Rightarrow S'$. For example, $S' = \text{IND-CCA}, S'' = \text{NM-CPA}$ or $S' = \text{OW-CCA}, S'' = \text{IND-CPA}$.
Let $\Pi = (Gen, Enc, Dec)$ be the double encryption such that
$Gen(1^\lambda) = (pk, sk)$

$(pk', sk') \gets Gen'(1^\lambda)$ and $(pk'', sk'') \gets Gen''(1^\lambda)$.

$pk = pk' \Vert pk ''$ and $sk = sk' \Vert sk''$.


$Enc_{pk}(m) = c$

$(pk' , pk'') \gets pk$

$c \gets Enc'_{pk'}( Enc''_{pk''}(m)) $.


$Dec_{sk}(c) = m$

$(sk' , sk'') \gets sk$

$c \gets Dec''_{sk''}( Dec'_{sk'}(m))$.


Is $\Pi$ secure both in the sense of $S'$ and $S''$?
In my opinion, it is true.

We define the CPA game of $\Pi$ against an adversary $A = (A_{1}, A_{2})$ as follows:

$(pk, sk) \gets Gen(1^\lambda)$
$(m_{0}, m_{1}, s) \gets A_{1}(pk)$
$b \leftarrow \{\, 0,1 \,\}$ and $c \gets Enc_{pk}(m_{b})$.
$d \gets A_{2}(c, s)$.

We say $A$ wins if $b = d$, and $\Pi$ is IND-CPA secure if $A$ has at most negligible advantage.

For example, if $S'' = \text{IND-CPA}$, assume there exists an adversary $A$ with non-negligible advantage against $\Pi$. Then we construct an adversary $A''$ against $\Pi''$ as follows:
$A''_{1}(pk'') = (m_{0}, m_{1}, s)$:

$(pk', sk') \gets Gen'(1^\lambda)$.

$pk = pk' \Vert pk''$.

$(m_{0}, m_{1}, s) \gets A(pk)$.


$A''_{2}(c, s) = d$:

$c' \leftarrow Enc'_{pk'}(c)$

$d \gets A(c', s)$.


We say that $A''$ wins the CPA game against $\Pi''$ if and only if $A$ would have won the corresponding game against $\Pi$. Thus $\Pi''$ is IND-CPA secure implies that $\Pi$ is IND-CPA secure.
If $S' = \text{IND-CPA}$, assume there exists an adversary $A$ with non-negligible advantage against $\Pi$. Then we construct an adversary $A'$ against $\Pi'$ as follows:
$A'_{1}(pk') = (m_{0}, m_{1}, s)$:

$(pk'', sk'') \gets Gen''(1^\lambda)$.

$pk = pk' \Vert pk''$.

$(m'_{0}, m'_{1}, s) \gets A(pk)$.

$m_{0} \gets Enc''_{pk''}(m'_{0})$ and $m_{1} \gets Enc''_{pk''}(m'_{1})$


$A'_{2}(c, s) = d$:

$d \gets A(c, s)$.

We say that $A'$ wins the CPA game against $\Pi'$ if and only if $A$ would have won the corresponding game against $\Pi$. Thus $\Pi'$ is IND-CPA secure implies
that $\Pi$ is IND-CPA secure.
Am I right? So I conclude that $\Pi$ is a little stronger than $\Pi'$ and $\Pi''$. If it is true, why is there no double public-key encryption scheme?
Am I right?


Yes, with double encryption, if both are functionally correct and at least one is CPA-secure, then the composition is CPA-secure.


  If it is true, why is there no double public-key encryption scheme?


Because you took a scheme that can be reasonably classified to be "unbreakable" and then combined it with an other "unbreakable" one, you have constructed an "unbreakable" one that takes more time to compute than a single "unbreakable" one. There's no practical advantage to such combinators if we're confident in the security of the scheme we're using. If we're not confident either we pick a better one - or if we have also no faith in the better one we do indeed use such combinators. If you want a recent example of this, look no further than the hybrid ECDH / PQ-Crypto key exchanges that are being tested where we don't have faith in the PQ-Crypto yet so use ECDH to secure it against classical adversaries.


  Is $\Pi$ secure both in the sense of $S'$ and $S''$?


To prove this I suggest a simpler approach of checking whether $\pi\circ\operatorname{Enc}\circ\pi'$ is $S'$-secure assuming $\operatorname{Enc}$ is $S'$-secure (coming up with the correct decryption is left as an exercise to the reader) and $\pi,\pi'$ are any permuations applied to the input and the output.