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:
“Only very slowly and late have men come to realize that unless freedom is universal it is only extended privilege.”
—Christopher Hill (b. 1912)
“The Anglican Church is marked by the grace and good sense of its forms, by the manly grace of its clergy. The gospel it preaches is, “By taste are ye saved.” ... It is not in ordinary a persecuting church; it is not inquisitorial, not even inquisitive, is perfectly well bred and can shut its eyes on all proper occasions. If you let it alone, it will let you alone. But its instinct is hostile to all change in politics, literature, or social arts.”
—Ralph Waldo Emerson (1803–1882)
“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)