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.
Read more about this topic: Church's Thesis (constructive Mathematics)
Famous quotes containing the words extended, church and/or thesis:
“No: until I want the protection of Massachusetts to be extended to me in some distant Southern port, where my liberty is endangered, or until I am bent solely on building up an estate at home by peaceful enterprise, I can afford to refuse allegiance to Massachusetts, and her right to my property and life. It costs me less in every sense to incur the penalty of disobedience to the State than it would to obey. I should feel as if I were worth less in that case.”
—Henry David Thoreau (1817–1862)
“He felt that it would be dull times in Dublin, when they should have no usurping government to abuse, no Saxon Parliament to upbraid, no English laws to ridicule, and no Established Church to curse.”
—Anthony Trollope (1815–1882)
“I have been maintaining that the meaning of the word ‘ought’ and other moral words is such that a person who uses them commits himself thereby to a universal rule. This is the thesis of universalizability.”
—Richard M. Hare (b. 1919)