Basis proofs for system C4, the pure implicational fragment of S4

Notation: Native | Polish | Psudo Otter | CS

EFHW = AB

To prove that the EFHW basis and the Anderson and Belnap basis are the same system, one needs to prove both that the Anderson and Belnap [AB] basis can prove the EFHW basis, and that the EFHW basis can prove the Anderson and Belnap basis [AB]. Given both of those, they are both bases for the same system.

AB contains EFHW

```
# Proof output notation
=format otter

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:16:35 2008
# by the "testy" program, version 2008-07-09 0.01.15

# Input files:
#   "input.c4.anderson-belnap"
#   "wishlist.c4.EFHW-2base1"

# Name of this logical system.
=name C4
# Axiomatic Basis:
=basis     Anderson and Belnap

#          --- Axioms ---

1: P(i(p,p)).                                         # Axiom 1
2: P(i(i(p,q),i(r,i(p,q)))).                          # Axiom 2
3: P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))).                # Axiom 3

#          --- Wish List ---

=wishlist "P(i(p,i(q,q)))."                          "EFHW 2base1 Axiom 1"
=wishlist "P(i(i(p,i(q,r)),i(i(p,q),i(s,i(p,r)))))." "EFHW 2base1 Axiom 2"

#          --- Theorems ---

# Wish list theorem: EFHW 2base1 Axiom 1
4: P(i(p,i(q,q))).                                    # Condensed detachment, inference line 2 with line 1

5: P(i(p,i(i(q,r),i(s,i(q,r))))).                     # Condensed detachment, inference line 2 with line 2
6: P(i(i(p,i(q,r)),i(p,i(s,i(q,r))))).                # Condensed detachment, inference line 3 with line 5
7: P(i(p,i(i(q,i(r,s)),i(i(q,r),i(q,s))))).           # Condensed detachment, inference line 2 with line 3
8: P(i(i(p,i(q,i(r,s))),i(p,i(i(q,r),i(q,s))))).      # Condensed detachment, inference line 3 with line 7
9: P(i(i(p,q),i(i(r,p),i(r,q)))).                     # Condensed detachment, inference line 8 with line 2
10: P(i(i(i(p,q),i(r,p)),i(i(p,q),i(r,q)))).           # Condensed detachment, inference line 3 with line 9
11: P(i(i(i(i(p,q),i(p,r)),s),i(i(p,i(q,r)),s))).      # Condensed detachment, inference line 10 with line 7

# Wish list theorem: EFHW 2base1 Axiom 2
12: P(i(i(p,i(q,r)),i(i(p,q),i(s,i(p,r))))).           # Condensed detachment, inference line 11 with line 6

# Final proof had 12 lines (9 steps)
# ------------------ End proof --------------

# Summary:
# 3 axioms given.
# 410 generated theorems in the working set.
# 16560 "one step away" theorems in the halo.
# 9 of those we generated seemed to be interesting.
#   (Factor of 40.1 overhead for the halo. [16560 vs. 413])
```

Proof that EFHW contains AB

```
# Proof output notation
=format otter

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:48:20 2008
# by the "testy" program, version 2008-07-09 0.01.15

# Input files:
#   "wishlist.c4.anderson-belnap"
#   "input.c4.EFHW-2base1"

# Name of this logical system.
=name C4
# Axiomatic Basis:
=basis     EFHW 2 base 2

#          --- Axioms ---

1: P(i(p,i(q,q))).                                    # Axiom 1
2: P(i(i(p,i(q,r)),i(i(p,q),i(s,i(p,r))))).           # Axiom 2

#          --- Wish List ---

=wishlist "P(i(p,p))."                          "Anderson and Belnap, basis 1, axiom 1"
=wishlist "P(i(i(p,q),i(r,i(p,q))))."           "Anderson and Belnap, basis 1, axiom 2"
=wishlist "P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))." "Anderson and Belnap, basis 1, axiom 3"

#          --- Theorems ---

# Wish list theorem: Anderson and Belnap, basis 1, axiom 1
3: P(i(p,p)).                                         # Condensed detachment, inference line 1 with line 1

# Wish list theorem: Anderson and Belnap, basis 1, axiom 2
4: P(i(i(p,q),i(r,i(p,q)))).                          # Condensed detachment, inference line 2 with line 1

5: P(i(p,i(q,i(r,r)))).                               # Condensed detachment, inference line 4 with line 1
6: P(i(i(i(p,i(q,r)),i(p,q)),i(s,i(i(p,i(q,r)),i(t,i(p,r)))))).
# Condensed detachment, inference line 2 with line 2
7: P(i(p,i(i(q,i(i(r,r),s)),i(t,i(q,s))))).           # Condensed detachment, inference line 6 with line 5
8: P(i(i(p,i(q,i(i(r,r),s))),i(t,i(p,i(u,i(q,s)))))). # Condensed detachment, inference line 2 with line 7
9: P(i(p,i(i(q,i(r,s)),i(t,i(i(q,r),i(q,s)))))).      # Condensed detachment, inference line 8 with line 2
10: P(i(i(p,i(q,r)),i(s,i(i(p,q),i(p,r))))).           # Condensed detachment, inference line 9 with line 1
11: P(i(i(i(p,q),p),i(r,i(i(p,q),q)))).                # Condensed detachment, inference line 2 with line 3
12: P(i(p,i(i(i(q,q),r),r))).                          # Condensed detachment, inference line 11 with line 1
13: P(i(i(p,i(i(q,q),r)),i(s,i(p,r)))).                # Condensed detachment, inference line 2 with line 12
14: P(i(p,i(i(i(i(i(q,q),r),r),s),s))).                # Condensed detachment, inference line 11 with line 12
15: P(i(i(p,i(i(i(i(q,q),r),r),s)),i(t,i(p,s)))).      # Condensed detachment, inference line 2 with line 14
16: P(i(p,i(i(q,i(i(r,r),s)),i(q,s)))).                # Condensed detachment, inference line 15 with line 13
17: P(i(i(p,i(i(q,q),r)),i(p,r))).                     # Condensed detachment, inference line 16 with line 1

# Wish list theorem: Anderson and Belnap, basis 1, axiom 3
18: P(i(i(p,i(q,r)),i(i(p,q),i(p,r)))).                # Condensed detachment, inference line 17 with line 10

# Final proof had 18 lines (16 steps)
# ------------------ End proof --------------

# Summary:
# 2 axioms given.
# 500 generated theorems in the working set.
# 13905 "one step away" theorems in the halo.
# 4 of those we generated seemed to be interesting.
#   (Factor of 27.7 overhead for the halo. [13905 vs. 502])
```