Constructive Logic with Strong Negation
is a Substructural Logic
(Web Support)
Matthew Spinks and
Robert Veroff
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 twopart 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 proofchecking 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_ewalgebras 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 3potent, classical FL_ewalgebras
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_ewalgebras satisfies the identity:
x > x = 1 (N2)
Proof.
(in,
out,
pf,
xml)

Lemma 4.6. The variety of Nelson FL_ewalgebras satisfies the identity:
(x > y) ^ (x > z) = x > (y ^ z) (N5)
Proof.
(in,
out,
pf,
xml)

Lemma 4.7. The variety of Nelson FL_ewalgebras 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_ewalgebras satisfies the identity:
(x ^ y) > z = x > (y > z) (N6)
Proof.
(in,
out,
pf,
xml)

Lemma 4.9. The variety of Nelson FL_ewalgebras satisfies the identity:
x ^ (~x v y) = x ^ (x > y) (N4)
Proof.
(in,
out,
pf,
xml)

Lemma 4.11. The variety of Nelson FL_ewalgebras 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):325348, 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):157174, 2001.
(postscript)