Intuitionistic logic
169262
222276881
2008-06-28T13:41:37Z
Classicalecon
4831766
/* Relation to other logics */ add ref.
'''Intuitionistic logic''', or '''constructivist logic''', is the [[symbolic logic]] system originally developed by [[Arend Heyting]] to provide a formal basis for [[Luitzen Egbertus Jan Brouwer|Brouwer]]'s programme of [[intuitionism]]. The system preserves [[Theory of justification|justification]], rather than [[truth]], across transformations yielding derived propositions. From a practical point of view, there is also a strong motivation for using intuitionistic logic, since it has the [[existence property]], making it also suitable for other forms of [[mathematical constructivism]].
==Syntax==
[[Image:Rieger-Nishimura.svg|thumb|right|280px|The Rieger-Nishimura lattice. Its nodes are the propositional formulas in one variable up to intuitionistic logical equivalence, ordered by intuitionistic logical implication.]]
The [[syntax]] of formulæ of intuitionistic logic is similar to [[propositional logic]] or [[first-order logic]]. However, intuitionistic connectives are not interdefinable 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 ¬ as the abbreviation {{nowrap|1=¬''A'' = (''A'' → ⊥)}}. In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.
Many [[Tautology (logic)|tautologies]] of classical logic can no longer be proven within intuitionistic logic. Examples include not only the [[law of excluded middle]] {{nowrap|''p'' ∨ ¬''p''}}, but also [[Peirce's law]] {{nowrap|((''p'' → ''q'') → ''p'') → ''p''}}, and even [[double negation elimination]]. In classical logic, both {{nowrap|''p'' → ¬¬''p''}} and also {{nowrap|¬¬''p'' → ''p''}} are theorems. In intuitionistic logic, only the former is a theorem: double negation can be introduced, but it cannot be eliminated.
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.
=== Sequent calculus ===
{{main|sequent calculus}}
[[Gerhard Gentzen|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.
=== Hilbert-style calculus ===
Intuitionistic logic can be defined using the following [[Hilbert-style deduction system|Hilbert-style 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
* THEN-1: φ → (χ → φ)
* THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
* AND-1: φ ∧ χ → φ
* AND-2: φ ∧ χ → χ
* AND-3: φ → (χ → (φ ∧ χ))
* OR-1: φ → φ ∨ χ
* OR-2: χ → φ ∨ χ
* OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
* FALSE: ⊥ → φ
To make this a system of first-order predicate logic, the [[generalization (logic)|generalization rules]]
* ∀-GEN: from ψ → φ infer ψ → (∀''x'' φ), if ''x'' is not free in ψ
* ∃-GEN: from φ → ψ infer (∃''x'' φ) → ψ, if ''x'' is not free in ψ
are added, along with the axioms
* PRED-1: (∀''x'' φ(''x'')) → φ(''t''), if no free occurrence of ''x'' in φ is bound by a quantifier quantifying a variable occurring in the term ''t''
* PRED-2: φ(''t'') → (∃''x'' φ(''x'')), with the same restriction as for PRED-1
====Optional connectives====
=====Negation=====
If one wishes to include a connective ¬ for negation rather than consider it an abbreviation for φ → ⊥, it is enough to add:
* NOT-1′: (φ → ⊥) → ¬φ
* NOT-2′: ¬φ → (φ → ⊥)
There are a number of alternatives available if one wishes to omit the connective ⊥ (false). For example,
one may replace the three axioms FALSE, NOT-1′, and NOT-2′ with the two axioms
* NOT-1: (φ → χ) → ((φ → ¬χ) → ¬φ)
* NOT-2: φ → (¬φ → χ)
as at [[Propositional calculus#Axioms]]. Alternatives to NOT-1 are (φ → ¬χ) → (χ → ¬φ) or (φ → ¬φ) → ¬φ.
=====Equivalence=====
The connective ↔ for equivalence may be treated as an abbreviation, with φ ↔ χ standing for
(φ → χ) ∧ (χ → φ). Alternatively, one may add the axioms
* IFF-1: (φ ↔ χ) → (φ → χ)
* IFF-2: (φ ↔ χ) → (χ → φ)
* IFF-3: (φ → χ) → ((χ → φ) → (φ ↔ χ))
IFF-1 and IFF-2 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 two-element [[Kripke frame]] <math>\circ{\longrightarrow}\circ</math> (in other words, that is not included in [[intermediate logic|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 constructivist semantics.
=== Non-interdefinability of operators ===
In classical propositional logic, it is possible to take one of [[logical conjunction|conjunction]], [[logical disjunction|disjunction]], or [[material conditional|implication]] as primitive, and define the other two in terms of it together with [[logical negation|negation]], such as in [[Jan Łukasiewicz|Łukasiewicz]]'s [[propositional logic#Example 1. Simple axiom system|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 function]]s. 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:
* <math>(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)</math>
* <math>(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)</math>
* <math>(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)</math>
* <math>(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)</math>
Conjunction versus implication:
* <math>(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)</math>
* <math>(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)</math>
* <math>(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)</math>
* <math>(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi) </math>
Disjunction versus implication:
* <math>(\phi \vee \psi) \to (\neg \phi \to \psi)</math>
* <math>(\neg \phi \vee \psi) \to (\phi \to \psi)</math>
* <math>\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)</math>
* <math>\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)</math>
Universal versus existential quantification:
* <math>(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))</math>
* <math>(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))</math>
* <math>(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))</math>
* <math>(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))</math>
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, "neither a nor b" is equivalent to "not a, and also not b". <!-- explain! -->
If we include equivalence in the list of connectives, some of the connectives become definable from others:
* <math>(\phi\leftrightarrow \psi) \leftrightarrow ((\phi \to \psi)\land(\psi\to\phi))</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\lor\psi) \leftrightarrow \psi)</math>
* <math>(\phi\to\psi) \leftrightarrow ((\phi\land\psi) \leftrightarrow \phi)</math>
* <math>(\phi\land\psi) \leftrightarrow ((\phi\to\psi)\leftrightarrow\phi)</math>
* <math>(\phi\land\psi) \leftrightarrow (((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)</math>
In particular, {∨, ↔, ⊥} and {∨, ↔, ¬} are complete bases of intuitionistic connectives.
As shown by [[Alexander Kuznetsov|Kuznetsov]], either of the following defined connectives can serve the role of a sole sufficient operator for intuitionistic logic:<ref>Alexander Chagrov, Michael Zakharyaschev, ''Modal Logic'', vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.</ref>
* <math>((p\lor q)\land\neg r)\lor(\neg p\land(q\leftrightarrow r)),</math>
* <math>p\to(q\land\neg r\land(s\lor t)).</math>
== Semantics ==
The semantics are rather more complicated than for the classical case. A model theory can be given by [[Heyting algebra]]s or, equivalently, by [[Kripke semantics]].
===Heyting algebra semantics===
In classical logic, we often discuss the [[truth value]]s that a formula can take. The values are usually chosen as the members of a [[Boolean algebra (structure)|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'''.<ref name="S-U">{{cite book | title = Lectures on the Curry-Howard Isomorphism | last = Sørensen | first = Morten Heine B | coauthors = Paweł Urzyczyn | year = 2006 | publisher = [[Elsevier]] | isbn = 0444520775 | series = Studies in Logic and the Foundations of Mathematics | page = 42 }}</ref> In this algebra, the ∧ and ∨ operations correspond to set intersection and union, and the value assigned to a formula ''A'' → ''B'' is int(''A''<sup>C</sup> ∪ ''B''), the [[interior (topology)|interior]] of the union of the value of ''B'' and the [[complement (set theory)|complement]] of the value of ''A''. The bottom element is the empty set ∅, and the top element is the entire line '''R'''. Negation is as usual defined as ¬''A'' = ''A'' → ∅, so the value of ¬''A'' reduces to int(''A''<sup>C</sup>), the interior of the complement of the value of ''A'', also known as the [[exterior (topology)|exterior]] of ''A''. With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line.<ref name="S-U"/>
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''))<sup>C</sup>) =
: int((Value(''A'') ∩ Value(¬''A''))<sup>C</sup>) =
: int((''X'' ∩ int((Value(''A''))<sup>C</sup>))<sup>C</sup>) =
: int((''X'' ∩ int(''X''<sup>C</sup>))<sup>C</sup>)
A theorem of [[topology]] tells us that int(''X''<sup>C</sup>) is a subset of ''X''<sup>C</sup>, so the intersection is empty, leaving:
: int(∅<sup>C</sup>) = 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 (logic)|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.<ref name="S-U"/> Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element.<ref>Alfred Tarski, ''Der Aussagenkalkül und die Topologie'', Fundamenta Mathematicae 31 (1938), 103–134. [http://matwbn.icm.edu.pl/tresc.php?wyd=1&tom=31]</ref><ref name="R-S">{{cite book | title = The Mathematics of Metamathematics | last = Rasiowa | first = Helena | coauthors = Roman Sikorski | year = 1963 | publisher = Państwowe Wydawn. Naukowe | isbn = | location = Warsaw |series = Monografie matematyczne | page = 385–386 }}</ref> No finite Heyting algebra has both these properties.<ref name="S-U"/>
===Kripke semantics===
{{main|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''' <ref name=Mosch-IntLog>[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic]. Written by [http://www.math.ucla.edu/~joan/ Joan Moschovakis]. Published in Stanford Encyclopedia of Philosophy.</ref>.
==Relation to other logics==
Intutionistic logic is related by [[duality (mathematics)|duality]] to a [[paraconsistent logic]] known as ''Brazilian logic'' or ''dual-intuitionistic logic''<ref>{{cite journal | author=Aoyama, Hiroshi | title= LK, LJ, Dual Intuitionistic Logic, and Quantum Logic | journal=Notre Dame Journal of Formal Logic | year=2004 | volume=45 | issue= 4 | pages= 193–213 | url= | doi=10.1305/ndjfl/1099238445}}</ref>.
==See also==
<div style="-moz-column-count:2; column-count:2;">
* [[Intuitionism]]
* [[BHK interpretation]]
* [[Intuitionistic Type Theory]]
* [[classical logic]]
* [[intermediate logics]]
* [[linear logic]]
* [[constructive proof]]
* [[Curry-Howard correspondence]]
* [[computability logic]]
* [[game semantics]]
* '''[[Heyting algebra]]'''
</div>
== Notes ==
{{reflist}}
==References==
* [[Dirk van Dalen|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.
==External links==
{{portalpar|Logic}}
*[[Stanford Encyclopedia of Philosophy]]: "[http://plato.stanford.edu/entries/logic-intuitionistic/ Intuitionistic Logic]" -- by Joan Moschovakis.
{{Logic}}
[[Category:Logic in computer science]]
[[Category:Mathematical logic]]
[[Category:Mathematical constructivism]]
[[Category:Systems of formal logic]]
[[cs:Intuicionistická logika]]
[[fr:Logique intuitionniste]]
[[it:Logica intuizionista]]
[[ja:直観論理]]
[[pl:Logika intuicjonistyczna]]