29
\$\begingroup\$

Challenge

Write a program P, taking no input, such that the proposition “the execution of P eventually terminates” is independent of Peano arithmetic.

Formal rules

(In case you are a mathematical logician who thinks the above description is too informal.)

One can, in principle, convert some Universal Turing machine U (e.g. your favorite programming language) into a Peano arithmetic formula HALT over the variable p, where HALT(p) encodes the proposition “U terminates on the program (Gödel-encoded by) p”. The challenge is to find p such that neither HALT(p) nor ¬HALT(p) can be proven in Peano arithmetic.

You may assume your program runs on an ideal machine with unlimited memory and integers/pointers big enough to access it.

Example

To see that such programs exist, one example is a program that exhaustively searches for a Peano arithmetic proof of 0 = 1. Peano arithmetic proves that this program halts if and only if Peano arithmetic is inconsistent. Since Peano arithmetic is consistent but cannot prove its own consistency, it cannot decide whether this program halts.

However, there are many other propositions independent of Peano arithmetic on which you could base your program.

Motivation

This challenge was inspired by a new paper by Yedidia and Aaronson (2016) exhibiting a 7,918-state Turing machine whose nontermination is independent of ZFC, a much stronger system than Peano arithmetic. You may be interested in its citation [22]. For this challenge, of course, you may use your programming language of choice in place of actual Turing machines.

\$\endgroup\$
  • 6
    \$\begingroup\$ What axiom systems may be used to prove that (a) the program does not halt, and (b) the program's non-halting is unprovable in PA? \$\endgroup\$ – feersum May 5 '16 at 19:33
  • 5
    \$\begingroup\$ I don't think it's reasonable to require that this question contain all the needed background in mathematical logic. There's quite a bit of it, and there are links to the relevant info. It's not obfuscated, it's just a technical topic. I think it would help for accessibility to state the requirement for the code separate from the motivation involving Turing machines and to link to some example of Peano-independent statements to consider, in particular Goodstein's Theorem (related golf) \$\endgroup\$ – xnor May 5 '16 at 21:45
  • \$\begingroup\$ For this to make sense, we'd need to assume the code runs on idealized machine with unlimited memory. Can we also assume the machine has arbitrary real precision? \$\endgroup\$ – xnor May 5 '16 at 21:51
  • 1
    \$\begingroup\$ @feersum I am not expecting an axiomatic proof of (a) and (b). Just write a program, and provide enough description/arguments/citations to be reasonably convincing that the claims are true, as you would with any other challenge. You may rely on any standardly accepted axioms and theorems that you need. \$\endgroup\$ – Anders Kaseorg May 5 '16 at 21:55
  • 2
    \$\begingroup\$ @xnor You may assume unlimited memory, and unbounded pointers with which to access it. But I don’t think it’s reasonable to assume arbitrary real precision unless your language actually provides it; in most languages, a program like x = 1.0; while (x) { x = x / 2.0; } will actually halt very quickly. \$\endgroup\$ – Anders Kaseorg May 5 '16 at 22:05
27
+200
\$\begingroup\$

Haskell, 838 bytes

“If you want something done, …”

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

Explanation

This program directly searches for a Peano arithmetic proof of 0 = 1. Since PA is consistent, this program never terminates; but since PA cannot prove its own consistency, the nontermination of this program is independent of PA.

T is the type of expressions and propositions:

  • A P represents the proposition ∀x [P(x)].
  • (V 1 :$ P) :$ Q represents the proposition PQ.
  • V 2 :$ P represents the proposition ¬P.
  • (V 3 :$ x) :$ y represents the proposition x = y.
  • (V 4 :$ x) :$ y represents the natural x + y.
  • (V 5 :$ x) :$ y represents the natural xy.
  • V 6 :$ x represents the natural S(x) = x + 1.
  • V 7 reprents the natural 0.

In an environment with i free variables, we encode expressions, propositions, and proofs as 2×2 integer matrices [1, 0; a, b], as follows:

  • M(i, ∀x [P(x)]) = [1, 0; 1, 4] ⋅ M(i, λx [P(x)])
  • M(i, λx [F(x)]) = M(i + 1, F(x)) where M(j, x) = [1, 0; 5 + i, 4 + j] for all j > i
  • M(i, PQ) = [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, xy) = [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, ΓQP)
  • 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, ΓPQ) = [1, 0; 8, 8] ⋅ M(i, (Γ, P) ⊢ Q)
  • M(i, ΓPQ) = [1, 0; 12, 8] ⋅ M(i, (Γ, ¬Q) ⊢ ¬P)

The remaining axioms are encoded numerically and included in the initial environment Γ:

  • M(0, ∀x [x = x]) = [1, 0; 497, 400]
  • M(0, ∀x [¬(S(x) = 0)]) = [1, 0; 8269, 8000]
  • M(0, ∀xy [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, ∀xy [x ⋅ S(y) = xy + x]) = [1, 0; 661072709, 644972544]

A proof with matrix [1, 0; a, b] can be checked given only the lower-left corner a (or any other value congruent to a modulo b); the other values are there to enable composition of proofs.

For example, here is a proof that addition is commutative.

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

You can verify it with the program as follows:

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

If the proof were invalid you would get the empty list instead.

\$\endgroup\$
  • 1
    \$\begingroup\$ Please explain the idea behind the matrices. \$\endgroup\$ – proud haskeller May 13 '16 at 7:00
  • 2
    \$\begingroup\$ @proudhaskeller They’re just a convenient, relatively compact way of Gödel numbering all possible proof trees. You can also think of them as mixed-radix numerals that get decoded from the least-significant side using div and mod by the number of possible choices at each step. \$\endgroup\$ – Anders Kaseorg May 13 '16 at 7:24
  • \$\begingroup\$ How did you encode the induction axioms? \$\endgroup\$ – PyRulez Jul 20 '17 at 12:42
  • \$\begingroup\$ @PyRulez M(i, Γ ⊢ ∀x, P(x)) = [1, 0; 12, 8] ⋅ M(i, Γ ⊢ P(0)) ⋅ M(i, λx [(Γ, P(x)) ⊢ P(S(x))]) is the induction axiom. \$\endgroup\$ – Anders Kaseorg Nov 15 '17 at 0:47
  • \$\begingroup\$ I think you could make this smaller if you use Calculus of Constructions instead (since Calculus of Constructions has first-order logic built in, and is very small). Calculus of Constructions is about as strong as ZFC, so its consistency is surely independent of PA. To check if its consistient, you simply look for a term of an empty type. \$\endgroup\$ – PyRulez Nov 15 '17 at 1:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.