Constructive Logic with Strong Negation (Web Support)

Constructive Logic with Strong Negation
is a Substructural Logic
(Web Support)

January 2008 (updated July 2008)

This page provides Web support for a paper that is published in two parts:

Constructive Logic with Strong Negation is a Substructural Logic. I [2].
Constructive Logic with Strong Negation is a Substructural Logic. II [3].

In particular, we present here proofs that were found with the assistance of the program Prover9 [1].

Abstract

The goal of this two-part series of papers is to show that constructive logic with strong negation is definitionally equivalent to a certain axiomatic extension NFL_ew of the substructural logic FL_ew. In Part I, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL_ew (namely, a certain variety of FL_ew algebras) are term equivalent. The main result of Part I is exploited in Part II to show that the deductive systems N and NFL_ew are definitionally equivalent, and hence, that constructive logic with strong negation is a substructural logic over FL_ew.

Prover9 Proofs

For each proof, we include input, output, proof and xml files created as follows.

prover9 -f file.in > file.out prooftrans -f file.out > file.pf
prooftrans xml -f file.out > file.xml

We note that these essentially are proof-checking runs, since they include steps from previously found proofs as hints. The original proofs were found using the method of proof sketches [4]. In particular, our approach was to find derivations with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired proofs.

Proofs for Part I

Lemma 3.1. The variety of Nelson algebras satisfies the identities:

   (x ^ y) -> y = 1                          (3.10)
   (x ^ y) => y = 1                          (3.11)
   ~x => ~y = y => x                         (3.12)
   (x => y) ^ y = y                          (3.13)
   x => (x ^ y) = x => y                     (3.14)

Proof. (in, out, pf, xml)

Alternate version that shows the 5 separate subproofs. (in, out, pf, xml)

Proposition 3.2. The variety of Nelson algebras satisfies the identity:
```
   x => (x => y) = x -> y                    (3.15)
```
Proof. (in, out, pf, xml)
Lemma 3.3. The variety of Nelson algebras satisfies the identity:
```
   (x => y) => ((z => x) => (z => y)) = 1    (BCK1')
```
Proof. (in, out, pf, xml)
Lemma 3.4. The variety of Nelson algebras satisfies the identity:
```
   x => ((x => y) => y) = 1                  (BCK5)
```
Proof. (in, out, pf, xml)
Lemma 3.6. The variety of Nelson algebras satisfies the identity:
```
   x => (x => (x => y)) = x => (x => y)      (E2)
```
Proof. (in, out, pf, xml)
Lemma 3.9. The variety of Nelson algebras satisfies the identity:
```
   (x * y) => z = x => (y => z)              (P)
```
Proof. (in, out, pf, xml)
Lemma 3.13. The variety of Nelson algebras satisfies the identity:
```
   x => 0 = ~x                               (3.19)
```
Proof. (in, out, pf, xml)

Lemma 4.3. The variety of classical FL_ew-algebras satisfies the identities:

   (x => y) ^ y = y                          (3.13)
   (x v y) => y = x => y                     (4.6)
   x -> (y => z) = y => (x -> z)             (4.7)
   x ^ (~x => y) = x                         (4.8)

Proof. (in, out, pf, xml)

Alternate version that shows the 4 separate subproofs. (in, out, pf, xml)

Lemma 4.4. The variety of 3-potent, classical FL_ew-algebras satisfies the identities:
```
   x -> ((y v x) -> z) = x -> z              (4.9)
   x -> (~x v y) = x -> y                    (4.10)
```
Proof. (in, out, pf, xml)
Alternate version that shows the 2 separate subproofs. (in, out, pf, xml)
Lemma 4.5. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   x -> x = 1                                (N2)
```
Proof. (in, out, pf, xml)
Lemma 4.6. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   (x -> y) ^ (x -> z) = x -> (y ^ z)        (N5)
```
Proof. (in, out, pf, xml)
Lemma 4.7. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   (x -> y) ^ (~x v y) = ~x v y              (N3)
```
Proof. (in, out, pf, xml)
Lemma 4.8. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   (x ^ y) -> z = x -> (y -> z)              (N6)
```
Proof. (in, out, pf, xml)
Lemma 4.9. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   x ^ (~x v y) = x ^ (x -> y)               (N4)
```
Proof. (in, out, pf, xml)
Lemma 4.11. The variety of Nelson FL_ew-algebras satisfies the identity:
```
   (x ^ ~x) ^ (y v ~y) = x ^ ~x              (N1)
```
Proof. (in, out, pf, xml)

Proofs for Part II

Lemma 5.1. In H, if

   w => x and x => w and y => z and z => y

then

   (w ^ y) => (x ^ z) and (w v y) => (x v z).

Proof. (in, out, pf, xml)

Lemma 5.5. The variety Alg Mod^* NFL_ew satisfies the identity:
```
   (x => (x => y)) ^ (~y => (~y => ~x)) = x => y   (N)
```
Proof. (in, out, pf, xml)

References

W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
M. Spinks and R. Veroff. Constructive Logic with Strong Negation is a Substructural Logic. I. Studia Logica, 88(3):325-348, 2008.
M. Spinks and R. Veroff. Constructive Logic with Strong Negation is a Substructural Logic. II. Studia Logica, to appear.
R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)