Points fixes en calculabilité et logique

Cette question a également été publiée sur Math.SE,

/math/1002540/fixed-points-in-computability-nd-logic

J'espère que c'est ok de le poster aussi ici. Sinon, ou si c'est trop basique pour CS.SE, dites-le moi et je le supprimerai.

Je voudrais mieux comprendre la relation entre les théorèmes du point fixe en logique et le $\lambda$ -calcul.

Contexte

1) Le rôle des points fixes dans l'incomplétude et l'indéfinissabilité de la vérité

Autant que je sache, en dehors de l'idée fondamentale d'intérioriser la logique, la clé à la fois des preuves de l'indéfinissabilité de la vérité de Tarski et du théorème d'incomplétude de Goedel est le théorème de point fixe logique suivant , vivant dans une métathéorie constructive et finitiste (j'espère que la formulation est ok, veuillez me corriger si quelque chose est incorrect ou imprécis):

Existence de points fixes en logique

Supposons que ${\mathscr T}$ soit une théorie suffisamment expressive et récursivement énumérable sur le langage ${\mathcal L}$ , et que ${\mathbf C}$ soit un codage de formules ${\mathcal L}$ dans ${\mathscr T}$ , c'est-à-dire un algorithme transformant des formules arbitraires bien formées φ en formules L avec une variable libre C ( φ ) ( v ) , de telle sorte que pour toute formule L φ nous avons T ⊢ ∃ ! v : C ( φ ) ( v ) .${\mathcal L}$$\varphi$${\mathcal L}$${\mathbf C}(\varphi)(v)$${\mathcal L}$$\varphi$${\mathscr T}\vdash \exists! v: {\mathbf C}(\varphi)(v)$

Ensuite , il existe un algorithme ${\mathbf Y}$ tournant bien formés ${\mathcal L}$ -formulas dans une variable libre dans bien formés fermés ${\mathcal L}$ -formulas, tel que pour tout ${\mathcal L}$ -formule dans une variable libre $\phi$ nous avons

$${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \exists v: {\mathbf C}({\mathbf Y}(\phi))(v)\wedge \phi(v),$$ qui, interprétant ${\mathbf C}$ comme un symbole de fonction définie $\lceil -\rceil$, pourrait également s'écrire de manière plus compacte sous la forme $${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \phi(\lceil{\mathbf Y}(\phi)\rceil).$$

En d'autres termes, ${\mathbf Y}$ est un algorithme pour la construction de points fixes par rapport à l' équivalence ${\mathscr T}$ des formules une variable ${\mathcal L}$.

Cela a au moins deux applications:

• En l'appliquant au prédicat $\phi(v)$ exprimant " $v$ code une phrase qui, lorsqu'elle est instanciée avec son propre codage, n'est pas prouvable". donne la formalisation de "Cette phrase n'est pas prouvable" qui est au cœur de l'argument de Goedel.

• Son application à pour une sentence arbitraire ϕ rend indéfinissable la vérité de Tarski.$\neg\phi$$\phi$

2) Points fixes dans le -calculus non typé$\lambda$

Dans le -calculus non typé, la construction de points fixes est importante dans la réalisation de fonctions récursives.$\lambda$

Existence de points fixes dans -calculus:$\lambda$

Il existe un combinateur à virgule fixe , c'est-à-dire un -term Y tel que pour tout λ -term f , on a f ( Y f ) ∼ α β Y f $\lambda$$Y$$\lambda$$f$

$$f(Y f)\sim_{\alpha\beta} Yf.$$

Observation

Ce qui m'étonne, c'est que le combinateur à point fixe en λ -calculus reflète directement, d'une manière très propre et non technique, la preuve habituelle du théorème du point fixe logique:$\lambda f.(\lambda x. f(x x))(\lambda x. f(x x))$$\lambda$

Très grossièrement , étant donné une formule , on considère la formalisation φ ( v ) de l'énoncé " v code une phrase qui, lorsqu'elle est instanciée avec elle-même, satisfait ϕ ", et met A ( ϕ ) : = φ ( ⌈ φ ⌉ ) . La phrase φ ( v ) est comme λ x . f ( x x ) , et φ ( ⌈ φ ⌉ ) correspond à$\varphi$$\varphi(v)$$v$$\phi$${\mathbf A}(\phi) := \varphi(\lceil\varphi\rceil)$$\varphi(v)$$\lambda x. f(x x)$$\varphi(\lceil\varphi\rceil)$ .$(\lambda x. f(x x))(\lambda x. f(x x))$

Question

Malgré son idée rapidement décrite, j'ai trouvé la preuve du théorème du point fixe logique assez technique et difficile à réaliser dans tous les détails; Kunen le fait par exemple dans le théorème 14.2 de son livre «Set Theory». En revanche, le combinateur dans le λ -calcul est très simple et ses propriétés sont facilement vérifiables.$Y$$\lambda$

Le théorème logique du point fixe découle-t-il rigoureusement des combinateurs à point fixe du -calcul?$\lambda$

Par exemple, peut-on modéliser le -calculus par L- formules jusqu'à l'équivalence logique, de sorte que l'interprétation de tout combinateur à point fixe donne un algorithme tel que décrit dans le théorème du point fixe logique?$\lambda$${\mathcal L}$

Éditer

Compte tenu des nombreux autres exemples du même argument de diagonalisation décrits dans les réponses de Martin et Cody, il convient de reformuler la question:

Existe-t-il une généralisation commune des arguments de diagonalisation suivant le principe exprimé dans le combinateur ? λ f . ( λ x . f ( x x ) ) $Y$

$$\lambda f.(\lambda x. f(xx))(\lambda x.f(xx))$$

Si je comprends bien, une proposition est le théorème du point fixe de Lawvere , voir ci-dessous. Malheureusement, je ne peux pas suivre les spécialisations pertinentes dans aucun des articles que Martin a cités dans sa réponse, et je serais heureux si quelqu'un pouvait les expliquer. Tout d'abord, pour être complet:

Théorème de point fixe de Lawvere

Soit une catégorie de produits finis et φ : A × A → Y tels que pour tout morphisme f : A → Y dans C il y ait ⌈ f ⌉ : 1 → A tel que pour tous les points p : 1 → A on ait 1 p → A f → Y = 1 p → A ⟨ ⌈ f ⌉ , id ${\mathscr C}$$\varphi: A\times A\to Y$$f: A\to Y$${\mathscr C}$$\lceil f\rceil: 1\to A$$p: 1\to A$

$$1\xrightarrow{p} A\xrightarrow{\ f\ } Y\ \ =\ \ 1\xrightarrow{p} A\xrightarrow{\langle \lceil f\rceil,\text{id}_A\rangle} A\times A\xrightarrow{\varphi} Y.$$

Ensuite , pour tout endomorphisme , mettant f : = A ô → A × A & phiv → Y g → Y , le choix de ⌈ f ⌉ donne lieu à un point fixe de g , à savoir 1 ⟨ ⌈ f ⌉ , ⌈ f ⌉ ⟩ → A × A & phiv → Y $g: Y\to Y$

$$f\ :=\ A\xrightarrow{\Delta} A\times A\xrightarrow{\varphi} Y\xrightarrow{g} Y,$$ $\lceil f\rceil$$g$ $$1\xrightarrow{\langle\lceil f\rceil,\lceil f\rceil\rangle} A\times A\xrightarrow{\varphi} Y.$$

Il s'agit d'un énoncé dans la théorie (intuitionniste) du premier ordre des catégories à produits finis et s'applique donc à tout modèle de ces derniers.

Par exemple , prendre l'univers théorique de l'ensemble comme domaine du discours donne le paradoxe de Russel (prendre l'ensemble hypothétique des ensembles, Y : = Ω : = { 0 , 1 } et ρ : A × A → Ω le prédicat ∈ ) et le théorème de Cantor (prendre A n'importe quel ensemble et ρ : A × A → Ω correspondant à la surjection hypothétique A → Ω $A$$Y := \Omega := \{0,1\}$$\rho: A\times A\to\Omega$$\in$$A$$\rho: A\times A\to \Omega$$A\to\Omega^A$). De plus, la traduction de la preuve du théorème de Lawvere donne les arguments diagonaux habituels.

Problème plus concret:

Quelqu'un peut-il expliquer en détail une application du théorème de Lawvere à des fonctions récursives partielles ou aux théorèmes logiques à point fixe? En particulier, quelles catégories devons-nous considérer là-bas?

Dans D. Pavlovic, Sur la structure des paradoxes , l'auteur considère la catégorie librement générée par avec Fin ( N ) les fonctions récursives partielles.${\mathbb N}$${\text{End}}({\mathbb N})$

Malheureusement, je ne comprends pas ce que cela signifie.

Par exemple, quelle devrait être la loi de composition sur ? Composition des fonctions récursives partielles? Après tout, il est dit que le théorème de Lawvere applique , avec A = Y = N , de sorte que , en particulier tout morphisme N → N doit avoir un point fixe 1 → N . Si les endomorphismes ne sont en effet que des fonctions récursives partielles et si la composition signifie la composition des fonctions, cela semble étrange - si les points 1 → N ne sont que des éléments de N , alors l'affirmation est fausse, et si un morphisme 1 → $\text{End}({\mathbb N})$$A=Y={\mathbb N}$${\mathbb N}\to{\mathbb N}$$1\to {\mathbb N}$$1\to {\mathbb N}$${\mathbb N}$$1\to {\mathbb N}$ n'est qu'une fonction partielle aussi, donc peut être indéfini, le théorème du point fixe est trivial.

Quelle est la catégorie que l'on veut vraiment considérer?

Peut-être que le but est d'obtenir le théorème du point fixe de Roger, mais alors on devrait en quelque sorte construire un codage des fonctions récursives partielles par des nombres naturels dans la définition de la catégorie, et je ne peux pas comprendre comment le faire.

Je serais très heureux si quelqu'un pouvait expliquer la construction d'un contexte auquel s'applique le théorème de point fixe de Lawvere, donnant naissance à un théorème de point fixe logique ou à un théorème de point fixe pour des fonctions récursives partielles.

Je vous remercie!

Je ne réponds probablement pas directement à votre question, mais il existe une généralisation mathématique commune de nombreux paradoxes, y compris les théorèmes de Gödel et le combinateur Y. Je pense que Lawvere a d'abord exploré cela. Voir aussi [2, 3].

1. FW Lawvere, Arguments diagonaux et catégories fermées cartésiennes .

2. D. Pavlovic, Sur la structure des paradoxes .

3. NS Yanofsky, Une approche universelle des paradoxes autoréférentiels, de l'incomplétude et des points fixes .

Je n'ai pas de réponse complète à votre question, mais je l'ai:

Comme le dit Wikipedia

$Q(x, y)$$p$

$$\varphi_p\simeq \lambda y.Q(p, y)$$ $\varphi$$\mathbb{N}$

$\lambda$

$\phi$${\mathscr T}$$n$

$${\mathscr T}\vdash \phi(\overline{n}) \Leftrightarrow {\mathscr T}\vdash \exists y, \varphi_n(y)=0$$

Ce n'est pas tout à fait ce que vous voulez, mais une astuce d'internalisation peut vous donner la déclaration la plus forte

${\mathscr T}\vdash \phi(\overline{n})\leftrightarrow \exists y, \varphi_n(y) = 0$

Là encore, ce n'est pas tout à fait le théorème du point fixe logique, mais il peut servir le même objectif.

$Q(x,y)$

$$Q(x,y) = 0 \mbox{ iff }{\mathscr T}\vdash \phi(\overline{x})\mbox{ in at most $y$ steps}$$ $Q$$\exists y, Q(x, y)$${\mathscr T}$$\phi(\overline{x})$${\mathscr T}\vdash\exists y,Q(\overline{x}, y)$$\omega$$Q$$\square$

Avec un peu de réflexion, vous pouvez probablement renforcer cet argument pour vous donner le théorème complet directement sans internalisation.