forcing:solexpanuni1 [WikiMat]

Iremos utilizar uma indução na complexidade, assim o conjunto $F$ dado por todas as fórmulas pode ser escrito da forma $F = \bigcup_{n\in \omega} F_n$, sendo $F_0$ as fórmulas atômicas e $F_{n+1} = F_n \cup \{\neg\varphi : \varphi \in F_n\}\cup\{\varphi \wedge \phi:\varphi,\phi \in F_n\}\cup\{\exists x \varphi : \varphi \in F_n\}$, assim supondo como hipótese de indução a validade para $F_n$, vamos mostrar para $F_{n+1}$, vamos separar por partes:
    *Começando pelo $F_0$:
        *$\varphi \in F_0$ da forma $\varphi(x) = x \in y$(os outros casos são análogos), supondo a validade de $\varphi(x)$.
        *Assim, como $x \in y$, então $[\![\check{x} \in \check{y}]\!]_2= 1$ e portanto $[\![ \varphi(\check{x})]\!]_2= 1$.
        *Supondo agora $[\![ \varphi(\check{x}])\!]_2= 1$ temos que $x \in y$, pois $[\![\check{x} \in \check{y}]\!]_2= 1$, pois se $x \notin y$ teríamos que $[\![\check{x} \in \check{y}]\!]_2= 0$.
        *Valendo portanto para $F_0$.
    *Caso $\neg$:
        *Se $\varphi \in F_{k+1}$ é tal que $\varphi \in F_k$, então temos o resultado pela hipótese de indução.
        *Se $\varphi \in F_{k+1}$ é tal que $\varphi(v_1,\dots,v_n)= \neg\phi(v_1,\dots,v_n)$ com $\phi \in F_k$, e pela hipótese de indução vale $\phi$.
        *Supondo a validade de $\varphi(x_1,\dots,x_n)$, ou seja, vale $\neg\phi(v_1,\dots,v_n)$, com isso  $[\![\phi(x_1,\dots,x_n)]\!]_2= 0$, assim $[\![\neg\phi(x_1,\dots,x_n)]\!]_2= 1$ e $[\![\varphi(x_1,\dots,x_n)]\!]_2= 1$.
    *Caso $\wedge$:
        *Se $\varphi \in F_{k+1}$ é tal que $\varphi(v_1,\dots,v_n)= \phi(v_1,\dots,v_n)\wedge\psi(v_1,\dots,v_n)$ com $\phi,\psi \in F_k$, e pela hipótese de indução vale $\phi$ e $\psi$.
        *Supondo que vale $\varphi(x_1,\dots,x_n)$ assim como vale $\phi(v_1,\dots,v_n)\wedge\psi(v_1,\dots,v_n)$, então valem $\phi(v_1,\dots,v_n),\psi(v_1,\dots,v_n)$ e assim $[\![\phi(\check{v_1},\dots,\check{v_n})]\!]_2= 1=[\![\psi(\check{v_1},\dots,\check{v_n)}]\!]_2$ e portanto $[\![\varphi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1$.
        *Supondo que vale $[\![\varphi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1$ temos que $[\![\phi(\check{x_1},\dots,\check{x_n})]\!]_2[[\psi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1$, assim $[\![\psi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1 = [\![\phi(\check{x_1},\dots,\check{x_n})]\!]_2$ e pela hipótese de indução valem $\phi(x_1,\dots,x_n)$ e $\psi(x_1,\dots,x_n)$, ou seja, vale $\varphi(x_1,\dots,x_n)$.    
     *Caso $\exists y$:
        * Suponha $\varphi \in F_{k+1}$ tal que $\varphi(v_1,dots,v_n) = \exists y \phi(y,v_1,\dots,v_n)$ com $\phi \in F_k$ e assim por hipótese de indução temos que $\phi(x,x_1,\dots,x_n) \iff [\![\phi(\check{x},\check{x_1},\dots,\check{x_n})]\!]_2 = 1$.
        * Suponha que vale $\varphi(x_1,dots,x_n)$, logo vale $\exists y \phi(y,x_1,\dots,x_n)$, portanto existe $x$ tal que vale $\phi(x,x_1,\dots,x_n)$, com isso segue que $[\![\phi(\check{x},\check{x_1},\dots,\check{x_n})]\!]_2 = 1$, então $[\![\exists y\phi(y,x_1,\dots,x_n)]\!]_2 = 1$ e portanto $[\![\varphi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1$.
        * Suponha $[\![\varphi(\check{x_1},\dots,\check{x_n})]\!]_2 = 1$, assim $[\![\exists\phi(y,x_1,\dots,x_n)]\!]_2 = 1$, portanto existe um nome $l$ de maneira que $[\![\phi(l,\check{x_1},\dots,\check{x_n})]\!]_2 = 1$, assim existe um nome $x$ tal que $[\![\check{x} = l]\!]_2 = 1$ e segue $[\![\phi(\check{x},\check{x_1},\dots,\check{x_n})]\!]_2 = 1$ e pela hipótese de indução, vale $\phi(x,x_1,\dots,x_n)$, com isso vale $\exists y \phi(y,x_1,\dots,x_n)$ e portanto vale $\varphi(x_1,\dots,x_n)$. <wrap right>$\square$</wrap>