2
$\begingroup$

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

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Do you have some bibliographical reference about this topic? Thanks. $\endgroup$
    – Mauro ALLEGRANZA
    Jan 31, 2014 at 15:55
  • $\begingroup$ Bishop said (Bishop and Bridges 1985, p. 10-11): "the negation of a statement P is the statement (P implies (0=1))." A few paragraphs later he suggests that for any statement, "we may be more meticulous and prove that the theorem is a consequence of the equality 0=1". But since the proof is just a matter of being meticulous about the formal system, I don't know anyone who's bothered to publish it. $\endgroup$
    – Matt F.
    Jan 31, 2014 at 17:17
  • $\begingroup$ 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. $\endgroup$
    – Mauro ALLEGRANZA
    Feb 1, 2014 at 16:02

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.