===== Teorema da incompletude de Gödel ===== 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. 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. **~~#~~** 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.[[dica:quantidadePrograma|Dica]] 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)$. **~~#~~** 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.[[dica:naoComputavel|Dica]]. 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). 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). 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. **~~#~~** 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$). 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$). **~~#~~** 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$. 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$. **~~#~~** 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. 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. **~~#~~** 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$). * 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. 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.