Suppose you're asked to give a formal proof of $\forall x \forall y(x \in \{x,y\})$, where a formal proof is essentially a sequence of invocations of inference rules and appeals to the set theory axioms. Assuming the inference rules of propositional logic and predicate logic are understood, what else do we need to establish to prove this? I guess what I'm saying is that I'm not sure how to manipulate the set literal (if you can call it that) notation. Is $\{x,y\}$ really just shorthand for something else that's easier to manipulate? Perhaps set literal notation is defined by something like "$x\in\{s_1,s_2,\dots,s_n\}$ is an abbreviation for $x=s_1 \vee x=s_2 \vee \dots \vee x=s_n$"? If that were the case, the proof would be very easy to write. So, is this how one would actually define the notation, or am I still missing something?

Note that my background in formal proofs comes from Graeme Forbes' "Modern Logic" and my past math teachers must have considered set literal notation intuitive enough that they didn't have to provide a definition of it as really being an abbreviation or something.

  • $\begingroup$ If the set is defined by enumerating its elements (i.e. Extensionally), then I would indeed use the disjunction as you propose. $\endgroup$ – Bram28 Oct 25 '16 at 3:09
  • $\begingroup$ did someone ask you to prove this? I imagine you can say it's an axiom. Maybe, I'd say for all y {x,y}= {x}U {y} and x in {x}which is a subset of {x}U {y} so x in {x}U {y}. But that seems like avoiding the issue. ... but consider the question might be more about "all y" rather then "x is always". Maybe. I'm not sure it's a legitimate thing to request. I'd put my money that this is true axiomatic ally if not be definition. But I don't know. GOOD question. $\endgroup$ – fleablood Oct 25 '16 at 3:17
  • $\begingroup$ No, I wasn't asked to prove this. When writing an English (not formal) proof for my foundations of computing class, I used the fact that x is a member of {x} without any justification since justifying this isn't necessary for the class. It just got me thinking about how I would handle this if I were to give a formal proof. $\endgroup$ – mathedpotatoes Oct 25 '16 at 3:24
  • $\begingroup$ The set $\{x,y\}$ is defined by $\exists z\forall w(w \in z \leftrightarrow (w=x \vee w=y))$, so just take $w$ to be $x$. It's even simpler to justify $x \in \{x\}$, since $\{x\}$ by definition is $\exists z\forall w (w \in z \leftrightarrow w=x))$. $\endgroup$ – leibnewtz Oct 25 '16 at 3:33
  • $\begingroup$ Then I'd say it's the definition of "element". {x,y} is, by definition, the set whose elements are x and y and therefore x is an element. There's nothing to prove. $\endgroup$ – fleablood Oct 25 '16 at 3:57

You asked, "Is $\{x,y\}$ really just shorthand for something else that's easier to manipulate?"

It's actually shorthand for something else that's harder to manipulate (because it's long and unwieldy).

A formula of the form $\varphi(\{x,y\})$ can be viewed as an abbreviation for

$$(\exists a)\Big(\varphi(a) \land (\forall b)\big(b\in a \iff (b=x\lor b=y)\big)\Big)$$

or for

$$(\forall a)\Big((\forall b)\big(b\in a \iff (b=x\lor b=y)\big)\implies \varphi(a)\Big),$$

which are equivalent over ZF (and, in fact, over much weaker set theories).


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.