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

Matthew Spinks and Robert Veroff

September 2009

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

1. W. McCune. Prover9. http://www.cs.unm.edu/~mccune/prover9.
2. 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)
3. M. Spinks and R. Veroff. Slaney's Logic F** is Constructive Logic with Strong Negation. Bulletin of the Section of Logic, to appear.
4. D. Vakarelov. Notes on N-lattices and Constructive Logic with Strong Negation. Studia Logica, 36:109-125, 1977.
5. R. Veroff. Solving Open Questions and Other Challenge Problems Using Proof Sketches. Journal of Automated Reasoning, 27(2):157-174, 2001. (postscript)