diff options
Diffstat (limited to 'pax_def/pred-set-eq.ghi')
| -rw-r--r-- | pax_def/pred-set-eq.ghi | 33 |
1 files changed, 29 insertions, 4 deletions
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)) |