# Prove ∀w(∀v((v=w∧φ(v))⇔φ(w)))

In this math question of mine, an answer pointed me to this theorem:

∀w(∀v((v=w∧φ(v))⇔φ(w)))

which in turn, the answerer stated, implies another theorem:

∃v(v=t∧φ(v))⇔φ(t)

which was the fact I needed for my proof.

However, how would one prove this first theorem? The book Axiomatic Set Theory by Patrick Suppes, which has been a great resource for me, proves a similar result `y∈{x:ψ(x)}⇔ψ(y)` on page 34; however, as far as I know, the particular result I'm looking for isn't answered in this book. Can anyone point me to a good book where this is proved? Thanks!

• It just occurred to me that I might have misread your question. Do you want to know how to prove ∀w(∀v((v=w∧φ(v))⇔φ(w)))? – Dennis Oct 19 '15 at 4:32
• @Dennis Yes, my apologies, my question wasn't clear. I mean to ask about the result `∀w(∀v((v=w∧φ(v))⇔φ(w)))` - where can I find this proved?. – Mathemanic Oct 19 '15 at 4:48
• I think I figured out the problem, but before I edit the answer, did you mean for the final operator in ∀w(∀v((v=w∧φ(v))⇔φ(w))) to be a biconditional? In the question you cite, the answer contains this: ∀w∀v((v=w∧φ(v))⟹φ(w)), but not your formula with a biconditional. (Incidentally, the conditional version is valid; once you change the conditional to a biconditional, however, it becomes invalid. – Dennis Oct 19 '15 at 5:11
• Yes the answer says `∀w(∀v((v=w∧φ(v))⇒φ(w)))`, but I think `∀w(∀v((v=w∧φ(v))⇔φ(w)))` (stronger) should also be true, isn't it? – Mathemanic Oct 19 '15 at 5:14
• I tried to clarify my thoughts, but once again I'm doing so at 3 am.... So, if something doesn't make sense then push back, because I might have messed something up. – Dennis Oct 20 '15 at 6:43

Well, it's late at night so I'm sure I'm going to repeat past mistakes and screw something up here. But let's give it a try.

∀w(∀v((v=w∧φ(v))⇔φ(w)))

From there we just need to discharge the outermost quantifier, instantiating to the term "t" (assuming we have such a term laying around):

∀v((v=t∧φ(v))⇔φ(t)))

Then we instantiate once more:

(r=t∧φ(r))⇔φ(t)

Finally, we existentially generalize:

∃v(v=t∧φ(v))⇔φ(t)

To a sleep-deprived version of me, that seems like what you're after. If I messed something up, lemme know and I'll revisit the question with a clearer head.

## Update

Ok, so I've typeset proofs of each of the principles (the conditional and the biconditional versions) as tree proofs in the style of Graham Priest's Introduction to Non-Classical Logic. Let me know if you have problems understanding them.

First the conditional, which I prove via reductio ad absurdum by assuming its negation: Since the proof terminates in a contradiction (a is both φ and not-φ), the negated conditional leads to contradiction and so our original conditional is valid.

Ok, so the conditional is valid, what about the bicondtional? Again, I don't think it is valid. Consider the following attempted proof: Now, the left hand branch leads to contradiction and so closes. The right hand branch, on the other hand, involves no contradictions and so the negation of the biconditional isn't invalid. But if the negation of the biconditional isn't invalid then the biconditional isn't valid.

The problem is the right-to-left side of the biconditional, since if we start off assuming that b is φ that doesn't guarantee that b is the only object in the domain. If there's another object a that is not identical to be, then though b is φ, the consequent of the right-to-left side comes out false since a is not identical to b.