# proof that weak axiom of pairing and axiom schema of specification imply axiom of pairing

as the title says I am trying to give a (nearly, but not fully formal) proof that the weak axiom of pairing (i.e. $$\forall x \forall y \exists p: x \in p \wedge y \in p$$) together with a suitable instance of the axiom schema of specification does imply the axiom of pairing. I haven't found a suitable instance yet, so this would be the first step to take.

Here is a 'nearly, but not fully, formal proof' (OK, it is fully formal, but it is not fully completed):

• What software is that? – J.G. Jan 12 at 18:46
• @J.G. It's called 'Fitch' .. it comes with the book "Language, Proof, and Logic" – Bram28 Jan 12 at 19:14
• This software seems awesome! (Though I don't fully understand the notions there.) Thank you for your reply! – Studentu Jan 13 at 18:10
• @Studentu The 'Fitch' system is actually a fairly well known and well-used system for creating fully formal proofs. Here is a list with all the rules: math.mcgill.ca/rags/JAC/124/Rules-Strategy-b.pdf – Bram28 Jan 13 at 18:21
• @Studentu Cool. You're welcome! :) – Bram28 Jan 15 at 1:31

Given $$x,y$$, let $$p$$ be such that $$x\in p\land y\in p$$. Then $$\{x,y\}=\{\,t\in p\mid t=x\lor t=y\,\}$$.

Fix $$x,y$$ and take $$p$$ such that $$x, y \in p$$. Now take the formula $$\Phi = ( z = x \lor z = y)$$ and apply the axiom of specification on $$p$$.