A4P3

[bmk]

I'm wondering how we get rid of the ∃ quantifier. I don't see it used
in any of the axioms, so do we make some kind of assumption? I would
assume that ∀x would also imply ∃x, but not really sure how it would
help, or if it would at all.

[Curtis Bright]

I'm wondering how we get rid of the ∃ quantifier. I don't see it used in
any of the axioms, so do we make some kind of assumption? I would assume
that ∀x would also imply ∃x, but not really sure how it would help, or
if it would at all.

Consider "∃x.A" as shorthand for "~∀x.~A".

Curtis