A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce to each other.

My question is whether or not there has been an attempt to formalize priority arguments in some proof system adopted by proof checkers or proof checkers. I believe this is an interesting problem, since:

  • Priority arguments can sometimes be very complicated (for humans to read);
  • Objects constructed by priority arguments are constructive (relative to something else), so it is possible that the argument is suitable to formalize in some proof systems, many of them are based on typed lambda calculi; and
  • Yet most construction in priority arguments do not look like a typical functional programs at all

Computability theory in general has been somewhat under-formalized. The short answer is that most theorems of computability theory do not pass one of the three tests for formalization:

  1. A proof that is computationally intensive or untrusted for some reason (long, complex).
  2. A result that is relevant to undergraduate mathematics.
  3. A result that is useful to program verification.

Reason 1 may apply in this case, but the preliminary work to build up to that result unfortunately hasn't been carried out. I found one reference to mechanized computability theory by Xu, Zhang and Urban in Isabelle. It falls significantly short of priority results though.

  • $\begingroup$ Are these "tests" widely known among the research community? I kind of understand the rationale for Test 1 and 3, but what about Test 2? Besides, If I understand correctly Feit-Thompson theorem was a target of formalization, but I guess it fails to satisfy Test 2 and 3 (we could say it passes Test 2 but then it would be reasonable to say at the same time so does Friedberg-Muchnik). $\endgroup$
    – Pteromys
    May 12 '15 at 20:31
  • $\begingroup$ No it's just a somewhat tongue in cheek notion of what is "acceptable" formalization material. Unfortunately, formalization is hard work that is not very appreciated, so targets for formalization are chosen to be either widely applicable, or sensational in some manner (Feit-Thompson is one of these, as is the Prime Number Theorem). $\endgroup$
    – cody
    May 12 '15 at 22:08

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.