 Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all wellformed statements are assumed to be either true or false, even if we do not have a proof of either. In constructive logic, a statement is 'only true' if there is a constructive proof that it is true, and 'only false' if there is a constructive proof that it is false. Operations in constructive logic preserve justification, rather than truth.
Syntactically, intuitionist logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not axioms of the system, and cannot be proved. There are several semantics commonly employed. One semantics mirrors classical Booleanvalued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models.
Constructive 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 given a constructive proof that an object exists, then that constructive proof can be turned 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 firstorder 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 firstorder 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 statement in constructive logic would require producing a proof for the truth or falsity of all possible statements, which is impossible for a variety of reasons.
Because many classically valid tautologies are not theorems of intuitionistic logic, but all theorems of intuitionist logic are valid classically, intuitionist logic can be viewed as a weakening of classical logic, albeit one with many useful properties.
Sequent calculus
Main article: Sequent calculusGentzen 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 intuitionstic derivations but still allow multiple conclusions in a sequent. LJ' ^{[1]} is one example.
Hilbertstyle calculus
Intuitionistic logic can be defined using the following Hilbertstyle calculus. Compare with the deduction system at Propositional calculus#Alternative calculus.
In propositional logic, the inference rule is modus ponens
 MP: from ϕ and infer ψ
and the axioms are
 THEN1:
 THEN2:
 AND1:
 AND2:
 AND3:
 OR1:
 OR2:
 OR3:
 FALSE:
To make this a system of firstorder predicate logic, the generalization rules
 GEN: from infer , if x is not free in ψ
 GEN: from infer , if x is not free in ψ
are added, along with the axioms
 PRED1: , if the term t is free for substitution for the variable x in ϕ (i.e., if no occurrence of any variable in t becomes bound in φ(t))
 PRED2: , with the same restriction as for PRED1
Optional connectives
Negation
If one wishes to include a connective for negation rather than consider it an abbreviation for , it is enough to add:
 NOT1':
 NOT2':
There are a number of alternatives available if one wishes to omit the connective (false). For example, one may replace the three axioms FALSE, NOT1', and NOT2' with the two axioms
 NOT1:
 NOT2:
as at Propositional calculus#Axioms. Alternatives to NOT1 are or .
Equivalence
The connective for equivalence may be treated as an abbreviation, with standing for . Alternatively, one may add the axioms
 IFF1:
 IFF2:
 IFF3:
IFF1 and IFF2 can, if desired, be combined into a single axiom using conjunction.
Relation to classical logic
The system of classical logic is obtained by adding any one of the following axioms:
 (Law of the excluded middle. May also be formulated as .)
 (Double negation elimination)
 (Peirce's law)
In general, one may take as the extra axiom any classical tautology that is not valid in the twoelement Kripke frame (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 firstorder logic into intuitionistic logic: a firstorder 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 manyvalued logic
Kurt Gödel in 1932 showed that intuitionistic logic is not a finitelymany valued logic. (See the section titled Heyting algebra semantics below for a sort of "infinitelymany valued logic" interpretation of intuitionistic logic.)
Noninterdefinability 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 firstorder 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 noncontradiction. 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:
Conjunction versus implication:
Disjunction versus implication:
Universal versus existential quantification:
So, for example, "a or b" is a stronger statement 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:
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]}
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.
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 sentence 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
Main article: Kripke semanticsBuilding upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.^{[6]}
Relation to other logics
Intutionistic logic is related by duality to a paraconsistent logic known as Brazilian, antiintuitionistic or dualintuitionistic logic.^{[7]}
The subsystem of intuitionistic logic with the FALSE axiom removed is known as minimal logic.
See also
 BHK interpretation
 Intuitionistic Type Theory
 Intermediate logics
 Linear logic
 Constructive proof
 CurryHoward correspondence
 Computability logic
 Game semantics
 Smooth infinitesimal analysis
Notes
 ^ Proof Theory by G. Takeuti, ISBN0444104925
 ^ Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59. ISBN 0198537794.
 ^ ^{a} ^{b} ^{c} ^{d} Sørensen, Morten Heine B; Paweł Urzyczyn (2006). Lectures on the CurryHoward Isomorphism. Studies in Logic and the Foundations of Mathematics. Elsevier. p. 42. ISBN 0444520775.
 ^ Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae 31 (1938), 103–134. [1]
 ^ Rasiowa, Helena; Roman Sikorski (1963). The Mathematics of Metamathematics. Monografie matematyczne. Warsaw: Państwowe Wydawn. Naukowe. pp. 385–386.
 ^ Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.
 ^ Aoyama, Hiroshi (2004). "LK, LJ, Dual Intuitionistic Logic, and Quantum Logic". Notre Dame Journal of Formal Logic 45 (4): 193–213. doi:10.1305/ndjfl/1099238445.
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 CurryHoward Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.
 W. A. Carnielli (with A. B.M. Brunner)."Antiintuitionism and paraconsistency". Journal of Applied Logic Volume 3, Issue 1, March 2005, pages 161184.
External links
 Stanford Encyclopedia of Philosophy: "Intuitionistic Logic"  by Joan Moschovakis.
Categories: Logic in computer science
 Nonclassical logic
 Mathematical constructivism
 Systems of formal logic
 Intuitionism
Wikimedia Foundation. 2010.
Look at other dictionaries:
intuitionistic logic — The logical system developed initially by A. Heyting (b. 1898) to formalize the reasonings allowed by mathematical intuitionism . It is designed so that p ∨ ¬ p is not a theorem, and the rule of inference from ¬¬ p to p is disallowed (the logic… … Philosophy dictionary
intuitionistic logic — noun A type of logic which rejects the axiom law of excluded middle or, equivalently, the law of double negation and/or Peirces law. It is the foundation of intuitionism. Just because is not axiomatically true (for all P) does not mean that is… … Wiktionary
Intuitionistic type theory — Intuitionistic type theory, or constructive type theory, or Martin Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per… … Wikipedia
Logic (disambiguation) — Logic is the study of the principles and criteria of valid inference and demonstration.Logic may also refer to:In logic and mathematics*A branch of logic: **Inductive logic, also called induction or inductive reasoning **Informal logic, the study … Wikipedia
logic, history of — Introduction the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic There was a medieval tradition according to which the Greek philosopher … Universalium
Logic — For other uses, see Logic (disambiguation). Philosophy … Wikipedia
logic, philosophy of — Philosophical study of the nature and scope of logic. Examples of questions raised in the philosophy of logic are: In virtue of what features of reality are the laws of logic true? ; How do we know the truths of logic? ; and Could the laws of… … Universalium
Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… … Wikipedia
Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… … Wikipedia
Paraconsistent logic — A paraconsistent logic is a logical system that attempts to deal with contradictions in a discriminating way. Alternatively, paraconsistent logic is the subfield of logic that is concerned with studying and developing paraconsistent (or… … Wikipedia