There are indeed many presentations of classical propositional logic1.
If complexity was measured purely in terms of number of axioms, then yes, Mendelson's axiom system would be more "economical". We could be even more "economical" with Meredith's system: $$((((A\to B)\to(\neg C\to\neg D))\to C)\to E)\to((E\to A)\to(D\to A))$$ Just rolls right off the tongue. While minimality is often a driver, people do still need to discover more minimal systems. (Indeed, the above is not the most minimal system if we include the complexity of the axiom and not just the number.) There's also the question of accepting the axioms. Ideally, we want the axioms to be "self-evident" or at least easy to understand intuitively. Maybe it's just me, but Meredith's axiom does not leap out at me as something that should obviously be true, let alone sufficient to prove all other classical tautologies.
Minimality is, however, not the "whole point" of axiomatic systems. You mention another reason: sometimes you actually do want to prove things at which point it is better to have a richer and more intuitive axiomatic system. You may argue that we can just derive any theorems we want to use from some minimal basis, and then forget about that basis. This is true but unnecessary complexity if we have no other reason for considering this minimal basis. When we compare different styles of proof system (e.g. Hilbert v. Sequent Calculus v. Natural Deduction), translations between them (especially into Hilbert-style systems) can involve a lot of mechanical complexity. That complexity can sometimes be significantly reduced by a careful choice of axioms.
For the Laws of the Excluded Middle (LEM) and Non-contradiction, the first thing you'd need to do is define the connectives. You can't prove $\neg(P\land\neg P)$ in a system that doesn't have $\land$. Given $\neg$ and $\to$ as primitives, standard definitions of $\land$ and $\lor$ are $P\land Q:\equiv \neg(P\to\neg Q)$ and $P\lor Q:\equiv\neg P\to Q$. With these definitions (or others), then yes, the LEM and Non-contradiction can both be proven in the systems you mention and any other proof system for classical propositional logic. Your concern here is an illustration that we often care about which axioms we have and not just that they're short and effective.
This also leads to another reason why we might want a certain presentation. We may want that presentation to line up with other, related logics. As you're starting to realize, it is ill-defined to say something like "intuitionistic propositional logic (IPL) is classical propositional logic (CPL) minus the LEM". When people say things like this, they are being sloppy. However, "CPL is IPL plus LEM" is unambiguous. Any presentation of IPL to which we add LEM is a presentation of CPL. For that presentation, it makes sense to talk about removing LEM. It doesn't make sense to talk about removing an axiom without a presentation of axioms that contains that axiom. It is also quite possible to have a presentation of CPL containing LEM that becomes much weaker than IPL when LEM is removed. In fact, you'd expect this because a presentation of IPL with LEM added is likely to be redundant because things which are intuitionistically distinct become identifiable when LEM is added. The story is the same for paraconsistent logics.
While it isn't as much of a driver for Hilbert-style proof systems, for natural deduction and sequent calculi the concerns of structural proof theory often push for more axioms (or rules of inference, rather). For example, many axioms in a Hilbert-style proof system mix together connectives, e.g. as Meredith's does above. This means we can't understand a connective on its own terms, but only by how it interacts with other connectives. A driving force in typical structural presentations is to characterize connectives by rules that don't reference any other connectives. This better reveals the "true" nature of the connectives, and it makes the system more modular. It becomes meaningful to talk about adding or removing a single connective allowing you to build a logic à la carte. In fact, structural proof theory motivates many constraints on what a proof system should look like such as logical harmony.
1 And that link only considers Hilbert-style proof systems.
(1) Yes. The particular dependent type theory one wants to use has UIP (Uniqueness of Identity Proofs), one universe of all propositions (in the homotopy-type-theory sense, i.e. subsingletons) satisfying propositional extensionality, pushouts (a kind of higher inductive type), and propositional truncations. This is a sort of truncated version of homotopy type theory.
(2) The type theory described above is one state of the art. Alternatively, one can use higher-order logic as described, for instance, in Sketches of an Elephant. I tend to prefer dependent type theory, since dependent types occur naturally in mathematics; but the semantics and metatheory are more difficult in that case (and filling in some of their details is a problem of current research).
(3) Agda, Coq, Idris can all manage this type theory easily, when suitably augmented by axioms (for UIP, propositional extensionality, etc.). The main wrinkle is that they all have a tower of universes, which an arbitrary elementary topos may not; but you can just ignore the larger universes. You can also reason in higher-order logic inside such a proof assistant by simply not making use of the dependent types.
Best Answer
In the context of topos theory the answer would be no. The reason is (which I think is what you are saying) that in a topos the lattice of subobjects of the subobject classifier is a Heyting algebra, not (generally) a co-Heyting algebra. The duality you are talking about above is really saying that paraconsistent logic is algebraically like a co-Heyting algebra, while intuitionistic logic is algebraically like a Heyting algebra.
Of course, it should not be surprising that topos theory is not ideal for modeling paraconsistent logic seeing that it was designed to be ideal for intuitionistic logic (and paraconsistent logic is quite disjoint from it).
Now, to partly answer you question, it is unlikely that a notion dual to a topos will model paraconsistent logic. The reason is that the dual of a topos is (of course) generally not a topos and subobjects in the dual (which are the same as quotient objects in the original topos) don't have any Heyting or co-Heyting structure. What happens is that the lattice of quotient objects in the dual of a topos is the Hetying algebra of the subobjects in the original topos. In any case, no co-Heyting algebra there.
Whether there are categories that model paraconsistent logic, I think is currently not known.