Proofs in Equivalence of S5 Systems

• S5 System can be defined in several different ways:
• Before trying to prove the equivalence of differently defined S5 systems, one of the four PC systems has to be chosen for the proof. The following tests are based on S5=KM5.sys and S5=KM4B.sys.

  Table 1
  

  System	Hilbert	Lukasiewicz	Principia	Rosser
  S5=KM5_to_S5=KM4B	2 out of 2 proved in 140 seconds & in 10 seconds	0 out of 2 proved	1 out of 2 proved in 600 seconds	2 out of 2 proved in 30 seconds & in 25 seconds
  S5=KM4B_to_S5=KM5	1 out of 1 proved in 40 seconds	1 out of 2 proved in 130 seconds	1 out of 1 proved in 150 seconds	1 out of 1 proved in 260 seconds

  So, Hilbert based PC system is chosen for all the proofs.

• We picked PC based system S5=KM4B, S5=KM5 and S1-0 based system S5=S1-0M6S3M9B, S5=S1-0M10 and proved the equivalence as follows:

  Table 2 (EP)
  

  To From	KM4B	KM5	S1-0M6S3M9B	S1-0M10
  KM4B	X	0 out of 1 proved	7 out of 12 proved	5 out of 9 proved
  KM5	0 out of 2 proved	X	7 out of 12 proved	5 out of 9 proved
  S1-0M6S3M9B	4 out of 17 proved	5 out of 16 proved	X	0 out of 1 proved
  S1-0M10	0 out of 17 proved	0 out of 16 proved	1 out of 4 proved	X

  Table 3 (Vampire)
  

  To From	KM4B	KM5	S1-0M6S3M9B	S1-0M10
  KM4B	X	1 out of 1 proved	8 out of 12 proved	7 out of 9 proved
  KM5	2 out of 2 proved	X	8 out of 12 proved	6 out of 9 proved
  S1-0M6S3M9B	12 out of 17 proved	11 out of 16 proved	X	0 out of 1 proved
  S1-0M10	15 out of 17 proved	14 out of 16 proved	1 out of 4 proved	X

  Succeeded on
  Computer : rockville.cs.miami.edu
  FreeSwap : 478MB
  SpareCPUs : 1
  NumberOfCPUs : 1
  Model : i686 i686
  SwapInUse : 30MB
  FreeRAM : 272MB
  CPUModel : Intel(R) Pentium(R) 4 CPU 2.00GHz
  RAMPerCPU : 503MB
  OS : Linux 2.6.9-1.667
  CPUSpeed : 1994MHz
  

• Lemmas for unproved theorems:
  • Add proved axioms in TO to FROM as lemmas to prove the rest axioms in TO:
    • In the proof from KM4B to S1-0M10, add "s1_1, s1_2, s1_3, s1_4, m10, adjunction, modus_ponens_strict_implies" to S5=KM4B_to_S5=S1-0M10.lemma.p as lemmas, no more succeeded.
    • In the proof from S5=S1-0M6S3M9B to S5=KM4B.lemma.p, add "modus_tollens, and_1, and_2, implies_1, or_2, equiv_2, axiom_k, axiom_b" to S5=S1-0M6S3M9B_to_S5=KM4B.lemma.p as lemmas, and prove "necessitation, modus_ponens, axiom_4, equiv_1, equiv_3, and_3, or_1, implies_2" S5=S1-0M6S3M9B_to_S5=KM4B.lemma.out. (Proved modus_ponens ,or_1 ,equiv_1).
  • Add unproved axioms in TO to FROM as lemmas to find out the key lemma:
    • Idea:
    • Example:
  • Pick the lemmas from hand proofs(e.g, from S5=KM4B to S5=S1-0M10)
    • According to Leo Simons' "New Axiomatizations of S3 and S4" substitution_strict_equiv can be proved by induction using Theorems 10, 12, 19, 20. So, we proved these four theorems from S5=KM4B.
    • Proved theorem_10,
    • Proved theorem_12,
    • Proved theorem_19,
    • Proved theorem_20,

    Succeeded on
    Computer : yorktown.cs.miami.edu
    

  • Interesting things
    • "definition", "activation" matters, it slows down the prover but not much
    • "=" and "equiv" Formulae encoded in "=" as axioms (or lemmas) quicken the proof process, but they have to be encoded in "equiv" like the rest as conjectures. For example, "~~X=X" is added to system PCHilbert as a lemma, and it is encode as follows: not(not(X)) = X but when we try to prove it from the rest of Hilbert system as a conjecture, it should be encoded in the format as the rest formula: is_a_theorem(equiv(not(not(X)), X))