### Constructive logic

**Intuitionistic logic**, sometimes more generally called **constructive logic**, is a system of symbolic logic that differs from classical logic by replacing the traditional concept of truth with the concept of constructive provability. For example, in classical logic, propositional formulae are always assigned a truth value from the two element set of trivial propositions $\backslash \{\backslash top,\; \backslash bot\backslash \}$ ("true" and "false" respectively) regardless of whether we have direct evidence for either case. In contrast, propositional formulae in intuitionistic logic are *not* assigned any definite truth value at all and instead *only* considered "true" when we have direct evidence, hence *proof*. (We can also say, instead of the propositional formula being "true" due to direct evidence, that it is inhabited by a proof in the Curry-Howard sense.) Operations in intuitionistic logic therefore preserve justification, with respect to evidence and provability, rather than truth-valuation. A consequence of this point of view is that intuitionistic logic is not a two-valued logic, nor even a finite-valued logic, in the familiar sense: although intuitionistic logic retains the trivial propositions $\backslash \{\backslash top,\; \backslash bot\backslash \}$ from classical logic, each *proof* of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

Semantically, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not admitted as axioms. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic.

Several semantics for intuitionistic logic have been studied. One semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models.

Intuitionistic logic is practically useful because its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if you have a constructive proof that an object exists, you can turn that constructive proof into an algorithm for generating an example of it.

Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism.

## Contents

## Syntax

The syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. In intuitionistic propositional logic it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬*A* as an abbreviation for (*A* → ⊥). In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.

Many tautologies of classical logic 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*, and even double negation elimination. In classical logic, both *p* → ¬¬*p* and also ¬¬*p* → *p* are theorems. In intuitionistic logic, only the former is a theorem: double negation can be introduced, but it cannot be eliminated. Rejecting *p* ∨ ¬*p* may seem strange to those more familiar with classical logic, but proving this propositional formula in intuitionistic logic would require producing a proof for the truth or falsity of *all possible propositional formulae*, which is impossible for a variety of reasons.

Because many classically valid tautologies are not theorems of intuitionistic logic, but all theorems of intuitionistic logic are valid classically, intuitionistic logic can be viewed as a weakening of classical logic, albeit one with many useful properties.

### Sequent calculus

Gentzen discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system which is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.

Other derivatives of LK are limited to intuitionisitic derivations but still allow multiple conclusions in a sequent. LJ' ^{[1]} is one example.

### Hilbert-style calculus

Intuitionistic logic can be defined using the following Hilbert-style calculus. This is similar to a way of axiomatizing classical propositional logic.

In propositional logic, the inference rule is modus ponens

- MP: from $\backslash phi$ and $\backslash phi\; \backslash to\; \backslash psi$ infer $\backslash psi$

and the axioms are

- THEN-1: $\backslash phi\; \backslash to\; (\backslash chi\; \backslash to\; \backslash phi\; )$
- THEN-2: $(\backslash phi\; \backslash to\; (\backslash chi\; \backslash to\; \backslash psi\; ))\; \backslash to\; ((\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; (\backslash phi\; \backslash to\; \backslash psi\; ))$
- AND-1: $\backslash phi\; \backslash land\; \backslash chi\; \backslash to\; \backslash phi$
- AND-2: $\backslash phi\; \backslash land\; \backslash chi\; \backslash to\; \backslash chi$
- AND-3: $\backslash phi\; \backslash to\; (\backslash chi\; \backslash to\; (\backslash phi\; \backslash land\; \backslash chi\; ))$
- OR-1: $\backslash phi\; \backslash to\; \backslash phi\; \backslash lor\; \backslash chi$
- OR-2: $\backslash chi\; \backslash to\; \backslash phi\; \backslash lor\; \backslash chi$
- OR-3: $(\backslash phi\; \backslash to\; \backslash psi\; )\; \backslash to\; ((\backslash chi\; \backslash to\; \backslash psi\; )\; \backslash to\; (\backslash phi\; \backslash lor\; \backslash chi\; \backslash to\; \backslash psi\; ))$
- FALSE: $\backslash bot\; \backslash to\; \backslash phi$

To make this a system of first-order predicate logic, the generalization rules

- $\backslash forall$-GEN: from $\backslash psi\; \backslash to\; \backslash phi$ infer $\backslash psi\; \backslash to\; (\backslash forall\; x\; \backslash \; \backslash phi\; )$, if $x$ is not free in $\backslash psi$
- $\backslash exists$-GEN: from $\backslash phi\; \backslash to\; \backslash psi$ infer $(\backslash exists\; x\; \backslash \; \backslash phi\; )\; \backslash to\; \backslash psi$, if $x$ is not free in $\backslash psi$

are added, along with the axioms

- PRED-1: $(\backslash forall\; x\; \backslash \; \backslash phi\; (x))\; \backslash to\; \backslash phi\; (t)$, if the term
*t*is free for substitution for the variable*x*in $\backslash phi$ (i.e., if no occurrence of any variable in*t*becomes bound in $\backslash phi\; (t)$) - PRED-2: $\backslash phi\; (t)\; \backslash to\; (\backslash exists\; x\; \backslash \; \backslash phi\; (x))$, with the same restriction as for PRED-1

#### Optional connectives

##### Negation

If one wishes to include a connective $\backslash lnot$ for negation rather than consider it an abbreviation for $\backslash phi\; \backslash to\; \backslash bot$, it is enough to add:

- NOT-1': $(\backslash phi\; \backslash to\; \backslash bot\; )\; \backslash to\; \backslash lnot\; \backslash phi$
- NOT-2': $\backslash lnot\; \backslash phi\; \backslash to\; (\backslash phi\; \backslash to\; \backslash bot\; )$

There are a number of alternatives available if one wishes to omit the connective $\backslash bot$ (false). For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms

- NOT-1: $(\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; ((\backslash phi\; \backslash to\; \backslash lnot\; \backslash chi\; )\; \backslash to\; \backslash lnot\; \backslash phi\; )$
- NOT-2: $\backslash phi\; \backslash to\; (\backslash lnot\; \backslash phi\; \backslash to\; \backslash chi\; )$

as at Propositional calculus#Axioms. Alternatives to NOT-1 are $(\backslash phi\; \backslash to\; \backslash lnot\; \backslash chi\; )\; \backslash to\; (\backslash chi\; \backslash to\; \backslash lnot\; \backslash phi\; )$ or $(\backslash phi\; \backslash to\; \backslash lnot\; \backslash phi\; )\; \backslash to\; \backslash lnot\; \backslash phi$.

##### Equivalence

The connective $\backslash leftrightarrow$ for equivalence may be treated as an abbreviation, with $\backslash phi\; \backslash leftrightarrow\; \backslash chi$ standing for $(\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash land\; (\backslash chi\; \backslash to\; \backslash phi\; )$. Alternatively, one may add the axioms

- IFF-1: $(\backslash phi\; \backslash leftrightarrow\; \backslash chi\; )\; \backslash to\; (\backslash phi\; \backslash to\; \backslash chi\; )$
- IFF-2: $(\backslash phi\; \backslash leftrightarrow\; \backslash chi\; )\; \backslash to\; (\backslash chi\; \backslash to\; \backslash phi\; )$
- IFF-3: $(\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; ((\backslash chi\; \backslash to\; \backslash phi\; )\; \backslash to\; (\backslash phi\; \backslash leftrightarrow\; \backslash chi\; ))$

IFF-1 and IFF-2 can, if desired, be combined into a single axiom $(\backslash phi\; \backslash leftrightarrow\; \backslash chi\; )\; \backslash to\; ((\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash land\; (\backslash chi\; \backslash to\; \backslash phi\; ))$ using conjunction.

#### Relation to classical logic

The system of classical logic is obtained by adding any one of the following axioms:

- $\backslash phi\; \backslash lor\; \backslash lnot\; \backslash phi$ (Law of the excluded middle. May also be formulated as $(\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; ((\backslash lnot\; \backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; \backslash chi\; )$.)
- $\backslash lnot\; \backslash lnot\; \backslash phi\; \backslash to\; \backslash phi$ (Double negation elimination)
- $((\backslash phi\; \backslash to\; \backslash chi\; )\; \backslash to\; \backslash phi\; )\; \backslash to\; \backslash phi$ (Peirce's law)

In general, one may take as the extra axiom any classical tautology that is not valid in the two-element Kripke frame $\backslash circ\{\backslash longrightarrow\}\backslash circ$ (in other words, that is not included in Smetanich's logic).

Another relationship is given by the Gödel–Gentzen negative translation, which provides an embedding of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. Therefore intuitionistic logic can instead be seen as a means of extending classical logic with constructive semantics.

In 1932, Kurt Gödel defined a system of Gödel logics intermediate between classical and intuitionistic logic; such logics are known as intermediate logics.

#### Relation to many-valued logic

Kurt Gödel in 1932 showed that intuitionistic logic is not a finitely-many valued logic. (See the section titled Heyting algebra semantics below for a sort of "infinitely-many valued logic" interpretation of intuitionistic logic.)

### Non-interdefinability of operators

In classical propositional logic, it is possible to take one of conjunction, disjunction, or implication as primitive, and define the other two in terms of it together with negation, such as in Łukasiewicz's three axioms of propositional logic. It is even possible to define all four in terms of a sole sufficient operator such as the Peirce arrow (NOR) or Sheffer stroke (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.

These are fundamentally consequences of the law of bivalence, which makes all such connectives merely Boolean functions. The law of bivalence does not hold in intuitionistic logic, only the law of non-contradiction. As a result none of the basic connectives can be dispensed with, and the above axioms are all necessary. Most of the classical identities are only theorems of intuitionistic logic in one direction, although some are theorems in both directions. They are as follows:

Conjunction versus disjunction:

- $(\backslash phi\; \backslash wedge\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash neg\; \backslash phi\; \backslash vee\; \backslash neg\; \backslash psi)$
- $(\backslash phi\; \backslash vee\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash neg\; \backslash phi\; \backslash wedge\; \backslash neg\; \backslash psi)$
- $(\backslash neg\; \backslash phi\; \backslash vee\; \backslash neg\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash phi\; \backslash wedge\; \backslash psi)$
- $(\backslash neg\; \backslash phi\; \backslash wedge\; \backslash neg\; \backslash psi)\; \backslash leftrightarrow\; \backslash neg\; (\backslash phi\; \backslash vee\; \backslash psi)$

Conjunction versus implication:

- $(\backslash phi\; \backslash wedge\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash phi\; \backslash to\; \backslash neg\; \backslash psi)$
- $(\backslash phi\; \backslash to\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash phi\; \backslash wedge\; \backslash neg\; \backslash psi)$
- $(\backslash phi\; \backslash wedge\; \backslash neg\; \backslash psi)\; \backslash to\; \backslash neg\; (\backslash phi\; \backslash to\; \backslash psi)$
- $(\backslash phi\; \backslash to\; \backslash neg\; \backslash psi)\; \backslash leftrightarrow\; \backslash neg\; (\backslash phi\; \backslash wedge\; \backslash psi)$

Disjunction versus implication:

- $(\backslash phi\; \backslash vee\; \backslash psi)\; \backslash to\; (\backslash neg\; \backslash phi\; \backslash to\; \backslash psi)$
- $(\backslash neg\; \backslash phi\; \backslash vee\; \backslash psi)\; \backslash to\; (\backslash phi\; \backslash to\; \backslash psi)$

Universal versus existential quantification:

- $(\backslash forall\; x\; \backslash \; \backslash phi(x))\; \backslash to\; \backslash neg\; (\backslash exists\; x\; \backslash \; \backslash neg\; \backslash phi(x))$
- $(\backslash exists\; x\; \backslash \; \backslash phi(x))\; \backslash to\; \backslash neg\; (\backslash forall\; x\; \backslash \; \backslash neg\; \backslash phi(x))$
- $(\backslash exists\; x\; \backslash \; \backslash neg\; \backslash phi(x))\; \backslash to\; \backslash neg\; (\backslash forall\; x\; \backslash \; \backslash phi(x))$
- $(\backslash forall\; x\; \backslash \; \backslash neg\; \backslash phi(x))\; \backslash leftrightarrow\; \backslash neg\; (\backslash exists\; x\; \backslash \; \backslash phi(x))$

So, for example, "a or b" is a stronger propositional formula than "if not a, then b", whereas these are classically interchangeable. On the other hand, "not (a or b)" is equivalent to "not a, and also not b".

If we include equivalence in the list of connectives, some of the connectives become definable from others:

- $(\backslash phi\backslash leftrightarrow\; \backslash psi)\; \backslash leftrightarrow\; ((\backslash phi\; \backslash to\; \backslash psi)\backslash land(\backslash psi\backslash to\backslash phi))$
- $(\backslash phi\backslash to\backslash psi)\; \backslash leftrightarrow\; ((\backslash phi\backslash lor\backslash psi)\; \backslash leftrightarrow\; \backslash psi)$
- $(\backslash phi\backslash to\backslash psi)\; \backslash leftrightarrow\; ((\backslash phi\backslash land\backslash psi)\; \backslash leftrightarrow\; \backslash phi)$
- $(\backslash phi\backslash land\backslash psi)\; \backslash leftrightarrow\; ((\backslash phi\backslash to\backslash psi)\backslash leftrightarrow\backslash phi)$
- $(\backslash phi\backslash land\backslash psi)\; \backslash leftrightarrow\; (((\backslash phi\backslash lor\backslash psi)\backslash leftrightarrow\backslash psi)\backslash leftrightarrow\backslash phi)$

In particular, {∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives.

As shown by Alexander Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself functionally complete: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the Sheffer stroke from classical propositional logic:^{[2]}

- $((p\backslash lor\; q)\backslash land\backslash neg\; r)\backslash lor(\backslash neg\; p\backslash land(q\backslash leftrightarrow\; r)),$
- $p\backslash to(q\backslash land\backslash neg\; r\backslash land(s\backslash lor\; t)).$

## Semantics

The semantics are rather more complicated than for the classical case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. Recently, a Tarski-like model theory was proved complete by Bob Constable, but with a different notion of completeness than classically.

### 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 connectives, 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 proposition of classical logic if and only if its value is 1 for every valuation—that is, for any assignment of values to its variables.

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 of the top element for any valuation on any Heyting algebra.

It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line **R**.^{[3]} In this algebra, the ∧ and ∨ operations correspond to set intersection and union, and the value assigned to a formula *A* → *B* is int(*A*^{C} ∪ *B*), the interior of the union of the value of *B* and the complement of the value of *A*. The bottom element is the empty set ∅, and the top element is the entire line **R**. The negation ¬*A* of a formula *A* is (as usual) defined to be *A* → ∅. The value of ¬*A* then reduces to int(*A*^{C}), the interior of the complement of the value of *A*, also known as the exterior of *A*. With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line.^{[3]}

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 the entire line:

- Value(¬(
*A*∧ ¬*A*)) = - int((Value(
*A*∧ ¬*A*))^{C}) = - int((Value(
*A*) ∩ Value(¬*A*))^{C}) = - int((
*X*∩ int((Value(*A*))^{C}))^{C}) = - int((
*X*∩ int(*X*^{C}))^{C})

A theorem of topology tells us that int(*X*^{C}) is a subset of *X*^{C}, so the intersection is empty, leaving:

- int(∅
^{C}) = int(**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 {*y* : *y* ≠ 0 }, *not* the entire line.

The interpretation of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula.^{[3]} Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.^{[4]}^{[5]} No finite Heyting algebra has both these properties.^{[3]}

### Kripke semantics

Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as **Kripke semantics** or **relational semantics**.^{[6]}

### Tarski-like semantics

It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, Robert Constable has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true *in the same way* in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.^{[7]}

## Relation to other logics

Intuitionistic logic is related by duality to a paraconsistent logic known as *Brazilian*, *anti-intuitionistic* or *dual-intuitionistic logic*.^{[8]}

The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic.

## See also

**
**

## Notes

## References

- van Dalen, Dirk, 2001, "Intuitionistic Logic", in Goble, Lou, ed.,
*The Blackwell Guide to Philosophical Logic*. Blackwell. - Morten H. Sørensen, Paweł Urzyczyn, 2006,
*Lectures on the Curry-Howard Isomorphism*(chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier. - W. A. Carnielli (with A. B.M. Brunner)."Anti-intuitionism and paraconsistency". Journal of Applied Logic Volume 3, Issue 1, March 2005, pages 161-184.

## External links

- Intuitionistic Logic"—by Joan Moschovakis.
- University of Amsterdam)
- Semantical Analysis of Intuitionistic Logic I by Saul A. Kripke from
*Harvard University, Cambridge, Mass., USA* - Dirk van Dalen
- The discovery of E.W. Beth's semantics for intuitionistic logic by A.S. Troelstra and P. van Ulsen
- Expressing Database Queries with Intuitionistic Logic (
*FTP one-click download*) by Anthony J. Bonner. L. Thorne McCarty. Kumar Vadaparty. Rutgers University, Department of Computer Science.