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 polish

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:16:17 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: Cpp                                                # Axiom 1
  2: CCpqCrCpq                                          # Axiom 2
  3: CCpCqrCCpqCpr                                      # Axiom 3

#          --- Wish List ---

      =wishlist "CpCqq"           "EFHW 2base1 Axiom 1"
      =wishlist "CCpCqrCCpqCsCpr" "EFHW 2base1 Axiom 2"

#          --- Theorems ---

# Wish list theorem: EFHW 2base1 Axiom 1
  4: CpCqq                                              # Condensed detachment, inference line 2 with line 1

  5: CpCCqrCsCqr                                        # Condensed detachment, inference line 2 with line 2
  6: CCpCqrCpCsCqr                                      # Condensed detachment, inference line 3 with line 5
  7: CpCCqCrsCCqrCqs                                    # Condensed detachment, inference line 2 with line 3
  8: CCpCqCrsCpCCqrCqs                                  # Condensed detachment, inference line 3 with line 7
  9: CCpqCCrpCrq                                        # Condensed detachment, inference line 8 with line 2
 10: CCCpqCrpCCpqCrq                                    # Condensed detachment, inference line 3 with line 9
 11: CCCCpqCprsCCpCqrs                                  # Condensed detachment, inference line 10 with line 7

# Wish list theorem: EFHW 2base1 Axiom 2
 12: CCpCqrCCpqCsCpr                                    # 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 polish

# ----------------- Proof: --------------------
# Produced Thu Jul 17 10:48:01 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: CpCqq                                              # Axiom 1

  2: CCpCqrCCpqCsCpr                                    # Axiom 2

#          --- Wish List ---

      =wishlist "Cpp"           "Anderson and Belnap, basis 1, axiom 1"
      =wishlist "CCpqCrCpq"     "Anderson and Belnap, basis 1, axiom 2"
      =wishlist "CCpCqrCCpqCpr" "Anderson and Belnap, basis 1, axiom 3"

#          --- Theorems ---

# Wish list theorem: Anderson and Belnap, basis 1, axiom 1
  3: Cpp                                                # Condensed detachment, inference line 1 with line 1

# Wish list theorem: Anderson and Belnap, basis 1, axiom 2
  4: CCpqCrCpq                                          # Condensed detachment, inference line 2 with line 1

  5: CpCqCrr                                            # Condensed detachment, inference line 4 with line 1
  6: CCCpCqrCpqCsCCpCqrCtCpr                            # Condensed detachment, inference line 2 with line 2
  7: CpCCqCCrrsCtCqs                                    # Condensed detachment, inference line 6 with line 5
  8: CCpCqCCrrsCtCpCuCqs                                # Condensed detachment, inference line 2 with line 7
  9: CpCCqCrsCtCCqrCqs                                  # Condensed detachment, inference line 8 with line 2
 10: CCpCqrCsCCpqCpr                                    # Condensed detachment, inference line 9 with line 1
 11: CCCpqpCrCCpqq                                      # Condensed detachment, inference line 2 with line 3
 12: CpCCCqqrr                                          # Condensed detachment, inference line 11 with line 1
 13: CCpCCqqrCsCpr                                      # Condensed detachment, inference line 2 with line 12
 14: CpCCCCCqqrrss                                      # Condensed detachment, inference line 11 with line 12
 15: CCpCCCCqqrrsCtCps                                  # Condensed detachment, inference line 2 with line 14
 16: CpCCqCCrrsCqs                                      # Condensed detachment, inference line 15 with line 13
 17: CCpCCqqrCpr                                        # Condensed detachment, inference line 16 with line 1

# Wish list theorem: Anderson and Belnap, basis 1, axiom 3
 18: CCpCqrCCpqCpr                                      # Condensed detachment, inference line 17 with line 10

# Final proof had 18 lines (16 steps) [work: 421]
# ------------------ 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])

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

EFHW = AB

AB contains EFHW

Proof that EFHW contains AB

Go to ...