Church's Thesis (constructive Mathematics) - Extended Church's Thesis

Extended Church's Thesis

Extended Church's thesis (ECT) extends the claim to functions which are totally defined over a certain type of domain. It is used by the school of constructive mathematics founded by Andrey Markov Jr. It can be formally stated by the schema:

In the above, is restricted to be almost-negative. For first-order arithmetic (where the schema is designated ), this means cannot contain any disjunction, and existential quantifiers can only appear in front of (decidable) formulas.

This thesis can be characterised as saying that a sentence is true if and only if it is computably realisable. In fact this is captured by the following meta-theoretic equivalences:

Here, stands for "". So, it is provable in with that a sentence is true iff it is realisable. But also, is provably true in with iff is provably realisable in without .

The second equivalence can be extended with Markov's principle (M) as follows:

So, is provably true in with and iff there is a number n which provably realises in . The existential quantifier has to be outside in this case, because PA is non-constructive and lacks the existence property.