Wyzwanie

Napisz program P, nie przyjmując żadnych danych wejściowych, tak aby zdanie „wykonanie P ostatecznie się kończy” było niezależne od arytmetyki Peano .

Zasady formalne

(W przypadku logika matematycznego, który uważa, że ​​powyższy opis jest zbyt nieformalny).

Zasadniczo można konwertować część uniwersalnej maszyny Turinga U (np. Ulubiony język programowania) na wzór arytmetyczny Peano HALT na zmienną p , gdzie HALT ( p ) koduje zdanie „ U kończy się na programie ( kodowane przez Gödela ) p ”. Wyzwanie polega na znalezieniu p takiego, że ani HALT ( p ), ani ¬HALT ( p ) nie mogą być udowodnione w arytmetyce Peano.

Możesz założyć, że twój program działa na idealnej maszynie z nieograniczoną pamięcią i liczbami całkowitymi / wskaźnikami wystarczająco dużymi, aby uzyskać do niej dostęp.

Przykład

Aby zobaczyć, że takie programy istnieją, jednym z przykładów jest program, który wyczerpująco szuka dowodu arytmetycznego Peano na 0 = 1. Arytmetyka Peano dowodzi, że ten program zatrzymuje się wtedy i tylko wtedy, gdy arytmetyka Peano jest niespójna. Ponieważ arytmetyka Peano jest spójna, ale nie może udowodnić własnej spójności , nie może zdecydować, czy ten program się zatrzyma.

Istnieje jednak wiele innych propozycji niezależnych od arytmetyki Peano, na których można oprzeć swój program.

Motywacja

Wyzwanie to zostało zainspirowane nową pracą Yedidii i Aaronsona (2016) przedstawiającą 7918-stanową maszynę Turinga, której nieterminacja jest niezależna od ZFC , znacznie silniejszego systemu niż arytmetyka Peano. Możesz być zainteresowany jego cytatem [22]. Do tego wyzwania możesz oczywiście użyć wybranego języka programowania zamiast rzeczywistych maszyn Turinga.

Haskell, 838 bajtów

„Jeśli chcesz coś zrobić…”

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

Wyjaśnienie

Ten program bezpośrednio szuka arytmetyki Peano o wartości 0 = 1. Ponieważ PA jest spójny, ten program nigdy się nie kończy; ale ponieważ PA nie może udowodnić swojej spójności, nieterminacja tego programu jest niezależna od PA.

T jest rodzajem wyrażeń i zdań:

• A Preprezentuje twierdzenie ∀ x [ P ( x )].
• (V 1 :$ P) :$ Qstanowi propozycję P → Q .
• V 2 :$ Poznacza propozycja ¬ P .
• (V 3 :$ x) :$ yreprezentuje twierdzenie x = y .
• (V 4 :$ x) :$ yreprezentuje naturalne x + y .
• (V 5 :$ x) :$ yreprezentuje naturalne x ⋅ y .
• V 6 :$ xreprezentuje naturalne S ( x ) = x + 1.
• V 7 reprezentuje naturalne 0.

W środowisku o ı zmiennych wolnych, że koduje wyrażeń propozycji i dowody w postaci 2 x 2 macierzy całkowitych [1, 0; a , b ], jak następuje:

• M ( i , ∀ x [ P ( x )]) = [1, 0; 1, 4] ⋅ M ( i , λ x [P (x)])
• M ( i , λ x [ F ( x )]) = M ( i + 1, F ( x )) gdzie M ( j , x ) = [1, 0; 5 + i , 4 + j ] dla wszystkich 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 )

Pozostałe aksjomaty są kodowane numerycznie i uwzględniane w środowisku początkowym Γ :

• 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]

Dowód z matrycą [1, 0; , b ] można sprawdzić podane jedynie lewy dolny narożnik A (lub dowolną inną wartość przystający do a modulo b ); pozostałe wartości mają na celu umożliwienie zestawienia dowodów.

Na przykład tutaj jest dowód, że dodawanie jest przemienne.

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

Możesz to zweryfikować za pomocą programu w następujący sposób:

*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)]

Jeśli dowód byłby nieważny, zamiast tego dostaniesz pustą listę.