Intuitionism (logic and math)

from Wikipedia, the free encyclopedia

The Intuitionism is one of LEJ Brouwer founded towards the philosophy of mathematics , in which mathematics is regarded as an activity of the exact thinking that produces its own objects and does not require. The truth of mathematical statements is reduced to constructibility, which means that intuitionism can be regarded as a kind of constructivism . Intuitionism is one of the basic positions in the fundamental dispute in mathematics .

Basic idea

In intuitionism, the truth of a mathematical proposition is related to the possibility of formulating a corresponding proof. Truth only arises through verification. True sentences or objects described by them have no existence independent of actual thought processes. This is in contrast, among other things, to so-called Platonism in the philosophy of mathematics.

history

The history of intuitionism begins in 1912, when Luitzen Egbertus Jan Brouwer formulated his philosophical foundations with his criticism of the law of the excluded third party . In the 1920s, the formalistic Hilbert School and Brouwer, who was supported by Hilbert's student Hermann Weyl , came to the fundamental crisis of mathematics mentioned in the introduction. The first complete formalization of intuitionist propositional and predicate logic was presented by Arend Heyting in 1930. In 1933 Kurt Gödel showed a possibility of translating classical into intuitionist logic. A semantics for intuitionistic logic as first presented Saul Kripke . Other logicians and mathematicians who contributed to intuitionism are Andrei Kolmogorow , Stephen Kleene and, in Germany, Paul Lorenzen .

Relationship to mathematical constructivism

Evidence based on intuitionist paradigms that go beyond pure logic and examine the properties of mathematical objects leads to constructive mathematics . This arises because, without the theorem of the excluded third party, no contradiction proofs are possible with which, in classical logic, the existence of a mathematical object can be proven by refuting its non-existence. Intuitionism comes to 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.

Intuitionist logic

The equation of truth and provability requires a compatible interpretation of mathematical statements and thus a non-classical logic. While in classical logic the statement is truth-functional (see truth value ) interpreted as “A applies or B applies”, the same statement is interpreted in intuitionistic logic as “There is a proof for A, or there is a proof for B , and you can tell from him whether he proves A or B ”.

From these different interpretations of the logical connections it follows that certain theorems of classical logic are not valid in intuitionist logic. One example is the law of the excluded , . The classic interpretation is “A applies or A does not apply” and is easily recognized as valid. The intuitionist interpretation is “A is provable, or A is refutable” (again with the requirement of the potential proof that it must be possible to recognize which partial statement has been proven). If the principle of the excluded third were true in this interpretation, it would assert the completeness of the calculus.

Calculi for intuitionist logic must therefore be such that the proposition of the excluded third cannot be derived from them. In a rule calculus this is achieved by dispensing with the elimination rule for double negation - for negation only the principle of contradiction remains as an axiom or as a rule. In this way one obtains the intuitionist logic which reflects the philosophical point of view in a purely formal way.

Relationship of intuitionism to classical logic

Intuitionism as a philosophical or metamathematic direction does not criticize classical logic as a formal system, but questions its applicability to scientific, especially mathematical, questions or takes the view that other logical systems are more appropriate to these questions.

For intuitionism as a philosophical position that places the concept of provability at the center of its considerations, classical logic, which interprets logical connections as truth functions (see truth value ), is of no interest because provability cannot be represented as a truth function.

Sentence of the excluded third party

The excluded third theorem becomes problematic when it refers to infinite sets. Take the sentence as an example

P: " Every even number that is greater than 2 can be represented as the sum of two prime numbers ".

According to classical logic, the opposite of this proposition is expressed by the proposition

¬P: “ There is an even number that is greater than 2 and cannot be represented as the sum of two prime numbers. "

Neither the theorem P nor the theorem ¬P could be proven to this day, see Goldbach's Hypothesis .

The enumeration method is not a suitable approach to prove P or ¬P: On the one hand, P cannot be proven in such a way that for every even number g two prime numbers p 1 and p 2 are written down, the sum of which results in g, because there are yes infinitely many even numbers. In order to prove ¬P, however, an even number would have to be given, for which the decomposition into two prime numbers is impossible. If ¬P holds, one would find such a number after a finite time; but if ¬P does not hold, one would search infinitely long.

From the point of view of the intuitionists, the “proposition of the excluded third party” now means that one of the two tasks described above, i.e. the proof of P or the proof of ¬P, must be feasible. In fact, this is not the case for all theorems P: If one day Goldbach's conjecture should be proved or refuted, there are still many other statements about infinite sets for which the same problem exists (for example the continuum hypothesis ); of Gödel's incompleteness theorem also shows that such examples exist of principle.

The principle of the excluded third is therefore accepted in classical logic , but not in intuitionism and Günther's logic .

Inspiration for computer scientists

Computer scientists discovered intuitionism as a source of inspiration and based on this, evidence support systems such as Coq , Epigram and Agda emerged , which require a constructive perspective for their construction and effective use and, for example, contain the sentence of the excluded third party as a "hack" at best. The profound relationship here lies in the Curry-Howard isomorphism , which equates statements with types and proofs with ( programs for calculating) values ​​of the type corresponding to the statement to be proven.

literature

  • LEJ Brouwer , Justification of Set Theory Independent of the Logical Theorem of the Excluded Third, in: ders., Collected Works, pp. 150-190, North-Holland Publishing Company, Amsterdam, Oxford 1975.
  • LEJ Brouwer (Ed.), Intuitionism , introduced and commented on by Dirk van Dalen Mannheim, Leipzig, Vienna, Zurich BI 1992, ISBN 3-411-15371-7 .

Individual evidence

  1. ↑ Bengt Nordström, Kent Petersson, Jan M. Smith: Programming in Martin-Löf's Type Theory - An Introduction , 1990 ( PDF )

Web links