# 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 native

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:15:27 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 p)                                           # Axiom 1
2: ('> ('> p q) ('> r ('> p q)))                      # Axiom 2
3: ('> ('> p ('> q r)) ('> ('> p q) ('> p r)))        # Axiom 3

#          --- Wish List ---

=wishlist "('> p ('> q q))"                                    "EFHW 2base1 Axiom 1"
=wishlist "('> ('> p ('> q r)) ('> ('> p q) ('> s ('> p r))))" "EFHW 2base1 Axiom 2"

#          --- Theorems ---

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

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

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

# Final proof had 12 lines (9 steps) [Work 395]
# ------------------ 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 native

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:59:52 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 ('> q q))                                    # Axiom 1
2: ('> ('> p ('> q r)) ('> ('> p q) ('> s ('> p r)))) # Axiom 2

#          --- Wish List ---

=wishlist "('> p p)"                                    "Anderson and Belnap, basis 1, axiom 1"
=wishlist "('> ('> p q) ('> r ('> p q)))"               "Anderson and Belnap, basis 1, axiom 2"
=wishlist "('> ('> p ('> q r)) ('> ('> p q) ('> p r)))" "Anderson and Belnap, basis 1, axiom 3"

#          --- Theorems ---

# Wish list theorem: Anderson and Belnap, basis 1, axiom 2
3: ('> ('> p q) ('> r ('> p q)))                      # Condensed detachment, inference line 2 with line 1

# Wish list theorem: Anderson and Belnap, basis 1, axiom 1
4: ('> p p)                                           # Condensed detachment, inference line 1 with line 1

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

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

# Final proof had 18 lines (16 steps) [work: 421]
# ------------------ End proof --------------
```