Ferramentas do usuário
Teorema da incompletude de Gödel
Provavelmente vai ajudar você saber os resultados da 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.
1 Fixe uma linguagem de programação de sua escolha. Vamos chamá-la de $P$.
2 Note que a quantidade de programas possíveis de serem feitos em $P$ é enumerável.Dica
Seja $f: \mathbb N \rightarrow \{0, 1\}$. Vamos dizer que $f$ é uma 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)$.
3 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.
Vamos chamar de uma teoria uma coleção de axiomas e algumas 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 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, \ldots, \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.
4 Faça um programa $Formulas$ que gere todas as fórmulas possíveis.
5 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).
6 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$.
7 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.
8 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 é teoria/completa; completa se, para toda afirmação $\varphi$ existe uma demonstração para $\varphi$ ou uma para $\neg \varphi$ (negação de $\varphi$).
9 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?
10 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 é teoria/consistente; consistente se não existe uma afirmação $\varphi$ tal que existam provas para $\varphi$ e para $\neg \varphi$.
11 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.
12 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.
13 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 "Gödel for Goldilocks: A Rigorous, Streamlined Proof of Gödel's First Incompleteness Theorem, Requiring Minimal Background" de Dan Gusfield.
Ferramentas da página
