Problème d'énumération des formules
Laisser $P_0, P_1, P_2, ...$ être une énumération de toutes les formules logiques avec une variable libre $n$(dénombrables car ce sont des chaînes finies d'un alphabet dénombrable). Laisser$Q(n) \iff \lnot P_n(n)$. Pour toute$n$, $Q$ n'est pas $P_n$ parce qu'ils ne sont pas d'accord sur $n$. Mais$Q$est une formule logique, elle devrait donc figurer dans l'énumération ...
Que se passe-t-il?
Réponses
Cela reviendra à ce qui suit: quelle est la définition précise de «formule logique»? Le fait est que bien que le$Q$ que vous avez décrit est définitivement "significatif", il est d'une plus grande complexité dans un sens que n'importe lequel des $P_i$s. Lorsque nous définissons une notion précise de «formule logique» et une énumération de celle-ci, par exemple «formule du premier ordre dans le langage de l'arithmétique» ordonnée lexicographiquement via un ordre raisonnable sur les symboles impliqués, le correspondant$Q$ ne sera pas exprimable par une formule dans ce sens particulier.
Pour un exemple concret de la façon dont cela se produit, voir par exemple le théorème d'indéfinissabilité de Tarski . Et comparez cela à des «paradoxes d'expression» similaires: le paradoxe de Berry, le paradoxe de Richard et le paradoxe de Grelling.
Il est important de faire la distinction entre les chaînes représentant des formules valides et les formules elles-mêmes.
Voir ce qui suit:
- Paradoxe de Richard (le paradoxe et une explication)
- Théorème d'indéfinissabilité de Tarski (il n'y a aucun moyen d'encoder la vérité d'une chaîne de formule dans un système logique cohérent)
- Théorème d'incomplétude de Godel (la prouvabilité peut être encodée, mais c'est différent de la vérité)