=====Axioma da Separação e Axioma das Partes=====

<WRAP info>
**Relembrando:**
  * Sejam $x, y$ nomes. Definimos:
              * $\displaystyle [\![ x \in y ]\!] = \sup_{t \in \text{dom}(y)}y(t)[\![ x = t ]\!]$
              * $\displaystyle [\![ x \subset y ]\!] = \inf_{t \in \text{dom}(x)} (x(t) \Rightarrow [\![ t \in y ]\!])$
              * $[\![ x = y ]\!] = [\![ x \subset y ]\!] [\![ y \subset x ]\!]$

  * Vamos usar a seguinte notação para $a, b \in B$: $a \Rightarrow b = -a + b$.
</WRAP>

<WRAP tip>
O próximo exercício ajuda com a entender a substitução de variáveis:
</WRAP>

**~~#~~** Se $a$ e $b$ são nomes e $\varphi$ é uma fórmula então

**~~#.#~~** $[\![ a=b ]\!] [\![ \varphi(b) ]\!] \leq [\![ \varphi(a) ]\!]$. <wrap tip>[[dica:a|Dica]]</wrap> 

**~~#.#~~** $\displaystyle \sup_c [\![ a=c \wedge \varphi(c) ]\!] = [\![ \varphi(a) ]\!]$. <wrap tip>[[dica:b|Dica]]</wrap>

<WRAP tip>
O próximo exercício ajuda a trabalhar com máximos e mínimos:
</WRAP>

**~~#~~** Mostre que $\displaystyle -\inf_{a \in A} a = \sup_{a \in A} -a$.

<WRAP tip>
O próximo exercício fala como trabalhar com quantificadores restritos:
</WRAP>

**~~#~~** Se $\dot{x}$ é nome e $\varphi$ é uma fórmula (possivemente com parâmetros) então

**~~#.#~~** $\displaystyle [\![ \exists y \in \dot{x} \varphi(y) ]\!] = \sup_{y \in \text{dom}(\dot{x})} \dot{x}(y) [\![ \varphi(y) ]\!]$ <wrap tip>[[dica:2a|Dica]]</wrap>  <wrap help>[[solucao:solsup|Solução]]</wrap>

**~~#.#~~** $\displaystyle [\![ \forall y \in \dot{x} \varphi(y) ]\!] = \inf_{y \in \text{dom}(\dot{x})}(\dot{x}(y)\Longrightarrow [\![ \varphi(y) ]\!])$ <wrap tip>[[dica:2b|Dica]]</wrap>  <wrap help>[[solucao:solinf|Solução]]</wrap>


<WRAP tip>
O próximo exercício é um roteiro para mostrar que se $\varphi$ é uma instância do esquema do axioma de separação então $[\![ \varphi ]\!]=1$.
</WRAP>


**~~#~~** Considere que $\varphi$ é da forma $\forall x \exists v \forall y (y \in v \Longleftrightarrow y \in x \wedge \psi(y)$. Seja $\dot{x}$ nome e considere $\dot{v}$ nome tal que $\text{dom}(\dot{v})=\text{dom}(\dot{x})$ e para todo $y \in \text{dom}(\dot{v})$, $\dot{v}(y)= \dot{x}(y)[\![ \psi(y) ]\!]$.

**~~#.#~~** Mostre que $[\![ \forall y (y \in \dot{v} \Longrightarrow y \in \dot{x} \wedge \psi(y)) ]\!]= 1$. <wrap help>[[solucao:solsep|Solução]]</wrap>

**~~#.#~~** Mostre que $[\![ \forall y (y \in \dot{x} \wedge \psi(y) \Longrightarrow y \in \dot{v}) ]\!]= 1$. <wrap help>[[solucao:solusep|Solução]]</wrap>

**~~#.#~~** Conclua que $[\![ \varphi ]\!]=1$. 


<WRAP tip>
O próximo exercício é um roteiro para mostrar que se $\varphi$ é o axioma das partes então $[\![ \varphi ]\!]=1$:
</WRAP>

**~~#~~** Considere que $\varphi$ é da forma $\forall x \exists y \forall z (z \subset x \Longrightarrow z \in y$). Fixe $\dot{x}$ nome. Considere $\dot{y}$ nome com $\text{dom}(\dot{y})=A^{\text{dom}(\dot{x})}$ tal que para cada $z \in \text{dom}(\dot{y})$, $\dot{y}(z)=[\![ z \subset \dot{x} ]\!]$.
Dado $z$ nome qualquer, considere $\alpha$ nome com $\text{dom}(\alpha)=\text{dom}(\dot{x})$ tal que $\alpha(\beta)=[\![ \beta \in z ]\!] \forall \beta \in \text{dom}(\dot{x})$.

**~~#.#~~** Mostre que $[\![ z\subset \dot{x} \Longrightarrow z = \alpha ]\!]=1$. <wrap help>[[solucao:solpart|Solução]]:</wrap>

**~~#.#~~** Mostre que $[\![ z\subset \dot{x} \Longrightarrow \alpha \in \dot{y} ]\!]=1$. <wrap help>[[solucao:solupart|Solução]]</wrap>

**~~#.#~~** Conclua que $[\![ \varphi ]\!]=1$.