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