Principle of Explosion rejected by formalized semantic constraints
The principle of explosion (Latin: ex falso (sequitur) quodlibet (EFQ), “from falsehood, anything (follows)”, or ex contradictione (sequitur) quodlibet (ECQ), “from contradiction, anything (follows)”)

Here is the big mistake of the current mathematical understanding of provability that is derived from the principle of explosion:  
p = “I am going to the store”
q = “I am going to the store to buy groceries”
~p ⊢ q
The fact that I am not going to the store at all proves that I am going to the store to buy groceries.

Principle of explosion: ∀P∀Q: (P∧~P) ⊢ Q asserts that:
It logically follows that there exists a provability relation between every pair of totally unrelated expressions of language.

Since any expression of language can be conjoined to its negation thus forming the EFQ premise, therefore EFQ asserts that any other totally unrelated expression of language is proven on the basis of this totally unrelated premise.

Validity and Soundness
A deductive argument is said to be valid if and only if it takes a form that makes it impossible for the premises to be true and the conclusion nevertheless to be false. Otherwise, a deductive argument is said to be invalid.

The above definition of valid deduction (logical consequence) is insufficient in that it does not require a semantic connection between the premises and the conclusion. I show how this semantic connection can be formalized syntactically below.

A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of the preceding wfs in the sequence. Such a sequence is called a proof (or deduction) of C from Γ. The members of Γ are called the hypotheses or premisses of the proof. We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”…  (Mendelson 2015:28)

Semantic connection between the premises and the conclusion
This is formalized by requiring that all of the premises of the proof be included in the inference chain from the LHS of “⊢” to the RHS consequence, extraneous premises are not allowed. A formal proof can be constructed (all the inference steps shown) from the premises to the consequence with every premises required in at least one inference step.

Semantically relevant premises:
{“5 > 4”, “4 > 3”} ⊢ “5 > 3”

Specifying these semantically relevant inference steps:
“5 > 4”
“4 > 3”
∴ “5 > 3”

The above makes this evaluate to false: ∴ ∃P∃Q (P∧~P) ⊢ Q.
Thus certainly refuting this:  ∀P∀Q: (P∧~P) ⊢ Q   (Principle of explosion)

Mendelson, Elliott 2015
Introduction to Mathematical logic Sixth edition
1.4 An Axiom System for the Propositional Calculus page 28