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)
“Now, honestly: if a large group of ... demonstrators blocked the entrances to St. Patrick’s Cathedral every Sunday for years, making it impossible for worshipers to get inside the church without someone escorting them through screaming crowds, wouldn’t some judge rule that those protesters could keep protesting, but behind police lines and out of the doorways?”
—Anna Quindlen (b. 1953)
“Some have said that the thesis [of indeterminacy] is a consequence of my behaviorism. Some have said that it is a reductio ad absurdum of my behaviorism. I disagree with this second point, but I agree with the first. I hold further that the behaviorism approach is mandatory. In psychology one may or may not be a behaviorist, but in linguistics one has no choice.”
—Willard Van Orman Quine (b. 1908)