Is the liar's paradox the principle of explosion in disguise? Sorry for a high-school-level question, but something is bugging me about the liar's paradox.
The liar's paradox can be formally written as an axiomatic system with an axiom $P \equiv \lnot P$. Due to the equivalence, we must have

*

*$P \iff \lnot P$,

*which is the same as $(P \implies \lnot P) \land (\lnot P \implies P)$

*which is the same as $(\lnot P \land \lnot P) \land (P \land P)$

*which is the same as $\lnot P \land P$
And now, due to the principle of explosion, we can prove any statement. In particular, we can prove $P$, and we can prove $\lnot P$.
What I want to say is that, according to my understanding, the liar's paradox is the paradox in exactly the same sense as an axiomatic system with an axiom False (i.e. a trivially contradictory axiomatic system), where for any statement $P'$, we can prove that $P'$ is true and $P'$ is false.
My understanding of the "philosophical" meaning of the liar's paradox is that it shows an example of a statement $P$ that can't be assigned a "True" or "False" value since it would lead to a contradiction. However, as I show above, the contradiction is already there: it has nothing to do with the value of $P$, in exactly the same sense as in the trivially contradictory axiomatic system, a truth value of any new statement $P'$ doesn't affect the contradiction.
So, the only thing that the liar's paradox achieves is a construction of a contradictory axiomatic system. However, this is already achieved in a less obfuscated manner by the trivially contradictory axiomatic system.
Is the above understanding correct? Or did I do something wrong in the above derivation? Or did I misunderstand the motivation behind the paradox?
 A: As blargoner says in the comments, thinking about the liar's paradox this way misses the real heart of it. The liar's paradox is about a statement $P$ which itself asserts that $P$ is false; in your rendition the assertion $P \equiv \neg P$ is made "outside of $P$." Said another way, you can introduce the assertion $P \equiv \neg P$ into an arbitrary set of axioms, but in order to state the liar's paradoxical sentence you need a set of axioms which is powerful enough to discuss its own propositions and their truth values.
What the liar's paradox implies in broad strokes is that there is no such set of axioms; in other words, we do not have an unlimited capacity for self-reference in logic. Other results in logic can be thought of as precise versions of this, most famously the incompleteness theorem but also Tarski's undefinability theorem. The Berry paradox is a similar paradox about the limits of self-reference and a personal favorite of mine.
Edit: To say everything a bit more explicitly, motivated by the discussion in the SEP article, one way to somewhat formalize the liar's paradox is that it implies a formal logic cannot simultaneously have all of the following ingredients:

*

*The law of excluded middle; every proposition is either true or false (not neither, not both).

*The ability to refer to its own propositions; if $P$ is a proposition, write $\ulcorner P \urcorner$ for its "name" in the formal logic.

*A truth predicate $\text{true}(\ulcorner P \urcorner)$ which takes as input the name of a proposition and returns as output its truth value.

*The ability for propositions to refer to themselves.

Given all four ingredients we can construct the liar's paradoxical sentence $P$ which asserts $\neg \text{true}(\ulcorner P \urcorner)$ but which cannot be either true or false. So there are (at least) four different ways to resolve the liar's paradox: throw out LEM, throw out the ability to refer to propositions, throw out the truth predicate, or throw out self-reference specifically. (Although, as the SEP article explains, there are variants of the liar's paradox showing that self-reference specifically is not necessary.)
First-order Peano arithmetic satisfies LEM, is capable of referring to its own propositions and is capable of constructing self-referential propositions (via the diagonal lemma); this is used crucially in the proof of the incompleteness theorem, for example. It resolves the liar's paradox by containing no truth predicate (this is Tarski's undefinability theorem).
Other ways of resolving the liar's paradox throw something else out; for example you could try to throw out LEM. See the SEP article, specifically the section on paracomplete and paraconsistent logics for more. It seems that a lot of work here has been motivated by the desire to not throw out the truth predicate:

Working in classical logic, Tarski (1935) famously concluded from the Liar paradox that a language cannot define its own truth predicate. More generally, he took the lesson of the Liar to be that languages cannot express the full range of semantic concepts that describe their own workings. One of the main goals of the non-classical approaches to the Liar we have surveyed here is to avoid this conclusion, which many have seen as far too drastic. However, how successful these approaches have been in this regard remains a highly contentious issue.

