# Formalized priority argument

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.

• 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). Commented May 12, 2015 at 20:31
• 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).
– cody
Commented May 12, 2015 at 22:08