Limited Principle Of Omniscience
   HOME

TheInfoList



OR:

In
constructive mathematics In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
, the limited principle of omniscience (LPO) and the lesser limited principle of omniscience (LLPO) are
axiom An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
s that are nonconstructive but are weaker than the full
law of the excluded middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, Exclusive or, either this proposition or its negation is Truth value, true. It is one of the so-called Law of thought#The three tradit ...
. The LPO and LLPO axioms are used to gauge the amount of nonconstructivity required for an argument, as in
constructive reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
. They are also related to
weak counterexample In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existenc ...
s in the sense of
Brouwer Brouwer (also Brouwers and de Brouwer) is a Dutch and Flemish surname. The word ''brouwer'' means 'beer brewer'. Brouwer * Adriaen Brouwer (1605–1638), Flemish painter * Alexander Brouwer (b. 1989), Dutch beach volleyball player * Andries Bro ...
.


Definitions

The limited principle of omniscience states : :LPO: For any sequence a_0, a_1, ... such that each a_i is either 0 or 1, the following holds: either a_i=0 for all i, or there is a k with a_k=1. The lesser limited principle of omniscience states: :LLPO: For any sequence a_0, a_1, ... such that each a_i is either 0 or 1, and such that at most one a_i is nonzero, the following holds: either a_=0 for all i, or a_=0 for all i, where a_ and a_ are entries with even and odd index respectively. It can be proved constructively that the law of the excluded middle implies LPO, and LPO implies LLPO. However, none of these implications can be reversed in typical systems of constructive mathematics. The term "omniscience" comes from a thought experiment regarding how a mathematician might tell which of the two cases in the conclusion of LPO holds for a given sequence (a_i). Answering the question "is there a k with a_k=1?" negatively, assuming the answer is negative, seems to require surveying the entire sequence. Because this would require the examination of infinitely many terms, the axiom stating it is possible to make this determination was dubbed an "omniscience principle" by .


Analytic versions

Both principles have analogous properties of the real numbers. The analytic LPO states that every real number satisfies the tritochtomy x < 0 or x = 0 or x > 0 . The analytic LLPO states that every real number satisfies the ditochtomy x \geq 0 or x \leq 0 , while the analytic
Markov's principle Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive m ...
states that if x \geq 0 is false, then x < 0 . All three analytic principles if assumed to hold for the Dedekind or Cauchy real numbers imply their arithmetic versions, while the converse is true if we assume (weak) countable choice, as shown in .


References

* *


External links

* Constructivism (mathematics) {{mathlogic-stub