Intuitionism

Intuitionism is a reasoned from LEJ Brouwer direction of the philosophy of mathematics, where mathematics is regarded as an activity of the exact thinking that produces its own objects and does not require. Truth of mathematical statements is reduced to constructability, which intuitionism can be considered a kind of constructivism. The intuitionism is one of the basic positions in the basic argument of mathematics.

• 3.1 ratio of intuitionism on classical logic
• 3.2 law of excluded middle

Basic idea

The truth of a mathematical proposition is based on intuitionism on the ability to formulate an appropriate proof. Truth arises is therefore only through the verification. True sets or objects described by them have no existence independent of actual thought processes. This is in contrast to, among other so-called Platonism in the philosophy of mathematics.

History

The history of intuitionism begins in 1912, formulated as Luitzen Egbertus January Brouwer with his criticism of the law of the excluded middle, its philosophical foundations. The first complete formalization of intuitionistic propositional and predicate logic provides Arend Heyting ago in 1930. 1933 Kurt Gödel showed a possibility of translation of classical into intuitionistic logic. A semantics for the intuitionistic logic presents the first Saul Kripke. More logician who contributed to intuitionism, are Stephen Kleene and in Germany Paul Lorenzen.

Relation to mathematical constructivism

Evidence by intuitionistic paradigms that go beyond the pure logic and study the properties of mathematical objects, lead to constructive mathematics. This arises because without the law of excluded middle no contradiction proofs are possible to those in classical logic, the existence of a mathematical object can be proved by the non-existence is refuted. Intuitionism reaches so far the same results as constructivism, although the underlying philosophical considerations are different - intuitionism is based on a non-classical concept of truth, constructivism on a non-classical concept of existence.

Intuitionistic logic

The equation of truth and provability requires a compatible therewith interpretation of mathematical statements and thus a non-classical logic. While in classical logic, the statement truth-functional (see truth value ) is interpreted as "A is true or B is true ," the same statement is interpreted in intuitionistic logic as "There is a proof of A or there is a proof of B and one recognizes him, if he proves A or B ".

From this different interpretation of the logical connectives follows that certain theorems of classical logic into intuitionistic are not valid. One example is the law of excluded middle. The classical interpretation is " A is true or A is not true " and is easily recognizable as valid. The intuitionistic interpretation is " A is provable, or A is refutable " (again with the requirement of the potential evidence that it must be clear which part statement has been proven). If the law of excluded middle true in this interpretation, he would argue the completeness of the calculus.

Calculi for intuitionistic logic must therefore be such that in them the law of excluded middle is not derivable. In a rule calculus to do this by one renounces the elimination rule for double negation - the negation then remains only the principle of contradiction as an axiom or rule. In this way we obtain the intuitionistic logic, which reflects the philosophical point of view in a purely formal way.

Ratio of intuitionism to classical logic

The intuitionism as a philosophical or meta-mathematical direction does not criticize the classical logic as a formal system, but is their applicability to science, especially mathematical questions in question or of the opinion that other logical systems, these questions are more appropriate.

For intuitionism as a philosophical position, which introduces the concept of provability in the center of their considerations is the classic logic, the logic operations as truth-functions (see truth value ) interpreted simply not of interest because provability is not represented as a truth function.

Law of excluded middle

The law of excluded middle is problematic when it refers to infinite sets. As an example, serve the sentence

P: " Every even number greater than 2, can be written as the sum of two primes ".

The converse of this proposition is, according to classical logic, expressed by the sentence

¬ P: "There is an even number greater than 2, and can not be written as the sum of two primes. "

Neither the rate nor the rate P ¬ P could be proved to date, see Goldbach's Conjecture.

The enumeration method is not a suitable approach in order to prove P or ¬ P: On the one hand P can not be proved in such a way that for every even number g of two prime numbers be written p1 and p2, the sum of which g, because there are infinitely many even numbers. In contrast, to prove ¬ P is an even number should be specified for the decomposition into two prime numbers is impossible. If ¬ P is true, one would indeed after a finite time find such a number; but if ¬ P does not hold, one would look infinitely long.

From the perspective of Intuitionists the " law of excluded middle " now states that one of the two tasks described above, so the proof of P or the proof of ¬ P must be feasible. This is in fact not for all sets P of the case: If one day now but the Goldbach's conjecture be proved or disproved, so there are still many other statements about infinite sets, for the same problem (for example, the continuum hypothesis ), the Gödel incompleteness theorem also shows that such examples of principle exist.

The law of excluded middle is therefore indeed accepted in classical logic, but not in intuitionism and Günther logic.

Inspiration for computer scientists

Computer scientists discovered intuitionism as a source of inspiration and building on that arose proof support systems such as Coq (software), Epigram and Agda, the demand for their construction and for the effective use of the constructive perspective and include, for example, the law of excluded middle, at best, as a "hack". The profound relationship here is in the Curry - Howard isomorphism, the same sets of statements with types and proofs ( programs for the calculation of ) the corresponding values ​​of the statement to be proved type.