Congettura di Takeuti
# Congettura di Takeuti

In logica matematica, la congettura di Takeuti è una congettura introdotta dal matematico giapponese Gaisi Takeuti. Essa afferma che ogni formalizzazione della logica di secondo ordine nel calcolo dei sequenti gode dell'eliminazione del taglio. Un'estensione naturale di tale congettura richiede che l'eliminazione del taglio valga per ogni formalizzazione nel calcolo dei sequenti di ogni logica di ordine finito.

Per la logica di secondo ordine, la congettura fu dimostrata da Tait nel 1966, sulla base di precedenti lavori di Schütte. La versione generalizzata fu dimostrata indipendentemente da Prawitz nel 1968, e da Takahashi nel 1967. Tutte e tre le dimostrazioni sfruttano tecniche semantiche. Una dimostrazione sintattica fu invece offerta da Jean-Yves Girard, nel cui sistema F la congettura risulta essere un corollario del teorema di normalizzazione forte.

La congettura di Takeuti è equivalente alla consistenza dell'aritmetica di secondo ordine, nonché alla normalizzazione forte del sistema F.

