Slaney's Logic F** is Constructive Logic with Strong Negation (Web Support)

Slaney's Logic F** is Constructive Logic
with Strong Negation
(Web Support)

September 2009

This page provides Web support for

Slaney's Logic F** is Constructive Logic with Strong Negation [3].

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

Abstract

In [2], Slaney et al. introduced a little-known deductive system F** in connection with the problem of the indeterminacy of future contingents. The main result of this paper shows that, to within definitional equivalence, F** has a familiar description: it is precisely Nelson's constructive logic with strong negation [4].

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 [5]. 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

Lemma 2.2. (16 parts)

   %
   % Identities and quasi-identities axiomatising Alg Mod* F**.
   %

   x => ((x => y) => y) = 1                               (A1)[= 1]
   (x => y) => ((y => z) => (x => z)) = 1                 (A2)[= 1]
   (x ^ y) => x = 1                                       (A3)[= 1]
   (x ^ y) => y = 1                                       (A4)[= 1]
   ((x => y) ^ (x => z)) => (x => (y ^ z)) = 1            (A5)[= 1]
   x => (x v y) = 1                                       (A6)[= 1]
   y => (x v y) = 1                                       (A7)[= 1]
   ((x => z) ^ (y => z)) => ((x v y) => z) = 1            (A8)[= 1]
   (x ^ (y v z)) => ((x ^ y) v z) = 1                     (A9)[= 1]
   ~x => x = 1                                            (A10)[= 1]
   (x => ~y) => (y => ~x) = 1                             (A11)[= 1]
   x => (y => x) = 1                                      (A12)[= 1]
   ((x => (x => y)) ^ (~y => (x => y))) => (x => y) = 1   (A13)[= 1]

   all x all y (((x = 1) & (x => y = 1)) -> (y = 1))      (3)
   all x all y (((x = 1) & (y = 1)) -> (x ^ y = 1))       (4)
   all x all y (((x => y = 1) & (y => x = 1)) -> (x = y)) (5)

Proof of (A1)-(A13). (in, out, pf, xml)

Proof of (3). (in, out, pf, xml)

Proof of (4). (in, out, pf, xml)

Proof of (5). (in, out, pf, xml)

Lemma 2.3. (3 parts)

   x => x = y => y                               (7)
   ~x = x => ~(y => y)                           (8)
   x => y = ~y => ~x                             (9)

Proof. (in, out, pf, xml)

Lemma 2.4. (22 parts)

   %
   % Identities axiomatising Nelson FL_ew-algebras.
   %
   
   % Bounded lattice part
   (x v y) v z = x v (y v z)                     (D1)
   (x ^ y) ^ z = x ^ (y ^ z)                     (D2)
   
   x ^ x = x                                     (D3)
   x v x = x                                     (D4)
   
   x v y = y v x                                 (D5)
   x ^ y = y ^ x                                 (D6)
   
   x v (x ^ y) = x                               (D7)
   x ^ (x v y) = x                               (D8)
   
   x ^ 0 = 0                                     (D9)
   x ^ 1 = x                                     (D10)
   
   % Monoid part
   x * 1 = x                                     (M1)
   x * y = y * x                                 (M2)
   (x * y) * z = x * (y * z)                     (M3)
   
   % Residuation part
   x * (y v z) = (x * y) v (x * z)               (R1)
   x => (y ^ z) = (x => y) ^ (x => z)            (R2)
   (x * (x => y)) v y = y                        (R3)
   (x => (x * y)) ^ y = y                        (R4)
   
   % Nelson part
   x => (x => (x => y)) = x => (x => y)          (E_2, 3-potency)
   
   (x v y) ^ (x v z) = x v (y ^ z)               (D11)
   (x ^ y) v (x ^ z) = x ^ (y v z)               (D12)
   
   ~(~x) = x                                     (I)
   
   (x => (x => y)) ^ (~y => (~y => ~x)) = x => y (N, Nelson identity)

Proof. (in, out, pf, xml)

References

W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
J. Slaney, T. Surendonk and R. Girle. Time, Truth and Logic. Tech. Report TR-ARP-11/89, Automated Reasoning Project, Australian National University, Canberra, 1989. (gzipped postscript)
M. Spinks and R. Veroff. Slaney's Logic F** is Constructive Logic with Strong Negation. Bulletin of the Section of Logic, to appear.
D. Vakarelov. Notes on N-lattices and Constructive Logic with Strong Negation. Studia Logica, 36:109-125, 1977.
R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)