Church's thesis (constructive mathematics)

Church's thesis (constructive mathematics)

In constructive mathematics, Church's thesis is the mathematical assertion that all total functions are recursive. It gets its name after the informal Church–Turing thesis, which states that every algorithm is in fact a recursive function, but the constructivist version is formal and much stronger. It is in fact incompatible with classical logic.

Formal statement

One way Church's Thesis can be formally stated is by the schema:

(\forall x \; \exist y \; \phi(x,y)) \to (\exist f \; \forall x \;\exist y,u \; \bold{T}(f,x,y,u) \wedge \phi(x,y))

Where the variables range over the natural numbers, and ϕ is any predicate. This schema asserts that, if for every x there is a y satisfying some predicate, then there is in fact an f which is the Gödel number of a general recursive function which will, for every x, produce such a y satisfying that predicate. (T is some universal predicate which decodes the Gödel-numbering used.)

The thesis is incompatible with classical logic; adding it to Heyting arithmetic (HA) allows one to disprove instances of the law of the excluded middle. For instance, it is a classical tautology that every Turing machine either halts or does not halt on a given input; but if that were true, then from Church's Thesis one would conclude that there is a general recursive function which solves the halting problem. This is impossible.

However, Heyting arithmetic is equiconsistent with Peano arithmetic (PA) as well as with Heyting arithmetic plus Church's thesis. That is, adding either the law of the excluded middle or Church's thesis can not make Heyting arithmetic inconsistent, but adding both will.

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:

(\forall x \; \psi(x) \to \exist y \; \phi(x,y)) \to \exist f (\forall x \; \psi(x) \to \exist y,u \; \bold{T}(f,x,y,u) \wedge \phi(x,y))

In the above, ψ is restricted to be almost-negative. For first-order arithmetic (where the schema is designated ECT0), this means ψ cannot contain any disjunction, and existential quantifiers can only appear in front of \Delta^0_0 (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[1]:

HA + ECT_0 \vdash (\phi \leftrightarrow (\exist n \; n \Vdash \phi))
(HA + ECT_0 \vdash \phi) \leftrightarrow (HA \vdash \exist n \; (n \Vdash \phi))

Here, n \Vdash \phi stands for "n realises ϕ". So, it is provable in HA with ECT0 that a sentence is true iff it is realisable. But also, ϕ is provably true in HA with ECT0 iff ϕ is provably realisable in HA without ECT0.

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

(HA + ECT_0 + M \vdash \phi) \leftrightarrow (\exist n \; PA \vdash (\bar{n} \Vdash \phi))

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

Reference

  1. ^ Troelstra, A. S. Metamathematical investigation of intuitionistic arithmetic and analysis. Vol 344 of Lecture notes in mathematics; Springer, 1973

Wikimedia Foundation. 2010.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Church–Turing thesis — Church s thesis redirects here. For the constructive mathematics assertion, see Church s thesis (constructive mathematics). In computability theory, the Church–Turing thesis (also known as the Church–Turing conjecture, Church s thesis, Church s… …   Wikipedia

  • History of the Church-Turing thesis — This article is an extension of the history of the Church Turing thesis.The debate and discovery of the meaning of computation and recursion has been long and contentious. This article provides detail of that debate and discovery from Peano s… …   Wikipedia

  • History of the Church–Turing thesis — This article is an extension of the history of the Church–Turing thesis. The debate and discovery of the meaning of computation and recursion has been long and contentious. This article provides detail of that debate and discovery from Peano s… …   Wikipedia

  • List of mathematics articles (C) — NOTOC C C closed subgroup C minimal theory C normal subgroup C number C semiring C space C symmetry C* algebra C0 semigroup CA group Cabal (set theory) Cabibbo Kobayashi Maskawa matrix Cabinet projection Cable knot Cabri Geometry Cabtaxi number… …   Wikipedia

  • Constructive set theory — is an approach to mathematical constructivism following the program of axiomatic set theory. That is, it uses the usual first order language of classical set theory, and although of course the logic is constructive, there is no explicit use of… …   Wikipedia

  • Constructive analysis — In mathematics, constructive analysis is mathematical analysis done according to the principles of constructive mathematics. This contrasts with classical analysis, which (in this context) simply means analysis done according to the (ordinary)… …   Wikipedia

  • mathematics, foundations of — Scientific inquiry into the nature of mathematical theories and the scope of mathematical methods. It began with Euclid s Elements as an inquiry into the logical and philosophical basis of mathematics in essence, whether the axioms of any system… …   Universalium

  • Constructivism (mathematics) — In the philosophy of mathematics, constructivism asserts that it is necessary to find (or construct ) a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption,… …   Wikipedia

  • Alonzo Church — This article is about the mathematician and logician. For the president of the University of Georgia, see Alonzo S. Church. Alonzo Church Alonzo Church (1903–1995) …   Wikipedia

  • Philosophy of mathematics — The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”