Principe de Markovvignette|250x250px|Une représentation artistique d'une machine de Turing. Le principe de Markov dit que s'il est impossible qu'une machine de Turing ne s'arrête pas, alors elle doit s'arrêter. Le principe de Markov, nommé d'après Andreï Markov Jr, est une déclaration d'existence conditionnelle pour laquelle il existe de nombreuses formulations, ainsi qu'il est discuté ci-dessous. Ce principe est utilisé dans la validité logique classique, mais pas dans les mathématiques intuitionniste constructives.
Church's thesis (constructive mathematics)In constructive mathematics, Church's thesis is an axiom stating that all total functions are computable functions. The similarly named Church–Turing thesis states that every effectively calculable function is a computable function, thus collapsing the former notion into the latter. is stronger in the sense that with it every function is computable. The constructivist principle is fully formalizable, using formalizations of "function" and "computable" that depend on the theory considered.
Constructive set theoryAxiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories. In addition to rejecting the principle of excluded middle (), constructive set theories often require some logical quantifiers in their axioms to be set bounded, motivated by results tied to impredicativity.
Heyting arithmeticIn mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it. Heyting arithmetic can be characterized just like the first-order theory of Peano arithmetic , except that it uses the intuitionistic predicate calculus for inference. In particular, this means that the double-negation elimination principle, as well as the principle of the excluded middle , do not hold.
Analyse constructiveL'analyse constructive est une branche des mathématiques constructives. Elle critique l'analyse mathématique classique et vise à fonder l'analyse sur des principes constructifs. Elle s'inscrit dans le courant de pensée constructiviste ou intuitionniste, dont les principaux membres ont été Kronecker, Brouwer ou Weyl. La critique porte sur la façon dont est utilisée la notion d'existence, de disjonction et sur l'utilisation du raisonnement par l'absurde.
