Are there any examples of consistent proper axiomatic extensions of classical logic? By a proper axiomatic extension, I mean a logic with the same set of well formed formulas as classical logic, but with the set of theorems of the logic a proper superset of the theorems of classical logic.
Have such systems been studied? Are there even any examples of such systems which are consistent? The similar class of superintuitionistic logics (i.e. inbetween intuitionistic and classical logic) seems to be well studied, so I was surprised when I couldn't find anything interesting about superclassical logics, with most articles I did find giving examples of syntactic extensions of classical logic like modal and temporal logic. Also, if such systems exist, does this class (or a similar class) of logics have a commonly used name in the literature so I can more easily find resources on them?
 A: Your question is ill-defined. $PA+Con(PA)$ is a proper extension of $PA$ that proves $Con(PA)$, which $PA$ cannot prove. But both are classical first-order theories. Thus you shouldn't be asking about "proving more theorems". Instead, as J Marcos suggests in a comment, you may be asking for a consequence relation that is a strict superset of the classical one. That is possible, but bad, in the sense that it is impossible to add any inference rule of the form $S \vdash φ$ for some finite set $S$ of formulae and some formula $φ$, without making some previously consistent theory inconsistent on extending to the new closure under consequence. This is because adding any such rule is equivalent to adding a single axiom $A$ that is not a classical tautology. Thus $\neg A$ is not a contradiction, so let $T$ be some classical first-order theory that proves $\neg A$. Clearly then $T$ cannot be extended to a theory that is closed under the new consequence without proving $A \land \neg A$.
The above shows that it is impossible to add any finitary rule, which means that you cannot extend the classical consequence relation recursively. But if you really really want you can add infinitary rules, though they will never be practical since they are not recursive. For example, you can add an inference rule that says that if the axioms are $Σ_1$-sound (via a suitable translation), then you can from $φ(0),φ(1),φ(2),\cdots$ (translated) derive $\forall n\ ( φ(n) )$ (translated), for any formula $φ$ over PA. This is called the $ω$-rule. One can see that this never makes any classically consistent axiomatization inconsistent, and it is a strict extension of the classical consequence relation, since it makes $PA$ become complete! Note that a proof of a true sentence about $\mathbb{N}$ over $PA$ may require infinitely many applications of the $ω$-rule.
