1
$\begingroup$

I would like to prove that axiom of specification and axiom of extensionality implies that set constructed from axiom of specification is unique. I understand the arguments given by words but I would like to practice and prove it using predicate logic and inference rules.

I would be happy if you could help or hint me about how to prove a specific part that I am stuck with. I will show you my reasoning below. I would also appreciate if there would be some comments on how to make proof easier or more readable.

I want to show that for all formula $\phi$ assumptions $\forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ and $\forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ prove that $\forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$.

My sketch of the proof proceeds as follows.

$1. \forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (premise)

$2. \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 1)

$3. \exists y : \forall z: (z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 2)

$4. \forall z: (z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $b$)

$5. \forall z: (z \in c \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $c$)

$6. d \in b \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 4)

$7. d \in c \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 5)

$8. d \in c \iff d \in b$ (modus ponens on 6 and 7 using the following tautology: $(p \iff q) \land (q \iff r) \to (p \iff r)$)

$9. \forall z: (z \in c \iff z \in b)$ (universal generalization from 8 because $d$ was arbitrary)

$10. \forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ (premise)

$11. \forall y: (c = y \iff (\forall z:(z \in c \iff z \in y)))$ (universal instantiation from 10)

$12. c = b \iff (\forall z: (z \in c \iff z \in b))$ (universal instantiation from 11)

$13. c = b$ (modus ponens from 9 and 12 using the following tautology: $p \land (p \iff q) \to q$)

Here is the point I get stuck because I would like to prove for uniqueness that $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z)) \to r = b$ but from step 13 I (at least I think so) can prove only existence because $b$ and $c$ were not arbitrary but specifically chosen (kind of).

Let us assume that I have proven $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b)$ as step 100.

$101. \forall z:(z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b))$

(modus ponens from 4 and 100)

$102. \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$

(existential generalization of 101)

$103. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \iff \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$

(tautology due to the definition of "exists unique")

$104. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (modus ponens from 103 and 104 using the following tautology: $p \land (p \iff q) \to q$)

$105. \forall x: \exists! y: \forall z:(z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 104 due to the fact that $a$ was arbitrary)

$106. \forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 105 due to the variables $w_1, ..., w_n$ being arbitrary)

This completes the proof. Any suggestions are very welcomed.

$\endgroup$
  • 1
    $\begingroup$ Regarding readibility, you can omit $w_1, \ldots, w_n$; they are needed for "generailty" but add nothing to the proof. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '18 at 13:01
  • 1
    $\begingroup$ In steps 6 and 7 you have to replace also the rightmost $z$ with $d$. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '18 at 13:03
  • $\begingroup$ Probably, the startegy must be: let $c$ be such that $∀z (z∈c ⟺ (z∈a ∧ ϕ(z)))$. Now assume that $\exists y [∀z (z∈y ⟺ (z∈a ∧ ϕ(z))) \land y \ne c]$. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '18 at 13:14
  • 1
    $\begingroup$ Let $c$... you have it already in 5. Tt is the "gist" of existential instantiation: having proved that $\exists x Px$ we call it $c$ and we have $Pc$. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '18 at 15:23
  • 1
    $\begingroup$ You can see e.g. Mendelson, page 34. $\endgroup$ – Mauro ALLEGRANZA Mar 18 '18 at 15:46
1
$\begingroup$

An attempt to re-structure the proof...

  1. $∀x ∃y ∀z (z∈y⟺(z∈x ∧ ϕ(z)))$ --- axiom

2.-3. $∃y ∀z (z∈y⟺(z∈a ∧ ϕ(z)))$ --- universal instantiation from 1

  1. $∀z (z∈b⟺(z∈a ∧ ϕ(z)))$ --- existential instantiation from 3, for some $b$

4a. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- new premise

  1. $∀z(z∈c⟺(z∈a∧ϕ(z))) ∧ d≠b$ --- existential instantiation from 4a, for some $c$

5a $∀z(z∈c⟺(z∈a∧ϕ(z)))$ --- from 5. by taut: $(p \land q) \to p$ and mp

5b. $c≠b$ --- from 5. by taut: $(p \land q) \to q$ and mp

5c. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to \lnot (c=b)$ --- from 5b by taut: $p \to (q \to p)$ and mp

  1. $d∈b⟺(d∈a ∧ ϕ(d))$ --- from 4

  2. $d∈c⟺(d∈a ∧ ϕ(d))$ --- from 5

  3. $d∈c ⟺ d∈b$ --- from 6 and 7

  4. $∀z (z∈c⟺z∈b)$ --- from 8 by universal generalization

  5. $c=b$ --- from 9 by extensionality

  6. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to (c=b)$ --- from 4a and 10 by Deduction Th, discharging premises 4a

  1. $\lnot ∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- from 5c and 11 and taut: $(p \to \lnot q) \to [(p \to q) \to \lnot p]$ (ex falso)
  1. $∀y[∀z(z∈y⟺(z∈a∧ϕ(z))) \to y=b]$ --- from 12 by equivalence for quantifiers and taut: $\lnot (p \land \lnot q) \Leftrightarrow (p \to q)$
$\endgroup$
  • $\begingroup$ Thanks! It really helped! $\endgroup$ – Daniels Krimans Mar 19 '18 at 19:24

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.