# How to check if this proof is valid?

I'm having some doubt if this proof is valid or invalid, especially regarding the `line 4` derived from `line 2`. Do I need to change the letter in there?

``````1. (z)~Fz
∴ ~(z)Fz
Using Indirect proof strategy we assume the opposite i.e.,
2. (z)Fz
3. ∴ ~Fa [from 1; Dropping universal]
4. ∴ Fa [from 2; Dropping universal]
5. ∴ ~(z)Fz [from 2]
``````

And the rule is that if we have a contradiction, our proof is done. Is there any way to check this if it is valid or not?

• 4 is not derived from 2, but from the supposition that (z)Fz, isn't it? Nov 4, 2012 at 12:31

The proof is not valid and it isn't even true. In particular, `(z)Fz` does not imply `Fa` for some `a`. If the universe is empty, `(z)P` is true for any `P` (including both `Fz` and `~Fz`).

If you can assume a non-empty universe, the proof is correct. To demonstrate it mechanically, you should write it out more completely as well-formed formulas and apply transformations like `((P => Q) && ~Q) => ~P` to demonstrate correctness. This usually ends up being a pointlessly tedious exercise after you've done it a few times to verify that it works.

• I have edited the proof in my question to be more clear. So, my question was, Is it correct to drop universal twice without changing the letter or constant like I did?
– cpx
Nov 6, 2012 at 18:20
• You cannot drop universal quantification without knowing your universe is inhabited. Otherwise you can (at least if you have the axiom of choice). Nov 6, 2012 at 18:22
• So, is the proof wrong? I was thinking to change it into something like this Would it be right?
– cpx
Nov 6, 2012 at 18:53
• @cpx - No, that is also wrong. Your statement is not true, so you cannot prove it. You cannot drop universals. All these items are fish: `{}`. (That statement is true.) I have a fish from that set. (Not true.) You need another premise, e.g. that something exists. Nov 6, 2012 at 18:58
• Okay. Even if it is wrong, If we just try to prove it anyhow, those are the steps that we must follow i.e. dropping universals each time with a new letter, right?
– cpx
Nov 6, 2012 at 19:12

I may be missing something here, but I assume we are using "reductio ad absurdum" proof principles here. If so, as I understand it, we assume the opposite of the thing we are trying to prove - instead of the original hypothesis. In your proof, you have conclusions drawn from both the original (3 from 1) and the opposite assumption (4 from 2) - which is always (and obviously, if you think about it a little) going to give you contradictions.

So assuming I have your question right, and understood your proof right, no, it's not valid. The contradiction has to come from assuming ONLY the opposite, not both the original and the opposite.

If I have understood wrong, please explain why, and I'll try to clarify.

• The OP is nowhere assuming ~z(Fz), is it? Nov 5, 2012 at 13:06
• in 1 we have (z)~Fz, in 2 we assume the opposite: (z)Fz But we then draw conclusions from 1 and from 2 in the proof(3 and 4). Can we use conclusions from the original (1) and the opposite (2) in the same proof? That way we can prove anything...
– Ryno
Nov 6, 2012 at 15:09
• But the negation of (z)~Fz is not (z)Fz, but ~(z)~Fz, and this the OP is not using. Rather they are using (z)Fz, which is the negation of ~(z)Fz -- supposing that ~~p iff p -- , which is what they are trying to prove. Nov 6, 2012 at 18:22
• OK, 2 is not the opposite of 1, but the opposite of a conclusion drawn from 1. There are still conclusions being drawn from 1(and the conclusion drawn from it) and from 2(The "opposite" being drawn to prove 1). regardless of the semantics of which part of 1 the opposite comes, 3 and 4 still come from hypotheses we assume in different cases, which is the problem I was raising. If that part isn't right, then I'm still missing a bigger part of this picture.
– Ryno
Nov 7, 2012 at 22:53
• I finally understand... I did understand A reductio, just mis-read the OP somewhat. Sorry it took so long to get my head around that, thanks for keeping at me until I did! :)
– Ryno
Nov 8, 2012 at 15:43