In Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965), we have the system I of intuitionistic (first-order) logic based on eleven introduction- and elimination-rules : the 3 couples for the connectives $\lor, \land$ and $\rightarrow$, the two couples for the quantifiers and the $\bot_I$ rule [page 20].
The system C of classical logic is obtained with the addition of the $\bot_C$ rule.
The system C’ is obtained from C excluding $\lor$ and $\exists$ and treating them as defined in the usual way [page 39].
It is assumed that the negation $\lnot A$ is an abbreviation for $A \rightarrow \bot$ [page 16] so that we do not need it.
We assume that a system is inconsistent if we have a proof [see page 24 for the definition] of $\bot$.
The following result is on page 44 :
COROLLARY 3 [to the Theorem on normal deductions for classical logic] [the system] C’ is consistent; in particular, $\bot$ is not provable in C’.
According to the definition of system of natural deduction [page 24], we can think of an “applied” calculus obtained form I or C with suitable axioms; e.g. first-order Peano axioms.
For simplicity, consider 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 Prawitz definition 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 ?
If so, are there “interesting fragments” of arithmetic or other mathematical theories that are “negation-free” ?
I made a research into Sara Negri & Jan von Plato, Structural Proof Theory (2001), due to the similarity between Natural Deduction and sequent calculus.
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, and I beg your pardon for a so long question, 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.
So my question becomes :
Are there “interesting fragments” of arithmetic, based on intuitionistic sequent calculus, that are “negation-free” ?