User:IssaRice/Computability and logic/Comparison of intuitive notions of computability and proof
See Boolos/Burgess/Jeffrey, p. 185.
|Intuitive notion||effectively computable/effectively calculable||informal notion of proof, "proof in the mathematician's ordinary sense"|
|Formal notion||Computable: Turing computable, recursive, register computable, etc. (there are many different formalizations)||Formal deduction in a specific proof system (e.g. formal proof in some axiomatic system or formal proof in some natural deduction system)|
|Interest/motivation||"results about the scope and limits of computability in one or another formal sense discussed in other chapters depend for their interest on their having something to do with computation in a more ordinary sense"||"For in later chapters we are going to be establishing results about the scope and limits of formal deducibility whose interest largely depends on their having something to do with proof in a more ordinary sense"|
|Thesis stating the equivalence between the intuitive notion and formal notion (we will call this the "equivalence thesis" in other parts of the table)||Church–Turing thesis||Hilbert's thesis|
|Evidence in favor of equivalence thesis: accumulation||Demonstration that a wide variety of functions (addition, multiplication, exponentiation, various fast-growing functions, etc.) are computable in the formal sense|
|Evidence in favor of equivalence thesis: independent formalizations turn out to be equivalent||Turing computability, recursiveness, register computability, etc., all turn out compute the same class of functions|
|Evidence in favor of equivalence thesis: ?||???||Completeness theorem|
|Avoidable appeal to equivalence thesis (informal → formal)||In proving that something is formally computable, we skip verification of some tedious details by appealing to our informal notion of computation. This is appeal is avoidable because if we really wanted to, we could go back and fix our proof by grinding out the tedious details. In other words, our argument looks like: (1) informal demonstration; (2) Church–Turing thesis in the direction informal → formal; (3) formal result (by modus ponens).|
|Unavoidable appeal to equivalence thesis (formal → informal)||In showing that something is or isn't intuitively computable, we do this by showing it is or isn't formally computable.|
"In response to a suggestion from Warren Goldfarb, an explicit discussion of the distinction between two different kinds of appeal to Church’s thesis, avoidable and unavoidable, has been inserted at the end of section 7.2. The avoidable appeals are those that consist of omitting the verification that certain obviously effectively computable functions are recursive; the unavoidable appeals are those involved whenever a theorem about recursiveness is converted into a conclusion about effective computability in the intuitive sense." (p. xii)
"An unavoidable appeal to Church’s thesis is made whenever one passes from a theorem about what is or isn’t recursively computable to a conclusion about what is or isn’t effectively computable. On the other hand, an avoidable or lazy appeal to Church’s thesis is made whenever, in the proof of a technical theorem, we skip the verification that certain obviously effectively computable functions are recursively computable." (p. 83)
What I'm confused about: if Church's thesis is (informally computable) ⇔ (formally computable), then we can break this into two sides, (informally computable) ⇒ (formally computable) and (formally computable) ⇒ (informally computable). But now, if (informally computable) ⇒ (formally computable) is an avoidable appeal, then its contrapositive, (not formally computable) ⇒ (not informally computable), must also be avoidable. Yet, the book says this is an unavoidable appeal.