<p>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:</p>

<ol>
<li>A proof that is computationally intensive or untrusted for some reason (long, complex).</li>
<li>A result that is relevant to undergraduate mathematics.</li>
<li>A result that is useful to program verification.</li>
</ol>

<p>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 <a href="http://link.springer.com/chapter/10.1007%2F978-3-642-39634-2_13" rel="nofollow">Xu, Zhang and Urban</a> in Isabelle. It falls significantly short of priority results though.</p>

CC BY-SA 3.0
2015-05-12T20:31:28.037Z
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).
Pteromys
CC BY-SA 3.0
2015-05-12T22:08:29.033Z
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
CC BY-SA 3.0
2015-05-12T16:43:03.837Z
2015-05-12T16:43:03.837Z
cody
<p>A <em>priority argument</em>, 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.  </p>

<p>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:</p>

<ul>
<li>Priority arguments can sometimes be very complicated (for humans to read);</li>
<li>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</li>
<li>Yet most construction in priority arguments do not look like a typical functional programs at all</li>
</ul>

<reference-request><lo.logic><computability><automated-theorem-proving><proof-assistants>
Formalized priority argument
Pteromys
# Formalized priority argument

(Asked by: username_0 on 2015-05-10)

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

**Tags:** reference-request, lo.logic, computability, automated-theorem-proving, proof-assistants


---

## 1 answers

### Answer by username_1 on 2015-05-12. Score: 1 | Accepted answer

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](http://link.springer.com/chapter/10.1007%2F978-3-642-39634-2_13) in Isabelle. It falls significantly short of priority results though.

> **Comments:**
> **username_0**: 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).  
> **username_1**: 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).  

---

