Added .gitignore, updated & commented prepositional logic axioms.HEADmaster

3 files changed, 57 insertions, 6 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..8e94089
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.pyc
+*~
+
diff --git a/pax_def/pred-set-eq.ghi b/pax_def/pred-set-eq.ghi
index 16b532d..b1f16d5 100644
--- a/pax_def/pred-set-eq.ghi
+++ b/pax_def/pred-set-eq.ghi
@@ -13,17 +13,42 @@ term (class (cv set))
 
 term (wff (= class class))
 
+# Axiom of Equality
 stmt (ax-8 () () ((-> (= (cv x) (cv y)) 
 		      (-> (= (cv x) (cv z)) (= (cv y) (cv z))))))
+
+# Axiom of Existence
 stmt (ax-9 () () ((-. (A. x (-. (= (cv x) (cv y)))))))
-stmt (ax-10 () () ((-> (A. x (= (cv x) (cv y))) (-> (A. x ph) (A. y ph)))))
-stmt (ax-11 () () ((-> (-. (A. x (= (cv x) (cv y)))) 
-		       (-> (= (cv x) (cv y)) 
-			   (-> ph (A. x (-> (= (cv x) (cv y)) ph)))))))
+
+# Old version of ax-10, redundant.
+#stmt (ax-10o () () ((-> (A. x (= (cv x) (cv y))) (-> (A. x ph) (A. y ph)))))
+
+# Axiom of quantifier substitution
+stmt (ax-10 () () ((-> (A. x (= (cv x) (cv y))) (A. y (= (cv y) (cv x))))))
+
+# Old version of ax-11, redundant.
+#stmt (ax-11o () () ((-> (-. (A. x (= (cv x) (cv y))))
+#		         (-> (= (cv x) (cv y))
+#			     (-> ph (A. x (-> (= (cv x) (cv y)) ph)))))))
+
+# Axiom of Variable Substitution
+stmt (ax-11 () () ((-> (= (cv x) (cv y)) 
+                       (-> (A. y ph) 
+                           (A. x (-> (= (cv x) (cv y)) ph))))))
+
+# Axiom of Quantifier Introduction (1)
+# Hint: Some things can be proven by showing they hold in both the case
+# (A. z (= (cv z) (cv x))) and the case (-. (A. z (= (cv z) (cv x)))).
 stmt (ax-12 () () ((-> (-. (A. z (= (cv z) (cv x))))
 		       (-> (-. (A. z (= (cv z) (cv y)))) 
 	                   (-> (= (cv x) (cv y)) (A. z (= (cv x) (cv y))))))))
+
+# Note, ax-16 is redundant given ax-17 (& the rest of the predicate/
+# propositional axioms). However, ax-17 is also 'logically redundant'
+# (via a meta proof) given ax-16. We keep them both here.
 stmt (ax-16 ((x y)) () ((-> (A. x (= (cv x) (cv y))) (-> ph (A. x ph)))))
 
+# Equivalence for classes, used in well-definedness proofs for class
+# definitions with dummy variables
 equiv (class_equiv () ((= A B)) (A B))
 
diff --git a/pax_def/pred-set-min.ghi b/pax_def/pred-set-min.ghi
index 94ab109..663592f 100644
--- a/pax_def/pred-set-min.ghi
+++ b/pax_def/pred-set-min.ghi
@@ -8,10 +8,33 @@ var (set x y z w v u)
 
 term (wff (A. set wff))
 
+# We comment out some older versions of axioms 5 and 6.
+# stmt (ax-5 () () ((-> (A. x (-> (A. x ph) ps)) (-> (A. x ph) (A. x ps)))))
+# stmt (ax-6 () () ((-> (-. (A. x (-. (A. x ph)))) ph)))
+
+# Axioms ax-5, ax-6, ax-7, ax-gen, and ax-17 are all consistent
+# with an interpretation in which (A. x ph) evaluates to True
+# regardless of ph and x.  That's obviously not the interpretation
+# of (A. x ph) that we want.  Metamath does not include ax-4 among
+# its axioms of predicate logic, but its proof ax4 in Metamath requires
+# the axioms concerning equality, which we do not introduce yet.
+# (Specifically, the Axiom of Existence, (-. (A. x (-. (= (cv x) (cv y)))))
+# is inconsistent with the above interpretation.)
+# So, we keep ax-4 here.
+
+# Axiom of Specialization
 stmt (ax-4 () () ((-> (A. x ph) ph)))
-stmt (ax-5 () () ((-> (A. x (-> (A. x ph) ps)) (-> (A. x ph) (A. x ps)))))
-stmt (ax-6 () () ((-> (-. (A. x (-. (A. x ph)))) ph)))
+
+# Axiom of Quantified Implication
+stmt (ax-5 () () ((-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))))
+# Axiom of Quantified Negation
+stmt (ax-6 () () ((-> (-. (A. x ph)) (A. x (-. (A. x ph))))))
+
+# Axiom of Quantifier Commutation
 stmt (ax-7 () () ((-> (A. x (A. y ph)) (A. y (A. x ph)))))
+# Rule of Generalization
 stmt (ax-gen () (ph) ((A. x ph)))
 
+# Axiom of Quantifier Introduction (2)
 stmt (ax-17 ((ph x)) () ((-> ph (A. x ph))))
+