A proof complexity conjecture and the Incompleteness theorem

1. Problema e Contesto

Il lavoro si colloca nell'intersezione tra la teoria della complessità delle dimostrazioni (proof complexity) e la logica matematica. Il problema centrale è la congettura secondo cui esiste un "generatore" (una funzione computabile in tempo polinomiale) che è "duro" (hard) per tutti i sistemi di dimostrazione.

In termini più semplici, la congettura afferma l'esistenza di una funzione $g: \{0, 1\}^* \to \{0, 1\}^*$ che:

1. È computabile in tempo polinomiale ($p$-time).
2. Estende ogni input di un bit (cioè $|g(u)| = |u| + 1$).
3. Il suo range (l'insieme dei valori in uscita) interseca tutti gli insiemi infiniti di classe NP.

Se tale funzione esistesse, implicherebbe che nessun sistema di dimostrazione proposizionale può dimostrare efficientemente che certi stringhe non appartengono al range di $g$, il che avrebbe profonde implicazioni per la separazione delle classi di complessità (in particolare $NP \neq coNP$).

2. Metodologia

L'autore utilizza una strategia costruttiva basata sulla provabilità all'interno di teorie formali, sviluppando due approcci principali:

A. Costruzione Teorica (Logica del Primo Ordine)

L'autore definisce una funzione $g_T$ basata su una teoria del primo ordine $T$ (che estende la teoria $S^1_2$ di Buss), assumendo che $T$ sia:

• Sana (Sound): Tutto ciò che è dimostrabile in $T$ è vero nel modello standard $\mathbb{N}$.
• Computabile in tempo polinomiale.
• Capace di formalizzare la sintassi della logica del primo ordine.

Algoritmo di $g_T(u)$:

1. Dato un input $u$ di lunghezza $n$, si cerca una formula $\Phi$ (con una variabile libera $x$) che è un prefisso di $u$ e ha lunghezza $\le \log n$.
2. Se non esiste, l'output è $0^{n+1}$.
3. Se esiste, si definisce $c = |\Phi| + 1$. Si iterano tutte le stringhe $w \in \{0, 1\}^{c+1}$ in ordine lessicografico.
4. Per ogni $w$, si cerca una dimostrazione in $T$ di dimensione $\le \log n$ della frase:
   $$\exists y \forall x > y (\Phi(x) \to \neg(w \subseteq_e x))$$
   (dove $w \subseteq_e x$ significa che $w$ è un prefisso di $x$).
5. Se per tutti i $w$ si trova una dimostrazione, l'output è $0^{n+1}$.
6. Altrimenti, si prende il primo $w_0$ per cui non si trova dimostrazione e si restituisce $w_0 u_0$ (dove $u = \Phi u_0$).

B. Costruzione Proposizionale (Verso la Complessità Computazionale)

Poiché la logica del primo ordine non è direttamente applicabile alla complessità proposizionale, l'autore traduce l'argomento nel dominio proposizionale.

• Le formule $\Phi_w$ (che sono $\Pi^b_1$) vengono tradotte in formule proposizionali $\varphi_{n,w}$ tramite una traduzione canonica.
• Si assume che i sistemi di dimostrazione proposizionali siano "ottimali" o che certe classi di complessità (come $E$) siano contenute in $P/poly$.
• L'algoritmo cerca dimostrazioni non in una teoria formale, ma all'interno di circuiti booleani di dimensioni limitate, sfruttando l'ipotesi che $E \subseteq P/poly$.

3. Risultati Chiave

Risultato 1: Una nuova dimostrazione del Teorema di Incompleteness di Gödel

L'autore dimostra che se $T$ è sana e completa, la funzione $g_T$ intersecherebbe ogni sottoinsieme infinito definibile di $\{0, 1\}^*$.
Tuttavia, il complemento del range di $g_T$ è infinito e definibile. Se $g_T$ intersecasse anche questo complemento, si creerebbe una contraddizione (un elemento sarebbe sia nel range che fuori).
Conclusione: Non può esistere una teoria $T$ che sia contemporaneamente sana, computabile in tempo polinomiale e completa. Questo fornisce una prova del Primo Teorema di Incompletezza di Gödel basata sulla complessità computazionale e sulla proprietà di "stretching" della funzione.

Risultato 2: Il Teorema Principale (Teorema 3.1)

L'autore dimostra che almeno una delle seguenti tre affermazioni deve essere vera:

1. Non esiste un sistema di dimostrazione proposizionale p-ottimale. (Questo è equivalente all'inesistenza di un algoritmo di ricerca di dimostrazioni ottimale in termini di tempo).
2. $E \not\subseteq P/poly$. (La classe di complessità $E$ non è contenuta in $P/poly$, ovvero i problemi risolvibili in tempo esponenziale non possono essere risolti da circuiti di dimensione polinomiale).
3. Esiste una funzione $h$ con le proprietà della congettura:
   • Estende ogni input di un bit.
   • È computabile in tempo sub-esponenziale ($2^{O((\log n)^{\log \log n})}$).
   • Il suo range interseca tutti gli insiemi infiniti di classe NP.

4. Contributi e Significato

• Collegamento tra Incompletezza e Complessità: Il paper offre un ponte concettuale diretto tra l'incompletezza logica (Gödel) e la durezza dei generatori nella complessità delle dimostrazioni. Mostra che l'incompletezza è una conseguenza necessaria della limitatezza temporale nella ricerca di dimostrazioni.
• Riduzione della Congettura: Il lavoro riduce la congettura originale (esistenza di un generatore duro per tutti i sistemi) a una disgiunzione di tre condizioni fondamentali. Se si potesse dimostrare che esistono sistemi di dimostrazione p-ottimali e che $E \subseteq P/poly$, allora la congettura sarebbe vera (esisterebbe un generatore $h$).
• Nuova Classe di Generatori: Introduce la possibilità di generatori che sono "quasi-polinomiali" (o sub-esponenziali) ma che soddisfano la proprietà di intersezione con tutti gli insiemi NP, offrendo un nuovo punto di vista sulla gerarchia di complessità.
• Problema Aperto: L'autore lascia come problema aperto (Problema 2.4) se, per una teoria $T$ specifica, la funzione $g_T$ soddisfi effettivamente la congettura originale (intersecando tutti gli insiemi NP infiniti). Una risposta affermativa implicherebbe $NP \neq coNP$.

Sintesi Finale

Jan Krajíček dimostra che l'esistenza di un generatore "duro" per tutti i sistemi di dimostrazione è strettamente legata all'impossibilità di avere un sistema di dimostrazione proposizionale ottimale e alla separazione tra classi di complessità come $E$ e $P/poly$. La costruzione di $g_T$ fornisce una prova elegante e costruttiva dell'incompletezza di Gödel, trasformando un teorema logico in un problema di complessità computazionale. Il lavoro suggerisce che la difficoltà nel trovare dimostrazioni efficienti (o la loro assenza) è una proprietà intrinseca dei sistemi formali sufficientemente potenti, e che la risoluzione della congettura sui generatori potrebbe richiedere progressi fondamentali nella teoria della complessità.