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” ?



A question about consistent fragments of formalized mathematical theories with Natural Deduction
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.


