(Partial) Church's thesis

Stream: maths

[Palalansoukî]

The Church's thesis states that all total functions are computable, in some constructive deduction system. Through lean (assuming it contains the axiom of choice) is not constructive, functions defined without nonconstructive machineries are computable in meta sense.

Thus, it is natural to add new axiom, say partial Church's thesis, that states "all functions f : α → β, α and β are Primcodable, such that Lean.isNoncomputable return false are Computable".
It is obviously conservative extention, through it may speedup the proofs.

My questions are:

1. How can we add this axiom? (Sorry, I am not familiar with metaprogramming)
2. Is it thinkable to add this axiom to Mathlib? Because the proof of computability is obvious from its definition, but the proof looks horrible in some cases.

[Kevin Buzzard]

Mathlib has a no axiom policy. If you can prove things using the axiom then the way to get them into mathlib is to state the axiom as a Prop and then prove theorems of the form "the proposition implies X"

[Kim Morrison]

Note that @Palalansoukî is proposing a whole family of axioms, on account of the clause "such that Lean.isNoncomputable return false". There is no way this is happening in Mathlib!

[Niels Voss]

Note that:

• noncomputable doesn't actually mean the same thing as "not computable", it means that Lean can't figure out how to generate bytecode for it, which can be different in certain situations.
• Using partial, you can convert basically any noncomputable function to a computable function that just loops forever. So, your axiom would state that every function is Computable, which is false.

[Mario Carneiro]

I don't think there is any way to express this in lean as an actual axiom, unless you define Lean.isNoncomputable f as not (Computable f) in which case it's trivial. What this is instead is a metaprogram / tactic, and I sketched how one might go about doing that without axiomatic extensions.