# A question about consistent fragments of formalized mathematical theories with Natural Deduction

Ref to : Sara Negri & Jan von Plato, Structural Proof Theory (2001).

In Ch.6 : Structural Proof Analysis of Axiomatic Theories [page 126-on], they

give a method of adding axioms to sequent calculus, in the form of nonlogical rules of inference.

Theorem 6.4.1 [page 136] : If $\Gamma \implies \Delta$ is derivable in $G3im^*$ or $G3c^*$, [where the first is an extesion of $G3im$, the intuitionistic multisuccedent sequent calculus] the derivation are either subformulas of the endsequent or atomic formulas.

Consider a theory having as axioms a finite set $D$ of regular formulas. Define $D$ to be inconsistent if $\implies \bot$ is derivable in the corresponding extension and consistent if it is not inconsistent. For a theory $D$, inconsistency surfaces with the axioms through regular decomposition, with no consideration of the logical rules:

Theorem 6.4.2: [...]

It follows that if an axiom system is inconsistent, its formula traces contain negations and atoms or disjunctions. Therefore, if there are neither atoms nor disjunctions, the axiom system is consistent, and similarly if there are no negations. [page 137]

Finally, they consider [page 147-148] Lattice theory, and conclude with :

All structural rules are admissible in the proof-theoretical formulation of lattice theory. The underivability of $\implies \bot$ follows, by Theorem 6.4.2, from the fact that no axiom of lattice theory is a negation.

Consider now, for simplicity, one of the following systems [see Peter Smith, An Introduction to Gödel's Theorems (1st ed - 2007), page 51-on] :

BA, Baby Arithmetic

Q, Robinson Arithmetic

Both have the axiom : $\lnot 0 = S(x)$, that is (using standard "unabbreviation" for $\lnot$) : $0 = S(x) \rightarrow \bot$.

Using the fact established above, may we say that if we have systems whose axioms does not include the $\bot$ sign, they are ipso facto consistent ?

Are there “interesting fragments” of arithmetic, based on intuitionistic sequent calculus, that are “negation-free” ?

In negation-free arithmetic, replace the axiom $\neg 0=S(x)$ with $0=S(x) \rightarrow 0=1$. This has the same negation-free theorems as ordinary arithmetic.
The amusing reason for this is that any arithmetical statement follows from $0=1$, even without negation: $0=1$, so $0=a$ and $0=b$ and therefore $a=b$, and so on.
• Thanks for your hints, but I'm not sure that it works. My idea (perhaps a stupid one) was : I'm asking if we can try to exploit the nature of sequent calculus rules with the above result of Negri & von Plato [i.e.if the axioms do not contain $\lnot$ nor $\bot$ we may have a consistentcy proof "by inspection] to a theory like Robinson arithmetic, omitting the axioms with the $\lnot$ symbol (eventually, replacing them). I think that $0=1$ is only $\bot$ "in disguise", so that using $0=S(x) \rightarrow 0=1$ in place of $\lnot 0=S(x)$ will inhibit the application of the above result. Feb 1 '14 at 16:02