diff options
-rw-r--r-- | .gitignore | 3 | ||||
-rw-r--r-- | pax_def/pred-set-eq.ghi | 33 | ||||
-rw-r--r-- | pax_def/pred-set-min.ghi | 27 |
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)))) + |