3
$\begingroup$

I read that the converse of

$\forall a \forall b (\forall c (c \in a \leftrightarrow c \in b) \rightarrow a = b)$

follows from the substitution property of equality.

Therefore I did the following, but I am quite sure this is not right. I would greatly appreciate if someone could point me to how to apply the substitution property.

What I tried to do was:

$ \phi = \forall c (c \in a \leftrightarrow c \in a)$

Now substituting some occurances of unbound $a$ with unbound $b$:

$ \phi' = \forall c (c \in a \leftrightarrow c \in b) $

Using the substitution property:

$ \forall a \forall b (a = b \rightarrow (\phi \rightarrow \phi') ) $

$ \forall a \forall b (a = b \rightarrow (\forall c (c \in a \leftrightarrow c \in a) \rightarrow \forall c (c \in a \leftrightarrow c \in b)) ) $

$ \forall a \forall b (a = b \rightarrow (\forall c \top \rightarrow \forall c (c \in a \leftrightarrow c \in b)) ) $

$ \forall a \forall b (a = b \rightarrow (\top \rightarrow \forall c (c \in a \leftrightarrow c \in b)) ) $

$ \forall a \forall b (a = b \rightarrow \forall c (c \in a \leftrightarrow c \in b)) $

This is the expected converse. But does the procedure make any sense?

Thank you in advance.

$\endgroup$
1
  • $\begingroup$ Nice and brilliant proof idea! $\endgroup$
    – user4414
    Feb 2, 2018 at 23:29

1 Answer 1

2
$\begingroup$

This seems perfectly reasonable. Whether it's a correct derivation in your particular context will depend on the specific rules your system uses (there are many different proof systems), so you will need to check that, but it seems reasonable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.