Notation: Native | Polish | Psudo Otter | CS

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.

# 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 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])

- Proofs page
- List of Systems
- List of Axioms
- List of Rules
- Logic structures page
- Logic page
- John Halleck's home page
- University of Utah at Salt Lake
- State of Utah

This page is http://www.cc.utah.edu/~nahaj/logic/structures/proofs/c4.polish.html

© Copyright 2009 by John Halleck, All Rights Reserved.

This page was last modified on Wednesday, February 6th, 2009.