Taking
¬∀x:X.r≡∃x:X.¬r
Is there a way of actually formally proving this? Not implementing it but proving how to go from a negated universal quantifier to a an existential with a negated element...
I understand the logic behind it, I just can't figure out how I can use definitions to exit the negation of the universal and swap it to an existential and negating the middle.
I'm simply conflicted as to whether I would be allowed to directly implement this rule or if I have to prove it. (The question simply says formally proof something, the entire problem would be solved if I simply quote the above rule, follow it with a DeMorgan and a Double Negation)
Thank anybody with any insight on the above.