I have been curious about intuitionistic logic for some time and I want to know about it and I have a question, the law of the excluded middle and double negation elimination seem completely logical to me and I think they are always correct. But intuitionistic logic does not accept these two laws. What is the cause of this? Are there really propositions in mathematics for which these two principles do not hold? If so, please give examples of propositions that are examined in intuitionistic logic and the law of the excluded middle and double negation elimination does not work in them.
What are the examples for intuitionistic logic
intuitionistic-logic
Best Answer
A practical application of intuitionistic logic comes up naturally in the study of modern algebraic geometry.
To be brief, algebraic geometry is the study of the geometry of solution sets to systems of polynomial equations. At some point, it becomes useful to study the sheaf of regular functions on such an object. This means that we are interested in rational functions defined on "open" subsets; here the notion of "open" is given by the Zariski topology, where we just want to impose some conditions that certain other polynomials are nonzero. More generally, we can have functions which look like rational functions only locally.
However, it then turns out that if you generalize to sheaves of sets (as opposed to the sheaves of abelian groups, or sheaves of modules over a sheaf of rings, that are usually studied in algebraic geometry), then that category of sheaves of sets can naturally be given what is known as an "internal logic", which gives a "type theory" which acts very close to usual mathematics. The big difference is that in general, excluded middle and double negation elimination do not hold in this internal logic.
The usefulness then comes in being able to use the internal language of a topos to define interesting objects in the category of sheaves of sets. Also, if you have any statement which is formally provable in the internal logic, then it will always hold on any sheaves of sets. That can sometimes be useful in clarifying what otherwise could be a confusing proof involving passing to refinement covers multiple times.
So, even if you believe that the universe containing the objects of algebraic geometry satisfies the law of excluded middle, you still get interesting models of intuitionistic logic which do not satisfy excluded middle, and for which theorems of this version of intuitionistic logic can give useful information in the original universe.
(Modern algebraic geometry also studies so-called "Grothendieck sites" which generalize the example of Zariski topology: the etale sites, the crystalline site, etc. You can also define sheaves of sets on these sites, and they also have a straightforward generalization of the internal logic.)