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

Question

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

Added Jan,30

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

Answer 1

On

"May we say that if we have systems whose axioms does not include the ⊥ sign, they are ipso facto consistent?"

In the absence of negation (or the absurdity sign), the usual definition of consistency is Post-consistency, i.e. you can't prove every proposition. [In the presence of negation and explosion, this is equivalent to not being able to prove a contradiction. For if you can prove every proposition, you can prove a contradiction, and conversely if you can prove a contradiction, explosion gives you every other proposition.]

Evidently, not including negation isn't enough to be Post consistent.

Answer 2

There are more than one description on what an inconistent system is.

the usual descriptions are:

1. a system in which you can proof $\bot$
2. a system in which you can proof for some formula and its negation $ P \land \lnot P$
3. a system in whichyou can proof all formulas

Of these 3. (a system in which you can proof all formulas) is the real problem, if you can proof everything what is the use of logic? The other two are just shorthands for the third one. (because proving that you can proof everything can be a rather time consuming exercize)

But 1 cannot be applied to logics that don't contain $\bot$, 2 cannot be applied to logics that don't contain $\lnot$ so for negation free logics you are stuck with 3. (as you are with paraconsistent logics where 1 or 2 does not lead to 3)

For a simple inconsistent logic read http://en.wikipedia.org/wiki/Logical_harmony , and then imagine a logic containing a Tonk - connective, no $\bot$ or $\lnot$ but still inconsistent.