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

- 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.native.html

© Copyright 2009 by John Halleck, All Rights Reserved.

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