diff options
Diffstat (limited to 'pax_def/pred-set-min.ghi')
| -rw-r--r-- | pax_def/pred-set-min.ghi | 27 |
1 files changed, 25 insertions, 2 deletions
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)))) + |