3
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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 $\endgroup$ – Hagen von Eitzen Apr 1 '18 at 16:36
  • $\begingroup$ @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. $\endgroup$ – user56834 Apr 2 '18 at 7:40
  • $\begingroup$ @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. $\endgroup$ – Rob Arthan Apr 2 '18 at 17:56
  • $\begingroup$ @RobArthan, but a non-recursive axiom scheme or inference rule can never be computed, correct? So it would be useless? $\endgroup$ – user56834 Apr 2 '18 at 18:35
  • $\begingroup$ 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. $\endgroup$ – Rob Arthan Apr 2 '18 at 18:55
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ What axiom is equivalent to the rule of universal generalisation (from $\phi(x)$ infer $\forall x\phi(x)$)? $\endgroup$ – Rob Arthan Apr 2 '18 at 17:59
  • $\begingroup$ All I get is lots of stuff about propaganda. Can you give a link please. $\endgroup$ – Rob Arthan Apr 26 '18 at 16:44
  • $\begingroup$ 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. $\endgroup$ – Daniil Kozhemiachenko Apr 26 '18 at 19:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.