Reto

Escriba un programa P, sin tomar ninguna entrada, de modo que la proposición "la ejecución de P finalmente termine" es independiente de la aritmética de Peano .

Reglas formales

(En caso de que sea un lógico matemático que piense que la descripción anterior es demasiado informal).

En principio, se puede convertir alguna máquina universal de Turing U (por ejemplo, su lenguaje de programación favorito) en una fórmula aritmética de Peano HALT sobre la variable p , donde HALT ( p ) codifica la proposición “ U termina en el programa ( codificado por Gödel por) p ". El desafío es encontrar p tal que ni HALT ( p ) ni ¬HALT ( p ) puedan probarse en la aritmética de Peano.

Puede suponer que su programa se ejecuta en una máquina ideal con memoria ilimitada y enteros / punteros lo suficientemente grandes como para acceder a ella.

Ejemplo

Para ver que tales programas existen, un ejemplo es un programa que busca exhaustivamente una prueba aritmética de Peano de 0 = 1. La aritmética de Peano demuestra que este programa se detiene si y solo si la aritmética de Peano es inconsistente. Dado que la aritmética de Peano es consistente pero no puede probar su propia consistencia , no puede decidir si este programa se detiene.

Sin embargo, hay muchas otras propuestas independientes de la aritmética de Peano en las que podría basar su programa.

Motivación

Este desafío se inspiró en un nuevo artículo de Yedidia y Aaronson (2016) que exhibe una máquina Turing de 7,918 estados cuya no determinación es independiente de ZFC , un sistema mucho más fuerte que la aritmética de Peano. Quizás te interese su cita [22]. Para este desafío, por supuesto, puede usar el lenguaje de programación que prefiera en lugar de las máquinas Turing reales.

Haskell, 838 bytes

"Si quieres que se haga algo, ..."

import Control.Monad.State
data T=V Int|T:$T|A(T->T)
g=guard
r=runStateT
s!a@(V i)=maybe a id$lookup i s
s!(a:$b)=(s!a):$(s!b)
s@((i,_):_)!A f=A(\a->((i+1,a):s)!f(V$i+1))
c l=do(m,k)<-(`divMod`sum(1<$l)).pred<$>get;g$m>=0;put m;l!!fromEnum k
i&a=V i:$a
i%t=(:$).(i&)<$>t<*>t
x i=c$[4%x i,5%x i,(6&)<$>x i]++map(pure.V)[7..i-1]
y i=c[A<$>z i,1%y i,(2&)<$>y i,3%x i]
z i=(\a e->[(i,e)]!a)<$>y(i+1)
(i?h)p=c[g$any(p#i)h,do q<-y i;i?h$q;i?h$1&q:$p,do f<-z i;a<-x i;g$p#i$f a;c[i?h$A f,do b<-x i;i?h$3&b:$a;i?h$f b],case p of A f->c[(i+1)?h$f$V i,do i?h$f$V 7;(i+1)?(f(V i):h)$f$6&V i];V 1:$q:$r->c[i?(q:h)$r,i?(2&r:h)$V 2:$q];_->mzero]
(V a#i)(V b)=a==b
((a:$b)#i)(c:$d)=(a#i)c&&(b#i)d
(A f#i)(A g)=f(V i)#(i+1)$g$V i
(_#_)_=0<0
main=print$(r(8?map fst(r(y 8)=<<[497,8269,56106533,12033,123263749,10049,661072709])$3&V 7:$(6&V 7))=<<[0..])!!0

Explicación

Este programa busca directamente una prueba aritmética de Peano de 0 = 1. Como PA es consistente, este programa nunca termina; pero como PA no puede probar su propia consistencia, la no terminación de este programa es independiente de PA.

T es el tipo de expresiones y proposiciones:

• A Prepresenta la proposición ∀ x [ P ( x )].
• (V 1 :$ P) :$ Qrepresenta la proposición P → Q .
• V 2 :$ Prepresenta la proposición ¬ P .
• (V 3 :$ x) :$ yrepresenta la proposición x = y .
• (V 4 :$ x) :$ yrepresenta el natural x + y .
• (V 5 :$ x) :$ yrepresenta la natural x ⋅ y .
• V 6 :$ xrepresenta el S natural ( x ) = x + 1.
• V 7 representa el 0 natural.

En un entorno con i variables libres, codificamos expresiones, proposiciones y pruebas como matrices enteras 2 × 2 [1, 0; a , b ], como sigue:

• M ( i , ∀ x [ P ( x )]) = [1, 0; 1, 4] ⋅ M ( i , λ x [P (x)])
• M ( i , λ x [ F ( x )]) = M ( i + 1, F ( x )) donde M ( j , x ) = [1, 0; 5 + i , 4 + j ] para todo j > i
• M ( i , P → Q ) = [1, 0; 2, 4] ⋅ M ( i , P ) ⋅ M ( i , Q )
• M ( i , ¬ P ) = [1, 0; 3, 4] ⋅ M ( i , P )
• M ( i , x = y ) = [1, 0; 4, 4] ⋅ M ( i , x ) ⋅ M ( i , y )
• M ( i , x + y ) = [1, 0; 1, 4 + i ] ⋅ M ( i , x ) ⋅ M ( i , y )
• M ( i , x ⋅ y ) = [1, 0; 2, 4 + i ] ⋅ M ( i , x ) ⋅ M ( i , y )
• M ( i , S x ) = [1, 0; 3, 4 + i ] ⋅ M ( i , x )
• M ( i , 0) = [1, 0; 4, 4 + i ]
• M ( i , ( Γ , P ) ⊢ P ) = [1, 0; 1, 4]
• M ( i , Γ ⊢ P ) = [1, 0; 2, 4] ⋅ M ( i , Q ) ⋅ M ( i , Γ ⊢ Q ) ⋅ M ( i , Γ ⊢ Q → P )
• M ( i , Γ ⊢ P ( x )) = [1, 0; 3, 4] ⋅ M ( i , λ x [P (x)]) ⋅ M ( i , x ) ⋅ [1, 0; 1, 2] ⋅ M ( i , Γ ⊢ ∀ x P (x))
• M ( i , Γ ⊢ P ( x )) = [1, 0; 3, 4] ⋅ M ( i , λ x [P (x)]) ⋅ M ( i , x ) ⋅ [1, 0; 2, 2] ⋅ M ( i , y ) ⋅ M ( i , Γ ⊢ y = x ) ⋅ M ( i , Γ ⊢ P ( y ))
• M ( i , Γ ⊢ ∀ x , P ( x )) = [1, 0; 8, 8] ⋅ M ( i , λ x [ Γ ⊢ P ( x )])
• M ( i , Γ ⊢ ∀ x , P ( x )) = [1, 0; 12, 8] ⋅ M ( i , Γ ⊢ P (0)) ⋅ M ( i , λ x [( Γ , P ( x )) ⊢ P (S ( x ))])
• M ( i , Γ ⊢ P → Q ) = [1, 0; 8, 8] ⋅ M ( i , ( Γ , P ) ⊢ Q )
• M ( i , Γ ⊢ P → Q ) = [1, 0; 12, 8] ⋅ M ( i , ( Γ , ¬ Q ) ⊢ ¬ P )

Los axiomas restantes se codifican numéricamente y se incluyen en el entorno inicial Γ :

• M (0, ∀ x [ x = x ]) = [1, 0; 497, 400]
• M (0, ∀ x [¬ (S ( x ) = 0)]) = [1, 0; 8269, 8000]
• M (0, ∀ x ∀ y [S ( x ) = S ( y ) → x = y ]) = [1, 0; 56106533, 47775744]
• M (0, ∀ x [ x + 0 = x ]) = [1, 0; 12033, 10000]
• M (0, ∀ y [ x + S ( y ) = S ( x + y )]) = [1, 0; 123263749, 107495424]
• M (0, ∀ x [ x ⋅ 0 = 0]) = [1, 0; 10049, 10000]
• M (0, ∀ x ∀ y [ x ⋅ S ( y ) = x ⋅ y + x ]) = [1, 0; 661072709, 644972544]

Una prueba con matriz [1, 0; a , b ] puede verificarse dada solo la esquina inferior izquierda a (o cualquier otro valor congruente con un módulo b ); los otros valores están ahí para permitir la composición de las pruebas.

Por ejemplo, aquí hay una prueba de que la suma es conmutativa.

• M (0, Γ ⊢ ∀ x ∀ y [ x + y = y + x]) = [1, 0; 6651439985424903472274778830412211286042729801174124932726010503641310445578492460637276210966154277204244776748283051731165114392766752978964153601068040044362776324924904132311711526476930755026298356469866717434090029353415862307981531900946916847172554628759434336793920402956876846292776619877110678804972343426850350512203833644, 14010499234317302152403198529613715336094817740448888109376168978138227692104106788277363562889534501599380268163213618740021570705080096139804941973102814335632180523847407060058534443254569282138051511292576687428837652027900127452656255880653718107444964680660904752950049505280000000000000000000000000000000000000000000000000000000]

Puede verificarlo con el programa de la siguiente manera:

*Main> let p = A $ \x -> A $ \y -> V 3 :$ (V 4 :$ x :$ y) :$ (V 4 :$ y :$ x)
*Main> let a = 6651439985424903472274778830412211286042729801174124932726010503641310445578492460637276210966154277204244776748283051731165114392766752978964153601068040044362776324924904132311711526476930755026298356469866717434090029353415862307981531900946916847172554628759434336793920402956876846292776619877110678804972343426850350512203833644
*Main> r(8?map fst(r(y 8)=<<[497,8269,56106533,12033,123263749,10049,661072709])$p)a :: [((),Integer)]
[((),0)]

Si la prueba no fuera válida, obtendría la lista vacía.