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

# ----------------- Proof: --------------------
# Produced Mon Jan  5 10:20:43 2009
# by the "shotgun" program, version 2009-01-01 0.01.002

# 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)
# ------------------ End proof --------------

# Summary of 2 wish list items proven:
#   (p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r))) # EFHW 2base1 Axiom 2
#   p -> (q -> q) # EFHW 2base1 Axiom 1
```

### Proof that EFHW contains AB

```
# ----------------- Proof: --------------------
# Produced Mon Jan  5 10:22:47 2009
# by the "shotgun" program, version 2009-01-01 0.01.002

# Input from standard input.

# Name of this logical system.
=name C4
# Axiomatic Basis:
=basis     EFHW 2 base 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"

#          --- Axioms ---

1: p -> (q -> q)                            # Axiom 1

2: (p -> (q -> r)) -> ((p -> q) -> (s -> (p -> r)))
# Axiom 2

=lastaxiom

#          --- 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 -> ((r -> r) -> s)) -> (q -> s))
# Condensed detachment, inference line 13 with line 13

15: (p -> ((q -> q) -> r)) -> (p -> r)       # Condensed detachment, inference line 14 with line 1

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

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

# Summary of 3 wish list items proven:
#   (p -> (q -> r)) -> ((p -> q) -> (p -> r)) # Anderson and Belnap, basis 1, axiom 3
#   (p -> q) -> (r -> (p -> q)) # Anderson and Belnap, basis 1, axiom 2
#   p -> p # Anderson and Belnap, basis 1, axiom 1
```