Topologia e conjuntos em exercícios

===== Teorema da incompletude de Gödel =====

<WRAP tip>
Provavelmente vai ajudar você saber os resultados da [[lista:enumerabilidade|lista de enumerabilidade]]. Também vamos assumir que você já mexeu com alguma linguagem de programação.
</WRAP>

<WRAP tip>
Vários exercícios terão coisas como "escreva um programa que faça...". Não é o objetivo do exercício que você realmente faça isso - apenas que se convença que tal programa pode ser feito.
</WRAP>

**~~#~~** Fixe uma linguagem de programação de sua escolha. Vamos chamá-la de $P$.

**~~#~~** Note que a quantidade de programas possíveis de serem feitos em $P$ é enumerável.<wrap tip>[[dica:quantidadePrograma|Dica]]</wrap>

<WRAP tip>
Seja $f: \mathbb N \rightarrow \{0, 1\}$. Vamos dizer que $f$ é uma {{entry>função/computável;função computável}} se existe um programa feito na linguagem $P$ que, ao receber o valor $n$, devolve $f(n)$.
</WRAP>

**~~#~~** Fixe $f: \mathbb N \rightarrow \{0, 1\}$ função não computável (pois é, em particular, para fazer exercício você tem que provar que existem funções não computáveis - o que já é bacana por si só). Mas para o que vai vir pela frente, você precisa de fato definir a função não computável. Faça isso usando as funções computáveis.<wrap tip>[[dica:naoComputavel|Dica]]</wrap>.

<WRAP info>
Vamos chamar de uma {{entry>teoria}} uma coleção de axiomas e algumas {{entry>regra de inferência; regras de inferência}}. Informalmente, uma regra de inferência é uma maneira de se "obter" afirmações a partir de anteriores. Por exemplo, uma possível (e bastante comum) regra é a que diz que a partir das afirmações "$A \rightarrow B$" e "$A$", obtemos a afirmação "$B$" (essa regra é conhecida por {{entry>modus ponens}}). Outro exemplo é a regra de substituição: se temos "$\varphi(x)$" e temos que "$x = y$", então temos "$\varphi(y)$", onde $\varphi$ é uma propriedade qualquer. Ao fixar uma teoria, também estamos fixando os símbolos que podem ser usados nas afirmações (em geral, são coisas como $\rightarrow$, $\forall$, $v_1$, etc).
</WRAP>

<WRAP tip>
Vamos fixar para o decorrer desta lista uma teoria $T$ que seja "rica" o suficiente para que possamos definir a $f$ fixada acima (ZFC por exemplo serve. Mas tem coisas bem mais pobres que também servem). 
</WRAP>

<WRAP info>
Fixada uma teoria, uma demonstração nada mais é que uma sequência $\varphi_1, ..., \varphi_n$ de fórmulas (afirmações) onde cada $\varphi_k$ é um axioma ou existem $\varphi_i$'s com $i < k$ de forma que $\varphi_k$ é obtida a partir de uma das regras de inferência da teoria a partir das $\varphi_i$'s. 
</WRAP>

**~~#~~** Faça um programa $Formulas$ que gere todas as fórmulas possíveis.

**~~#~~** Faça um programa $Provas$ em $P$ tal que $Provas$ gere todas as possíveis demonstrações de $T$. Não se preocupe em fazer com que $Provas$ gere apenas as demonstrações - ele pode gerar bastante lixo (apenas queremos que ele gere todas as demonstrações). 

**~~#~~** Melhore (se necessário) o programa $Provas$ de maneira que ele receba um $n \in \mathbb N$ e devolva uma sequência de símbolos presentes em $T$. Faça isso de maneira que para qualquer demonstração, exista um $n$ tal que tal demonstração é $Provas$ aplicado a $n$.

**~~#~~** Faça um outro programa, chamado $EhUmaDemonstracao$ que recebe uma sequência de símbolos da teoria $T$. O programa retorna $1$ se tal sequência é uma demonstração e $0$ caso contrário.

**~~#~~** Melhore o progama $EhUmaDemonstracao$ de maneira que ele receba dois parâmetros: uma sequência de símbolos e uma afirmação $\varphi$ de $T$. Daí ele deve retornar $1$ se a sequência é uma demonstração para $\varphi$ ou $0$ caso contrário (uma demonstração para $\varphi$ nada mais é que uma demonstração cuja última afirmação é a própria $\varphi$).

<WRAP info>
Dizemos que uma teoria é {{entry>teoria/completa; completa}} se, para toda afirmação $\varphi$ existe uma demonstração para $\varphi$ ou uma para $\neg \varphi$ (negação de $\varphi$). 
</WRAP>

**~~#~~** Suponha $T$ completa. Mostre que existe um programa $Provou$ que recebe uma afirmação de $T$ e retorna $1$ se ela admite uma demonstração e $0$ se $\neg \varphi$ admite uma demonstração (se por algum acaso, tanto $\varphi$ como $\neg \varphi$ admitirem demonstrações, ela retorna $0$ ou $1$ sem problemas). Para que você precisou da hipótese de $T$ ser completa?

**~~#~~** Note que se $T$ é completa, para cada afirmação do tipo $f(n) = 1$ ou $f(n) = 0$ ($f$ é a fixada acima), existe uma demonstração para $f(n) = 1$ ou uma para $f(n) = 0$. 

<WRAP info>
Dizemos que uma teoria é {{entry> teoria/consistente; consistente}} se não existe uma afirmação $\varphi$ tal que existam provas para $\varphi$ e para $\neg \varphi$. 
</WRAP>

**~~#~~** Suponha $T$ completa e consistente. Note que, para cada afirmação do tipo $f(n) = 1$, ou existe uma demonstração para ela, ou existe uma demonstração para $f(n) \neq 1$, mas não ambos os casos simultaneamente.


**~~#~~** Suponha $T$ completa e consistente. Faça um programa que, dado $n$, calcule $f(n)$. Note que isso é uma contradição com o fato de $f$ não ser computável.

<WRAP tip>
Resumindo, mostramos que, se $T$ é uma teoria tal que:
  - é suficientemente rica para podermos definir $f$
  - consistente
  - completa
Chegamos a uma contradição. Desta forma, não existe uma teoria rica o suficiente para definir $f$, que não prove contradições e que prove ou refute qualquer afirmação.
</WRAP>

**~~#~~** Mostre que se $T$ é tal que podemos aplicar o teorema feito nesta lista, não adianta acrescentarmos algum axioma a ela que ela vai continuar sendo incompleta (isto é, continuará tendo alguma afirmação $\varphi$ tal que ela não prova $\varphi$ nem $\neg \varphi$).

<WRAP tip>
  * Uma maneira de formalizar a parte "existe um programa que faça tal coisa" é via máquinas de Turing.
  * Deixamos alguns "probleminhas" de fora: por exemplo, se a lista de axiomas de $T$ for infinita (ou a lista de regras de inferência o for), poderia ser que os programas aqui apresentados nunca terminassem (é um exercício descobrir o motivo) e isso impossibilitaria seguir como aqui (outro exercício). Mas se você fixou algum caso "concreto", isso não deve ter ocorrido - apesar que a lista dos axiomas de ZFC é infinita. Isso se corrige pelo fato de, apesar deles serem infinitos, são de "finitos tipos". Na verdade, poderíamos definir que uma teoria é "axiomatizável" se ela possui uma lista de axiomas para o qual é possível fazer os programas aqui apresentados.
</WRAP>

<WRAP tip>
Essa lista foi inspirada em [[http://arxiv.org/abs/1409.5944v1|"Gödel for Goldilocks: A Rigorous, Streamlined Proof of Gödel's First Incompleteness Theorem, Requiring Minimal Background"]] de Dan Gusfield.
</WRAP>
Topologia e conjuntos em exercícios

Ferramentas do usuário

Ferramentas do site

Ferramentas da página
