==== A definição de Forcing ====

<WRAP info>
Chamamos uma ordem $\mathbb{P}$ de um **forcing** se existe $1 \in \mathbb{P}$ tal que $1 \geq p$ para todo $p \in \mathbb{P}$ e, para todo $p,q \in \mathbb{P}$ tais que $q \not \leq p$, existe $p' \leq q$ tal que $p' \perp p.$ Dado $p \in \mathbb{P}$, considere $\downarrow p = \{q \in \mathbb{P}: q \leq p \}$.
</WRAP>

**~~#~~** Se $\mathbb{P}$ possui um menor elemento, então $\mathbb{P}$ é unitária. 

**~~#~~** O conjunto $\{ \downarrow p: p \in \mathbb{P} \}$ forma uma base para uma topologia sobre $\mathbb{P}$.

**~~#~~** Seja $(X,\tau)$ um espaço topológico. Então o conjunto $\{V \subset X: \mathring{\overline{V}} = V\}$ forma uma álgebra completa com $\leq$, $\cdot$, $0$ e $1$ sendo $\subseteq$, $\cap$, $\emptyset$ e $X$, respectivamente, e definindo $U + V \doteq \mathring{\overline{U \cup V}}$ e $-V \doteq \mathring{(X \setminus V)}$ (Lembre-se que os subconjuntos de $X$ que satisfazem $\mathring{\overline{V}} = V$ são chamados de **abertos regulares**).

**~~#~~** Seja $p \in \mathbb{P}$. Se $A \subset \mathbb{P}$ é aberto e $p \in A$, então $\downarrow p \subset A$.

**~~#~~** Dado $p \in \mathbb{P}$, temos que $\downarrow p$ é um aberto regular.

<WRAP info>
Denotamos por $RO(\mathbb{P})$ a álgebra completa dos abertos regulares (ou o completamento) de $\mathbb{P}$. 
</WRAP> 

**~~#~~** A função $\varphi: \mathbb{P} \rightarrow RO(\mathbb{P})$ dada por $\varphi(p) = \downarrow p$ é um isomorfismo de ordem sobre um conjunto denso de $RO(\mathbb{P})$. <wrap tip>[[dica:isotodense|Dica]]</wrap>

**~~#~~** Sejam $A,B$ álgebras de Boole completas. Se existem $a: \mathbb{P} \rightarrow A$ e $b: \mathbb{P} \rightarrow B$ isomorfismos sobre subconjuntos densos em $A$ e $B$, então $A$ e $B$ são isomorfos. <wrap tip>[[dica:unitaryboolean|Dica]]</wrap>

<WRAP info>
Dada $\varphi$ uma fórmula, denotamos por $p \Vdash \varphi$ ($p$ **força** $\varphi$) se $\downarrow p \leq [\![\varphi]\!]$, onde $[\![\cdot]\!]$ é tomado em relação a $RO(\mathbb{P})$.
</WRAP>

**~~#~~** Sejam $p,q \in \mathbb{P}$ e $\varphi$ uma fórmula. Então: 

**~~#.#~~** Se $p \Vdash \varphi$ e $q \leq p$, então $q \Vdash \varphi$.

**~~#.#~~** $p \Vdash ¬\varphi$ se, e somente se, não existe $q \leq p$ tal que $q \Vdash \varphi$. 

**~~#~~** Dadas $\varphi$ e $\psi$ fórmulas, temos:

**~~#.#~~** $p \Vdash \varphi \wedge \psi$ se, e somente se, $p \Vdash \varphi$ e $p \Vdash \psi$.

**~~#.#~~** $p \Vdash \varphi \vee \psi$ se, e somente se, para todo $q \leq p$, existe $r \leq q$ tal que $r \Vdash \varphi$ ou $r \Vdash \psi$.

**~~#.#~~** $p \Vdash \varphi \rightarrow \psi$ se, e somente se, para todo $q \leq p, (q \Vdash \varphi) \Rightarrow (q \Vdash \psi)$. 

**~~#~~** Sejam $p \in \mathbb{P}$ e $\varphi$ fórmula. Então:

**~~#.#~~** $p \Vdash \forall x \varphi(x)$ se, e somente se, para todo $\dot{x}$ nome $p \Vdash \varphi(\dot{x})$. 

**~~#.#~~** $p \Vdash \exists x \varphi(x)$ se, e somente se, para todo $q \leq p$, existem $r \leq q$ e $\dot{x}$ nome tais que $r \Vdash \varphi(\dot{x})$.

**~~#~~** Sejam $p \in \mathbb{P}$, $\varphi$ fórmula e $y$ conjunto. Então:

**~~#.#~~** $p \Vdash \forall x \in \check{y}$ $\varphi(x)$ se, e somente se, para todo $x \in y$ vale $p \Vdash \varphi(\check{x})$.  

**~~#.#~~** $p \Vdash \exists x \in \check{y}$ $\varphi(x)$ se, e somente se, para todo $q \leq p$, existem $r \leq q$ e $x \in y$ tais que $r \Vdash \varphi(\check{x})$.

**~~#~~** Seja $\varphi$ fórmula. Então:

**~~#.#~~** $[\![\varphi]\!] = 0$ se, e somente se, $\not \exists p$ $p \Vdash \varphi$. 

**~~#.#~~** $[\![\varphi]\!] = 1$ se, e somente se, $\forall p$ $p \Vdash \varphi$. 

**~~#~~** Sejam $p \in \mathbb{P}$ e $\varphi$ uma fórmula. Então existe $q \leq p$ tal que $q \Vdash \varphi$ ou $q \Vdash \neg \varphi$. <wrap tip>[[dica:noidea|Dica]]</wrap>

**~~#~~** Sejam $p \in \mathbb{P}$ e $\varphi$ uma fórmula. Se $p \Vdash \varphi$, então $p \not \Vdash ¬\varphi$.