Fitch's paradox of Knowability I interpret your axioms as follows:
1. x --> ◊K(x) (All truths are knowable ie. it is possible that somebody knows x at some time.) (axiom)
2. P (Proposition P is a truth) (axiom)
3.a) ~K(P) (P is unknown) (axiom)
3.b) Q:=~K(P) (definition of Q)
4. ◊K(Q) (Theorem from 1. and 3.)
5. K(Q) (Q is known) (axiom)
6. Theorem: K(P) (P is known)
Can you please clarify the proof of that theorem using this formal language? I don't think these axioms are enough to prove statement 6. Maybe your logic differs from this. In fact (6.) is not a theorem of the above system.
As long as I understand your premises are stronger than that of Fitch's paradox in existential terms.
While Fitch's paradox only assumes P and Q; you assume K(Q) also.
So first I don't see how we can prove 6. and even if we can get a contradiction from your axioms they may be stronger than the axioms of Fitch's paradox.
To be honest I don't really understand the paradox explained here:
https://plato.stanford.edu/entries/fitch-paradox/#ParKno
At (6) they get a contradiction and from that we can prove every statement (can't we?)
But they keep proving for 5 more steps for no apparent reason.