(KK)If one knows that p, then one knows that one knows that p.

Definitions
A0is the proposition that 1+1=2.
A1is the proposition that Emil knows that 1+1=2.
A2is the proposition that Emil knows that Emil knows that 1+1=2.

Anis the proposition that Emil knows that Emil knows that … that 1+1=2.
Where “…” is filled by “that Emil knows” repeated the number of times in the subscript of A.

Argument
1. Assumption for RAA
(∀P∀x)Kx(P)→Kx(Kx(P)))
For any proposition, P, and any person, x, if x knows that P, then x knows that x knows that P.

2. Premise
Ke(A0)
Emil knows that A0.

3. Premise
(∃S1)(A0S1A1S1…∧AnS1)∧|S1|=∞∧S1=SA
There is a set, S1, such that A0belongs to S1, and A1belongs to S1, and … and Anbelongs to S1, and the cardinality of S1is infinite, and S1is identicla to SA.

4. Inference from (1), (2), and (3)
(∀P)P∈SAKe(P)
For any proposition, P, if P belongs to SA, then Emil knows that P.

5. Premise
¬(∀P)P∈SAKe(P)
It is not the case that, for any proposition, P, if P belongs to SA, then Emil knows that P.

6. Inference from (1-5), RAA
¬(∀P∀x)Kx(P)→Kx(Kx(P)))
It is not the case that, for any proposition, P, and any person, x, if x knows that P, then x knows that x knows that P.

Proving it
Proving that it is valid formally is sort of difficult as it requires a system with set theory, predicate logic with quantification over propositions. The above sketch should be enough for whoever doubts the formal validity.