Is it necessary to explicitly state that $\lnot (q \notin X)$ is equivalent to $q \in X$ when writing a proof?

Question

In a proof I am trying to write, I have shown that $q \in X$ and $(q \notin X) \lor (Y= \emptyset)$ are both true. Is it necessary to explicitly state $\lnot (q \notin X)$ is true in order to use the disjunction elimination to get $Y = \emptyset$, or can I assume that it is obvious?

Answer 1

There is no correct answer to your question, since it all depends on what kind of proof you're writing, who the written proof is aimed at, and (if it's part of an assessment) what the expectations of you and/or assessment criteria are.

For example:

• If you're writing a formal axiomatic proof which keeps track of things like disjunction elimination, then you should probably also keep track of your use of double negation as well. There is no 'obvious' in axiomatic proofs, there are only the axioms and rules of inference!

• If you're writing an informal proof, where it's assumed that the reader can fill in gaps where the details required to fill the gaps are glaringly obvious, then I'd say it's fine to omit this particular detail.

• If this is part of a larger proof and the intended audience is expected to have a good knowledge of elementary set theory, then you have probably already included far too much detail in mentioning disjunction elimination and the like.

If you're writing a proof as part of an assessment which is testing your ability to apply axiomatic reasoning (which is what I suspect is the case), then the first example I gave probably applies and I'd recommend that you include it.

Answer 2

This is a somewhat subjective thing, so it's difficult to have a definitive answer. Here is my personal take: it depends on the point of your exercise. If the point of your current book / chapter / exercise is to be explicit about every single logical step, then yes you would need to state that deduction explicitly. If the point is almost anything else, then it may be assumed as obvious, and you will not have to use terms like "disjunction elimination".

If this isn't an exercise but rather an original proof, then the point of the proof is to convince other mathematicians through your writing that your theorem is true. They will be able to follow your logic without adding in that extra step, as long as your writing is clear enough.