# Are there “structure-specific” logical axiomatic systems? Do these have extra power?

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:

1. 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.

2. 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":

1. The logical axioms should draw inferences that are valid regardless of the interpretation.

2. 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?

• If you keep modus ponens as rule of inference, then any new rule of inference could be recast into an axiom scheme. At any rate, you can't beat Gödel this way – Hagen von Eitzen Apr 1 '18 at 16:36
• @HagenvonEitzen, could you explain why any rule of inference can be recast in an axiom scheme? Also, the reason why I don't immediately see that we can't beat godel this way, is that godel's theorem seems to assume that the proof system is valid, which $\mathcal L ^\mathcal N$ wouldn't be. – user56834 Apr 2 '18 at 7:40
• @HagenvonEitzen: you need to be a bit careful: you can "beat" Gödel by allowing non-recursive axiom schemas. So you need some restrictions on new inference rules. I think your conclusion is true if you restrict to inference rules defined as recursive relations. – Rob Arthan Apr 2 '18 at 17:56
• @RobArthan, but a non-recursive axiom scheme or inference rule can never be computed, correct? So it would be useless? – user56834 Apr 2 '18 at 18:35
• What do you mean by useless? (It's not true that particular values of a non-recursive function cannot be computed.) An extreme of your suggestion of adding structure-specific inference rules would be add to PA all rules that are sound for PA. The resulting system of inference relations would not be recursive. – Rob Arthan Apr 2 '18 at 18:55

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.

1. $\forall x\quad x=x$
2. $\forall x\forall y(x=y\supset y=x)$
3. $\forall x\forall y\forall z((x=y\&y=z)\supset x=z)$
4. $\forall x\neg x+1=x$
5. $\forall x\forall y\quad x+y=y+x$
6. $\forall x\forall y\forall z\quad x+(y+z)=(x+y)+z$

So, how do we get rid of these axioms? We make rules of inference from them! Here big letters denote arbitrary formulas.

1. $\dfrac{A}{x=x}$
2. $\dfrac{x=y}{y=x}$
3. $\dfrac{x=y\quad y=z}{x=z}$
4. $\dfrac{x+1=x}{\bot}$
5. $\dfrac{x+y=z}{y+x=z}$
6. $\dfrac{x+(y+z)=w}{(x+y)+z=w}$

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.

• What axiom is equivalent to the rule of universal generalisation (from $\phi(x)$ infer $\forall x\phi(x)$)? – Rob Arthan Apr 2 '18 at 17:59
• All I get is lots of stuff about propaganda. Can you give a link please. – Rob Arthan Apr 26 '18 at 16:44
• In a way, yes. Here it is: $\forall x(A\supset B)\supset(A\supset\forall x B)$ where $x$ is not free in $B$. However, there is a problem. Generalisation rule is correct only w.r.t. valid (or at least true in a model) formulas. This is why you cannot use deduction theorem as a rule of inference in FOL as freely as you can do it in propositional logic. – Daniil Kozhemiachenko Apr 26 '18 at 19:20