Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. Logic (from Classical Greek λόγος (logos), originally meaning the word, or what is spoken, but coming to mean thought or reason) is most often said to be the study of arguments, although the exact definition of logic is a matter of controversy amongst philosophers (see below). ... In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach to mathematics as the constructive mental activity of humans. ... In the philosophy of mathematics, constructivism asserts that it is necessary to find (or construct) a mathematical object to prove that it exists. ...

Roughly speaking, "intuitionism" holds that logic and mathematics are "constructive" mental activities. That is, they are not analytic activities wherein deep properties of existence are revealed and applied. Instead, logic and mathematics are the application of internally consistent methods to realize more complex mental constructs (really, a kind of game). In a stricter sense, intuitionistic logic can be investigated as a very concrete and formal kind of mathematical logic. While it may be argued whether such a formal calculus really captures the philosophical aspects of intuitionism, it has properties which are also quite useful from a practical point of view. Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics. ... For other uses of the term calculus see calculus (disambiguation) Calculus is a central branch of mathematics, developed from algebra and geometry, and built on two major complementary ideas. ...

Both notions of the term will be considered below.

Intuitionistic logic as a paradigm for logical reasoning

In intuitionistic logic, epistemologically unclear steps in proofs are forbidden. In classical logic, a formula—say, A—asserts that A is true. In intuitionistic logic a formula is only considered to be true if it can be proved. As an example of this difference consider the law of excluded middle. Accepted by classical logic, the law is not accepted by intuitionistic logic because, in a language that allows the formula, it is possible to draw the conclusion that P ∨ ¬P without knowing which of the disjuncts is true. In effect, in intuitionistic logic, P ∨ ¬P says that at least one of P or ¬P can be proved, which is stronger than saying that their disjunction is true. Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. ... In logic, the law of excluded middle (tertium non datur in Latin) states that for any proposition P, it is true that (P ∨ ¬P). ...

The thought behind this is that the validity of a mental construct is dependent upon its coherence with its context (the mind). From this perspective, epistemological opacity is, in effect, cheating.

Intuitionistic logic substitutes justification for truth in its logical calculus. The logical calculus preserves justification, rather than truth, across transformations yielding derived propositions.

Intuitionistic logic gave philosophical support to several schools of philosophy, most notably the Anti-realism of Michael Dummett. In philosophy, the term anti-realism is used to describe any position involving either the denial of the objective reality of entities of a certain type or the insistence that we should be agnostic about their real existence. ... Sir Michael Anthony Eardley Dummett (1925 - ) is a leading British philosopher, who has both written on the history of analytic philosophy, and made original contributions to the subject, particularly in the areas of philosophy of mathematics, philosophy of logic, philosophy of language and metaphysics. ...

Intuitionistic logic as a formal logical calculus

From a practical point of view, there is also a strong motivation for using intuitionistic logic. Indeed, if one goes for automated reasoning like in logical programming, then one obviously is not interested in mere statements of existence. A computer program is assumed to compute an answer, not to state that there is one. Thus, in applications, one usually looks for a witness for a given existence assertion. In addition, one may have concerns about a proof system which has a proof for ∃x : P(x), but which fails to prove P(b) for any concrete b it considers. Logic programming is a declarative programming paradigm in which a set of attributes that a solution should have are specified rather than set of steps to obtain such a solution. ...

In order to formalize intuitionistic logic in a mathematically precise way, both a model theory (by semantics) and an appropriate proof theory are needed. The syntax of formulæ of intuitionistic logic is similar to propositional logic or first-order logic. The obvious difference is that many tautologies of these classical logics can no longer be proven within intuitionistic logic. Examples include not only the law of excluded middle P ∨ ¬P, but also Peirce's Law ((P → Q) → P) → P. In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the models which underlie mathematical systems. ... In the main, semantics (from the Greek semantikos, or significant meaning, derived from sema, sign) is the study of meaning, in some sense of that term. ... Proof theory, studied as a branch of mathematical logic, represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. ... The first meaning of the term syntax, originating from the Greek words συν (sun, meaning ‘together’) and ταξις (taxis, meaning sequence/order), can be described as the study of the rules, or patterned relations that govern the way the words in a sentence come together. ... In mathematical logic the propositional calculus or sentential calculus is a formal deduction system whose atomic formulas are propositional variables. ... First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as there exists an x such that. ... In logic, a tautology is a statement which is true by its own definition. ... In logic, the law of excluded middle (tertium non datur in Latin) states that for any proposition P, it is true that (P ∨ ¬P). ... Peirces law in logic is named after the philosopher and logician Charles Sanders Peirce. ...

A more familiar example of a classical tautology which is invalid in intuitionistic logic concerns the so-called double negation elimination. In classical logic, both P → ¬¬P and also ¬¬P → P are theorems. In intuitionistic logic, only the first is a theorem: Double negation can be introduced, but it cannot be eliminated. The interpretation of negation in intuitionistic logic is different from its counterpart in classical logic. In classical logic, ¬P asserts that P is false; in intuitionistic logic, ¬P asserts that a proof of P is impossible. The asymmetry between the two implications above now becomes apparent. If P is provable, then it is certainly impossible to prove that there is no proof of P; this is the first implication. However, the second implication fails: Just because there is no proof that a proof of P is impossible, we cannot conclude from this absence that there is a proof of P. In logic and the propositional calculus, double negative elimination is a rule that states that double negatives can be removed from a proposition without changing its meaning: means the same as: Formally: ¬ ¬ A ∴ A Also: ¬ ¬ ¬ A ∴ ¬ A The rule of double negative introduction states the converse, that double negatives can...

The observation that many classically valid tautologies are not theorems of intuitionistic logic leads to the idea of weakening the proof theory of classical logic. This has for example been done by Gentzen with his sequent calculus LK, obtaining a weaker version, that he called LJ. This gives a suitable proof theory. Gerhard Gentzen (November 24, 1909 – August 4, 1945) was a German mathematician and logician. ... In proof theory and mathematical logic, the sequent calculus is a widely known deduction system for first-order logic (and propositional logic as a special case of it). ... In proof theory and mathematical logic, the sequent calculus is a widely known deduction system for first-order logic (and propositional logic as a special case of it). ...

The semantics are rather more complicated than for the classical, deterministic case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras. ... Kripke semantics (also known as possible world semantics, relational semantics, or frame semantics) is a formal semantics for modal logic systems, created in late 1950s and early 1960s by Saul Kripke. ...

Heyting algebra semantics

In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connnectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Then we have the useful theorem that a formula is a valid sentence of classical logic if and only if its value is 1 for any valuation---that is, for any assignment of values to its variables. In logic, a truth value, or truth-value, is a value indicating to what extent a statement is true. ... This article may be too technical for most readers to understand. ... Valuation can mean: Valuation (finance) Valuation (mathematics) This is a disambiguation page — a navigational aid which lists other pages that might otherwise share the same title. ...

A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from a Heyting algebra, of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value 1 for any valuation on any Heyting algebra. In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras. ...

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open sets of the real plane R². In this algebra, The ∧ and ∨ operations correspond to set intersection and union, and the value assigned to a formula A→B is the same as the value assigned to the formula ¬(A ∧ ¬B). The value assigned to ¬F is F^C°, the interior of the complement of value of F. The value that represents 1 (truth) is the entire set R². With these assignments, intuitionistically valid formulas are precisely those that are assigned the value 1.

For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be 1:

Value(¬(A ∧ ¬A)) =

(Value(A ∧ ¬A))^C° =

(Value(A) ∩ Value(¬A))^C° =

(X ∩ (Value(A))^C°)^C° =

(X ∩ X^C°)^C°

A theorem of topology tells us that X^C° is a subset of X^C, so the intersection is empty, leaving:

ø^C° = (R²)° = R²

So the valuation of this formula is true, and indeed the formula is valid.

But the law of the excluded middle, A∨¬A, can be shown to be invalid by letting the value of A be {y : y > 0 }. Then the value of ¬A is the interior of {y : y ≤ 0 }, which is {y : y < 0 }, and the value of the formula is the union of {y : y > 0 } and {y : y < 0 }, which is not the entire plane.

The infinite Heyting algebra described above gives a true valuation to all intuitionistically valid formulas, regardless of what values are assigned to the variables in a formula. Conversely, for every invalid formula, there is an assignment of values from this algebra to the variables that yields a false valuation for the formula. It can be shown that no finite Heyting algebra has this property.

Kripke semantics

Main article Kripke semantics Kripke semantics (also known as possible world semantics, relational semantics, or frame semantics) is a formal semantics for modal logic systems, created in late 1950s and early 1960s by Saul Kripke. ...

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics. Modal logic, or (less commonly) intensional logic is the branch of logic that deals with sentences that are qualified by modalities such as can, could, might, may, must, possibly, and necessarily, and others. ... Saul Kripke in 1983 Saul Aaron Kripke (b. ...

See also

• Intuitionism
• Intuitionistic Type Theory
• classical logic
• intermediate logics
• linear logic
• constructive proof
• Curry-Howard correspondence
• computability logic
• game semantics

In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach to mathematics as the constructive mental activity of humans. ... Intuitionistic Type Theory, or Constructive Type Theory, or Martin-Löf Type Theory or just Type Theory (with capital letters) is at the same time a functional programming language, a logic and a set theory based on the principles of mathematical constructivism. ... Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. ... Intermediate logics are intermediate between intuitionistic logic and classical logic in the sense that they contain theorems that are not provable in intuitionistic logic, without giving rise to the whole of classical logic. ... In mathematical logic, linear logic is a type of substructural logic that denies the structural rules of weakening and contraction. ... In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object. ... The Curry-Howard correspondence is the close relationship between computer programs and mathematical proofs; the correspondence is also known as the Curry-Howard isomorphism, or the formulae-as-types correspondence. ... Computability logic is a formal theory of computability, introduced by Giorgi Japaridze in 2003. ... Game semantics is an approach to the semantics of logic that bases the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player. ...

External links

• Stanford Encyclopedia of Philosophy entry