MENTAL
 Main Menu
 Applications
 Logic
 Intuitionistic Logic


Intuitionistic Logic
 INTUITIONIST
LOGIC

"Brouwer's construction of intuitionistic mathematics is nothing more and nothing less than an investigation of the limits that the intellect can reach in its unfolding" (Arend Heyting).

"The edifice of intuitionistic mathematics is an art, not a science" (Brouwer).

"There can be no mathematics if it has not been constructed intuitively" (Brouwer).



Brouwer's Intuitionistic Logic

Classical logic is a bivalent logic: it uses only two truth values: V (true) and F (false). It is an analytical, superficial and dualistic logic.

Intuitionistic logic is a synthetic, deep, non-dualistic logic. It is a more flexible logic than classical logic. In other words, classical logic is more restrictive than intuitionistic logic.

According to Michael Dummett [1977], the correct logic to apply to mathematics is not classical logic, but intuitionistic logic.

Intuitionistic logic breaks with the duality V-F of classical logic, where ¬V = F and ¬F = V, and has the following characteristics:


Truth

The traditional concept of truth in classical logic is replaced by the concept of constructive demonstration (or constructive procedure). In classical logic, a truth value V (true) or F (false) is assigned to a proposition. In intuitionistic logic a true value is assigned to a mathematical entity only after a constructive demonstration has been found, and a false value is assigned when it is shown not to be constructible. If a constructive proof has not been found for a mathematical entity, it does not mean that it is false, but that it is not known whether it is true or false.

A mathematical entity can also be a relation between mathematical entities. For example, the relations 3×4 = 12 and a∈{a b} are true. And the relations 4<3 and 1+1 = 3 are false.

The truth of a mathematical entity is language independent. It does not depend on its formal or linguistic expression.


The principle of double negation.

In general, the law of elimination of double negation does not hold: ¬¬AA. On the other hand, the converse implication is valid: A → ¬¬A.

The expression ¬A indicates that A is not constructible. Denying that "A is not constructible" does not imply that "A is constructible". If we do not find a constructive procedure for a mathematical entity, this does not mean that it is false, since it may happen that later we find it, or it may happen that we prove that it is impossible to construct it. In the latter case, the entity would indeed be false.

As Brower used to say, using a simile, the impossibility of proving the guilt of a defendant does not prove his innocence.

In this sense, there is asymmetry between positive and negative sentences, a symmetry that does exist in classical logic. In intuitionistic logic, the positive sentence (A) is "stronger" (has more value) than the negative sentence (¬A).


The principle of the excluded third party (PTE)

In classical logic, the ETP states that a proposition is either true or false; there is no third value. In propositional logic it is expressed as (A ∨ ¬A). This principle in propositional logic is equivalent (by De Morgan's law) to its dual: ¬(A ∧ ¬A), which is the principle of non-contradiction. These principles are tautologies in classical logic: But in intuitionistic logic a distinction is made between the two principles: Brouwer observed that the PTE had been established for finite situations and had been generalized without justification for infinite situations. For Brouwer this was equivalent to saying a priori that every mathematical problem has a solution. Accepting the PTE is equivalent to accepting the Hilbertian axiom of resolvability of all mathematical problems. By questioning this principle, Brouwer anticipated Gödel's incompleteness theorem by a quarter of a century. That is, there are problems that are undecidable, i.e., it is not possible to know their truth or falsity. There are also problems that we do not know if they will ever be solved or if they will be proved to be undecidable. For example: However, a conjecture or mathematical question may become proved in the course of time and cease to be undecidable.


Demonstration by reductio ad absurdum

The proof by reductio ad absurdum (introduced by Hilbert) consists in the fact that to prove that a sentence A is true, it is assumed that the sentence ¬A is true. If it is shown that ¬A is false or leads to a contradiction, then A is true. But for intuitionistic logic this only shows that the negative sentence (¬A) is false, but does not necessarily imply the positive one (A).


The standard interpretation of intuitionistic logic

The standard interpretation of intuitionistic logic is the so-called "BHK interpretation" (of Brouwer, Heyting, and Kolmogorov), also called the "demonstration interpretation," which assigns constructivist meaning to logical symbols.

The BHK interpretation is formed by the following definitions:
  1. A demonstration of AB is a demonstration of A and a demonstration of B.

  2. A demonstration of AB is a demonstration of A or a demonstration of B.

  3. A demonstration of AB is a construction that allows us to transform a demonstration of A into a demonstration of B.

  4. The formula ¬A is defined as A→⊥, i.e., a demonstration of ¬A is a construction that transforms a demonstration of A into a contradiction.

  5. A demonstration of ∀xA(x) is a construction that transforms a demonstration < i>d∈D (the range of the variable x) into a demonstration of A(d).

  6. A demonstration of ∃xA(x) is a demonstration of A(d), where dD (the rank of the variable x).
The problem with the BHK interpretation is that there is no formal definition of construction, so these definitions can be interpreted in various ways. The BHK interpretation is more heuristic than mathematically precise.


Heyting's Intuitionistic Logic

Arend Heyting −a disciple of Brouwer and a great defender of his ideas−, proposed a new logic to "formalize intuitionism", which is a contradiction, because according to the principles of intuitionism: 1) mathematics is independent of language and does not need to be formalized, since it is a mental construction; 2) logic is an application of mathematics.

Heyting created in 1930 the intuitionistic logic −also called "constructivist logic"− with the intention of making it the formal logical foundation of Brouwer's intuitionistic mathematics, in particular to formalize the non-validity of the classical principles of the excluded third party (ETP) and the law of the elimination of double negation.

However, Brouwer dismissed Heyting's project of formalizing intuitionistic logic, since he did not regard it as authentic intuitionism, although he described his disciple's work as "extraordinarily interesting."

Because of Heyting, intuitionism entered into a formalistic dynamic with which new logics, such as polyvalent logics, were created.

Heyting justified the introduction of a formal axiomatic system for intuitionistic logic by saying that he only considered it an auxiliary means, because mathematics cannot be reduced to a finite set of pre-established rules expressed in a language. Language is somewhat limited and does not allow the expression of thoughts and intuitions. Formalism has an incompleteness because it cannot capture mathematics in its entirety. Logic is an application of mathematics. Inference or deduction is applied mathematics. Logic is not the foundation of mathematics, but an auxiliary means of it.

Intuitionistic logic has been formalized axiomatically in several ways. Besides that of Heyting [1971], there are among others those of Gentzen [1935], Kleene [1952] and Kripke [1965].

The most widespread and well-known interpretation is Kripke's "semantics of possible worlds," which bears a close resemblance to classical model theory. Kripke's models have been adopted as the standard models for modal logic and intuitionistic logic. Kripke's model is a model initially devised for modal logic, but later, Kripke realized that it provided a semantics for intuitionistic logic. So in the semantics of possible worlds there is a close connection between intuitionistic logic and modal logic.


Features of Heyting's intuitionistic logic
MENTAL and Intuitionistic Logic

Truth

In intuitionistic logic a mathematical entity is true if it is constructible.

In MENTAL, any well-formed constructed expression (according to syntactic rules) exists. A relation that is fulfilled between expressions in abstract space exists.

The truth (V) can also be applied to an expression as an extrinsic predicate or attribute: x/V.


Excluded Third Party Principle (ETP)

In MENTAL the PTE applies in 3 senses:
  1. In Condition. A condition is either met or it is not met. It cannot be met "half-way".

  2. In the existential meta-expressions θ and α, which are contrary to each other:

      (θ' = α)    (α' = θ)

  3. In qualitative magnitudes (q) such as high, rich, fast, etc. and their contraries (q'), including true (V) and false (F), which are also contrary to each other:

      (V' = F)    (F' = V)

    These expressions may be affected by a factor between 0 and 1, the following relations being satisfied:

      ⟨( f*q ≡ (1−f)*q' )⟩ ⟨( f*q' ≡ (1−f)*q )⟩
      ⟨( (f*q)' ≡ (1−f)*q )⟩ ⟨( (f*q)' ≡ f*q' )⟩

    For example, if (high' = low), we have:

    (0.3*high ≡ 0.7*low)
    (0.3*high)' ≡ 0.7*high)
    (0.3*high' ≡ 0.3*low)
If V is used as predicate, as the language is open, we can define: which is the interpretation of classical logic. But we could establish an intuitionistic logic and not give the double negation as true and admit that we do not know whether it is true or false. Formally, For finite expressions the PTE holds, which applies to all kinds of expressions, not just logical ones: an expression either exists or it does not exist. The evaluation of an expression using the operator "?" is the null expression (θ) or the existential expression (α). For example, For infinite expressions this is also true, as long as there are descriptive operators. For example,

({2 4 ...} ⊂ {1...})? // ev. α

(the set of even numbers are included in the set of natural numbers)


Conclusions

MENTAL harmonizes classical logic and intuitionistic logic:

Addenda

Intuitionism and conceptualism

Intuitionism is a gnoseological theory according to which intuition is the only way to know reality. True reality resides in the deep and can only be grasped by intuition. Intuitionism is different from conceptualism, the philosophical school that claims that universals, abstractions, and ideas are entities that exist only in the human mind.


Constructivism and idealism

Constructivism is a theory of knowledge based on 3 principles: 1) Knowledge is not received passively, but is actively constructed by the cognizing subject; 2) The process of cognition is adaptive in the sense that it serves to internally organize the experiential world and not to discover external ontological reality; 3) Mental contents have no relation to "truth", understood as correspondence between internal and external world. Constructivism was born with Giambattista Vico: truth is what man comes to know by constructing through his actions. The human being can only know a thing that he himself creates. "Verum ipsum factum" (Truth is doing). What we create, is determined by our previous constructions. Knowledge is internal, mental constructivism. Vico was an epistemological innovator.

Until Kant, the subject was considered passive in the act of knowing; the subject had to subordinate itself to the object in order to know it. With Kant, the subject is active; it is the object that has to subordinate itself to the subject in the act of knowing. Kant uses the expression "transcendental idealism" to distinguish himself from Berkeley's radical subjective idealism. Human knowledge can only refer to the phenomenon and not to the noun (the thing in itself). In the experience of knowledge, the human psyche is determinant in the knowledge of the object. The construction of reality is determined by the categories of thought and the a priori intuitions of space and time. Metaphysics can be interpreted through epistemology, since we can address metaphysical problems by understanding the source and limits of knowledge.

Radical constructivism was founded by Heinz Von Foerster and Ernst von Glasersfeld. For Von Foerster, the nervous system does not distinguish between perception and allusionation (today we say that the brain does not distinguish between the real and the imagined).

Idealism is a philosophical doctrine that gives primacy to ideas. The object of knowledge is not reality itself, but the representation of reality in our mind (ideas).

For objective idealism, ideas exist by themselves and we can only apprehend them by sensible experience. For subjective idealism, ideas exist only in the mind of the subject. For radical subjective idealism, reality is only mental.

For George Berkeley, radical subjective idealist, reality is nothing but a collection of ideas in our mind. The external world is only an idea in the spirit of God. We only know what we perceive. There are no abstract concepts.


Bibliography