Problema com a enumeração de fórmulas
Deixei $P_0, P_1, P_2, ...$ ser uma enumeração de todas as fórmulas lógicas com uma variável livre $n$(contáveis, pois são sequências finitas de um alfabeto contável). Deixei$Q(n) \iff \lnot P_n(n)$. Para qualquer$n$, $Q$ não é $P_n$ porque eles não concordam com $n$. Mas$Q$é uma fórmula lógica, por isso deveria estar na enumeração ...
O que está acontecendo?
Respostas
Isso se resumirá ao seguinte: qual é a definição precisa de "fórmula lógica?" A questão é que embora o$Q$ que você descreveu é definitivamente "significativo", é de maior complexidade em certo sentido do que qualquer um dos $P_i$s. Quando definimos uma noção precisa de "fórmula lógica" e uma enumeração de tal, por exemplo, "fórmula de primeira ordem na linguagem da aritmética" ordenada lexicograficamente por meio de alguma ordem razoável nos símbolos envolvidos, o correspondente$Q$ acabará não sendo exprimível por uma fórmula nesse sentido particular.
Para um exemplo concreto de como isso acontece, consulte, por exemplo, o teorema da indefinição de Tarski . E compare isso com "paradoxos de expressão" semelhantes: o paradoxo de Berry, o paradoxo de Richard e o paradoxo de Grelling.
É importante distinguir entre strings que representam fórmulas válidas e as próprias fórmulas.
Veja o seguinte:
- Paradoxo de Richard (o paradoxo e uma explicação)
- Teorema da indefinição de Tarski (não há maneira de codificar a verdade de uma fórmula em um sistema lógico consistente)
- Teorema da incompletude de Gõdel (a comprovação pode ser codificada, mas é diferente da verdade)