I suspect that it will be hard to correctly convey this question, but here goes:
How its normally done:
The way I've been taught, and what is normally done in mathematical logic, is as follows:
We have a logical system, let's take first order logic, together with one of the standard valid-and-complete proof systems, i.e. a proof system such that $\Phi \models\phi$ iff $\Phi\vdash \phi$, where $\Phi\models\phi$ means "Every possible interpretation that satisfies $\Phi$ also satisfies $\phi$". Such logical systems are intended to provide valid inferences for all possible interpretations.
Then, we formulate a set of axioms for a specific mathematical structure, such as standard arithmetic $(\mathbb N, +,\cdot, 0,1)$. We then use the logical axioms (which are valid for all mathematical structures, since they do not presuppose any) to draw inferences from those axioms. i.e. we say: Every interpretation that satisfies these axioms must also satisfy these other statements.
So essentially, we have a kind of "division of labor":
The logical axioms should draw inferences that are valid regardless of the interpretation.
The "object-level" axioms should make specific claims about the structure we want to axiomatize. (e.g. the peano axioms).
My proposal:
I am wondering whether the following proposal will have expressive advantages over the standard one:
We now create a logical system that is specifically tailored to a mathematical structure. Let me denote by $\mathcal L^\mathfrak A$ some logical system with a set of logical axioms that is intended for the structure $\mathfrak A$.
We still have a logical system with logical axioms, but we no longer require that its inferences are correct in all interpretations. i.e. we no longer require that $\Phi \models\phi$ iff $\Phi\vdash \phi$. Instead, we only require that $\Phi \models^{\mathfrak A}\phi$ iff $\Phi\vdash^ {\mathfrak A} \phi$, for a specific mathematical structure $\mathfrak A$, where $\Phi \models^{\mathfrak A}\phi$ means "if $\Phi$ is satisfied in the structure $\mathfrak A$ then $\phi$ is also satisfied in $\mathfrak A$", and $\Phi\vdash^ {\mathfrak A} \phi$ means "using the logical system $\mathcal L ^\mathfrak A$ we can prove $\phi$ from $\Phi$".
For example, we create a set of logical axioms specifically for the structure of standard arithmetic $\mathcal N =(\mathbb N, +, \cdot, 0, 1)$, meaning that if $\Phi$ is a set of statements that hold in standard arithmetic, then we can only have $\Phi\vdash^\mathcal N \phi$, if $\phi$ is also true in $\mathcal N$ (standard arithmetic).
This means that we can obviously add the logical axioms of standard first-order logic to any $\mathcal L^\mathfrak A$, since they by assumption hold for all interpretations. But we may now also add additional logical axioms that rely on specific properties of the structure in question. For example, $\mathcal L^\mathcal N$ may contain logical axioms that rely on $\mathbb N$ having a countable number of elements.
Therefore, we no longer have such a strict "division of labor": Both the logical axioms and the "object-level" axioms are specifically tailored to a specific structure.
Obviously, this has a serious downside: the logical system now only applies to one structure, so it is not as versatile.
But my question is:
If we allow for logical axioms (i.e. inference rules) that don't necessarily give correct conclusions when applied to all interpretations, but always give correct conclusions when applied to a specific structure, does that give us a potentially more powerful proof system for that structure?
For example, could we potentially formulate a finite set of logical axioms specifically for standard arithmetic, such that contrary to Godel's theorem, all true statements are provable with this $\mathcal L^\mathcal N$?
Or does this add nothing to our expressive power? i.e. can we always reformulate such structure-specific logical axioms into "object-level" axioms?
We can always convert axioms to rules and vice versa. Here is a “natural deduction” for a very weak arithmetic.
Consider now following statements of elementary number theory.
So, how do we get rid of these axioms? We make rules of inference from them! Here big letters denote arbitrary formulas.
Using these rules it is easy to obtain our initial axioms. In fact, it is an easy exercise to make axioms from rules and rules from axioms.