Bloviatius
Bloviatius, the bloviator.
By necessitation, it follows that K (p ∧ ¬Kp) is necessarily false. Depending on the paraconsistent logic, the paraconsistist may object to use of reductio, or may object to other inferences. The claim that K (p ∧ ¬Kp) is impossible (at line 9) is inferred from this claim that K (p ∧ ¬Kp) is necessarily false.
I really hope you don't always talk like that.