I was working with Dr. S.P Suresh at CMI on introductory automata theory during the summer of 2018 when I first came across Kleene Algebras. I had not done any abstract algebra then and this topic was way too abstract for me to make much sense of it. After completing a course on Group Theory the following semester, I went back to this topic and proved most of the results that were left as exercises in the book I was following - “Automata and Computability” by D.C Kozen. While I was working on this, I discovered that the axioms that were used to define a Kleene Algebra were not independent - I was able to derive one of the axioms that involved the Kleene star operator from the others. I later found out that Kozen was the first one to axiomatize Kleene Algebras in his 1996 paper in which he mentions “No attempt has been made to reduce the axioms above to a minimal set and no claim is made as to their independence”. I have, however, not done any further literature survey to see if my result is already known. It seems too trivial to not have been discovered already, to be honest.
The small manuscript linked below has the proof of my claim. If you find any typos, mistakes or just want to talk about this topic, email me!