6
\$\begingroup\$

This was originally a pure mathematics question, but I think I've got the best chance for an answer here.

The Challenge

For concreteness, consider Peano Arithmetic (PA). For some language L of your choosing, construct a computer program of length at most N bits in L such that:

  1. If it terminates, it outputs a number that PA proves cannot be outputted by a program in L of length at most N.
  2. If PA proves any specific number cannot be outputted by a program of length at most N, then the program terminates.

Carefully engineering L to make constructing the program easier is encouraged. Smallest N wins.

Motivation

Essentially, the program runs through proofs in PA until it finds one that some specific number cannot be outputted by a program of length N until it finds such a proof, then outputs that specific number. I don't actually know of any explicit previously constructed program that satisfies the above conditions.

The upshot of such a program is Chaitin's incompleteness theorem: Given any computable axiom system (e.g. PA, ZFC, etc.), there exists a N (which equals the size of the computer program describing the axiom system plus an explicit constant) such that that axiom system cannot prove any output has Kolmogorov complexity (the length of the minimal program which outputs said output) larger than N. This is a pretty disturbing result!

Stupid Technical Requirements

  1. There shouldn't be any funny business involved in showing your program satisfies the two conditions above. More precisely, they should be provable in PA. (If you know what Robinson's is, then it has to be provable in that.)
  2. The language L has to be simulatable by a computer program.
  3. The usage of PA is purely for definiteness - your construction should generalize, holding L fixed, to ZFC (for example). This isn't quite a precisely well defined requirement, but I have had some difficulty in constructing a pathological language where the single-byte program A satisfies the above requirements, so I don't think this requirement can be violated accidentally.
  4. Technically, it might be possible that the best N is achieved by a shorter program. In this case, I want the best N. Practically speaking, these are probably going to be the same.

Simplifying Notes

  1. Don't do this in Python! For a typical programming language, formalizing the language within the language of PA is going to be tough going.
  2. PA itself has an infinite number of axioms. Naively, this would mean that you would have to make a subroutine to generate these axioms, but PA has a extension called ACA_0 of the same strength which has a finite axiomatization. These finite number of axioms can then be lumped together into a single axiom, so you only have to deal with a single sentence. Note that any statement of PA which is provable in ACA_0 is provable in PA, so this allows satisfying condition 2. of the challenge.
  3. A potential way to test your program would be to replace PA with something inconsistent. Then, it should eventually terminate, having constructed a proof of large Kolmogorov complexity from the inconsistency.
Improve this question
\$\endgroup\$
5
  • 1
    \$\begingroup\$ Would having a builtin which returns the axioms of PA be against the third rule? \$\endgroup\$
    – Command Master
    Oct 17 at 2:07
  • \$\begingroup\$ Yeah, that's the intention. I'm not sure that it would save any bits in this case, since you would still have to encode this addition to the language into first-order logic in order to define what a proof of Kolmogorov complexity being more than something is. I think a builtin returning the sentence defining ACA_0 might actually let you cheat. \$\endgroup\$
    – Charles Wang
    Oct 17 at 2:40
  • \$\begingroup\$ @CommandMaster What language has a built in for the axioms of PA ???? \$\endgroup\$
    – Pacmanboss256
    Oct 17 at 13:10
  • \$\begingroup\$ @Pacmanboss256 this challenge is about designing a language \$\endgroup\$
    – Command Master
    Oct 17 at 13:47
  • \$\begingroup\$ @CommandMaster I would say, though, that since Chaitin has a program that solves a piece of the problem in a stripped down version of Lisp (arxiv.org/pdf/chao-dyn/9407003v1.pdf), I would also would be interested if someone could exhibit any explicit program in Lisp that solves the challenge. \$\endgroup\$
    – Charles Wang
    Oct 17 at 18:03

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.