
Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. 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 symbolic logic. While it may be argued whether such a formal calculus#Other_uses_of_the_term really captures the philosophical aspects of intuitionism, it has properties which are also quite useful from a practical point of view. 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 an abstract sense. In intuitionistic logic, a formula is only considered to be true if it can be ''proved''. As an example of this difference, law of excluded middle, while classically valid, is not intuitionistically valid, because, in a logical calculus that allows it, it's possible to argue ''P'' ∨ ¬''P'' without knowing which one specifically is the case. This is fine if one assumes that the law of the excluded middle is some kind of subtle truth inherent in the nature of being; but if the validity of a mental construct is entirely dependent upon its coherence with its context (the mind), then epistemological opacity is, in effect, cheating. In intuitionistic logic, it is not permitted to assert a disjunction such as ''P'' ∨ ¬''P'' without also being able to say specifically which one is true. More generally, the formula ''P'' ∨ ¬''P'' is not a theorem of intuitionistic logic as it is of classical logic. In classical logic, ''P'' ∨ ¬''P'' means that one of ''P'' or ¬''P'' is ''true''; in intuitionistic logic, ''P'' ∨ ¬''P'' means that one of ''P'' or ¬''P'' can be ''proved'', which is a much stronger statement, and which might not always be the case. Intuitionistic logic substitutes ''justification'' for truth in its logical calculus. Instead of a deterministic, bivalent truth assignment scheme, it allows for a third, indeterminate truth value. A proposition may be provably justified, or provably not justified, or undetermined. 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. ==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. 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 calculus or first-order logic. The obvious difference is that many tautology 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''. 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''. 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 Gerhard Gentzen with his sequent calculus, obtaining a weaker version, that he called sequent calculus. This gives a suitable proof theory. The semantics are rather more complicated than for the classical, two-valued case. A model theory can be given by Heyting algebra or, equivalently, by Kripke semantics. ==Heyting algebra semantics== A valuation (mathematics) on propositional variables can be given by assigning elements of a Heyting algebra. The valuation can then be extended to formulæ by matching the propositional connectives with their corresponding operations in the algebra. A valid sentence is then one which has valuation 1 in any valuation on any Heyting algebra. It can be shown that we need in fact consider only the Heyting algebra given by the open sets of the real plane with its usual topology—intuitionistic validities correspond precisely to Heyting formulae which evaluate to the entire plane for any assignment of open subsets to the variables. For example, the law of the excluded middle can then easily be seen not to be valid: Let ''A'' be the strict upper plane {(''x'', ''y'') : ''y'' > 0}. Then ¬''A'' is the strict lower plane Int(R2 \ ''A'') = {(''x'', ''y'') : ''y'' < 0}, so ''A'' ∨ ¬''A'' = {(''x'', ''y'') : ''y'' ≠ 0} ≠ R2. So we do not have |= ''P'' ∨ ¬''P'' in intuitionistic logic. ==Kripke semantics== ''Main article 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. ==See also== * Intuitionism * Intuitionistic Type Theory * classical logic * intermediate logics * linear logic * constructive proof * Curry-Howard correspondence * computability logic * game semantics ==External links== * [http://plato.stanford.edu/entries/logic-intuitionistic/ Stanford Encyclopedia of Philosophy entry] Logic Logic in computer science Mathematical logic
Very nice start to the article. A bit POV, though, it's kind of obvious it's written by an advocate of intuitionism. But still good start. Ummm ... isn't it a bit narrow-based around the assumption of that old chestnut, intuitionism as one of the three main philosophies of mathematics? The Kolmogorov interpretation may have been the first step clear of that. Certainly the Brouwer not not not = not result needs a mention, too. Goedel used IL at one juncture, and after that, historically speaking, wasn't IL respectable in a technical sense? What happened then in relation to Markov was perhaps confusing. Anyway, there are several strands to disentangle here: this is a bit ahistorical for me. User:Charles Matthews 10:36, 15 Oct 2003 (UTC) ==my take== Terms should not be equivocated. Speakers end up suggesting that not isn't not, so classical logicians should use a term meaning the exact opposite: un. User:Lysdexia 00:16, 13 Nov 2004 (UTC) == I don't get it. How is this an example? == In the "law of the excluded middle" example under "Heyting algebra", is divvied up into a set A and its complement, the first comprising . Now, it would seem to me that the complement of A would be . However, it's given as , which is then used to show that the plane isn't included in the union of A and not-A. How can this be? User:Grendelkhan|User_talk:Grendelkhan 03:45, 2005 Jan 14 (UTC) :It's really badly explained. But the idea is that if you consider subsets of , they form a Heyting algebra if you consider "or" and "and" to be set union and intersection, and (this is they key point) the complement of ''X'' to be the ''interior'' of . Then the complement of the open upper half-plane is the ''open'' lower half-plane. The axioms of the Heyting algebra are satisfied in this case, but the law that doesn't hold. -- User:Dominus 12:30, 14 Jan 2005 (UTC)
See other meanings of words starting from letter:
Words begining with Intuitionistic_logic:
Intuitionistic_logic
Intuitionistic_logic
Intuitionistic logic
Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. 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 symbolic logic. While it may be argued whether such a formal calculus#Other_uses_of_the_term really captures the philosophical aspects of intuitionism, it has properties which are also quite useful from a practical point of view. 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 an abstract sense. In intuitionistic logic, a formula is only considered to be true if it can be ''proved''. As an example of this difference, law of excluded middle, while classically valid, is not intuitionistically valid, because, in a logical calculus that allows it, it's possible to argue ''P'' ∨ ¬''P'' without knowing which one specifically is the case. This is fine if one assumes that the law of the excluded middle is some kind of subtle truth inherent in the nature of being; but if the validity of a mental construct is entirely dependent upon its coherence with its context (the mind), then epistemological opacity is, in effect, cheating. In intuitionistic logic, it is not permitted to assert a disjunction such as ''P'' ∨ ¬''P'' without also being able to say specifically which one is true. More generally, the formula ''P'' ∨ ¬''P'' is not a theorem of intuitionistic logic as it is of classical logic. In classical logic, ''P'' ∨ ¬''P'' means that one of ''P'' or ¬''P'' is ''true''; in intuitionistic logic, ''P'' ∨ ¬''P'' means that one of ''P'' or ¬''P'' can be ''proved'', which is a much stronger statement, and which might not always be the case. Intuitionistic logic substitutes ''justification'' for truth in its logical calculus. Instead of a deterministic, bivalent truth assignment scheme, it allows for a third, indeterminate truth value. A proposition may be provably justified, or provably not justified, or undetermined. 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. ==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. 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 calculus or first-order logic. The obvious difference is that many tautology 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''. 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''. 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 Gerhard Gentzen with his sequent calculus, obtaining a weaker version, that he called sequent calculus. This gives a suitable proof theory. The semantics are rather more complicated than for the classical, two-valued case. A model theory can be given by Heyting algebra or, equivalently, by Kripke semantics. ==Heyting algebra semantics== A valuation (mathematics) on propositional variables can be given by assigning elements of a Heyting algebra. The valuation can then be extended to formulæ by matching the propositional connectives with their corresponding operations in the algebra. A valid sentence is then one which has valuation 1 in any valuation on any Heyting algebra. It can be shown that we need in fact consider only the Heyting algebra given by the open sets of the real plane with its usual topology—intuitionistic validities correspond precisely to Heyting formulae which evaluate to the entire plane for any assignment of open subsets to the variables. For example, the law of the excluded middle can then easily be seen not to be valid: Let ''A'' be the strict upper plane {(''x'', ''y'') : ''y'' > 0}. Then ¬''A'' is the strict lower plane Int(R2 \ ''A'') = {(''x'', ''y'') : ''y'' < 0}, so ''A'' ∨ ¬''A'' = {(''x'', ''y'') : ''y'' ≠ 0} ≠ R2. So we do not have |= ''P'' ∨ ¬''P'' in intuitionistic logic. ==Kripke semantics== ''Main article 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. ==See also== * Intuitionism * Intuitionistic Type Theory * classical logic * intermediate logics * linear logic * constructive proof * Curry-Howard correspondence * computability logic * game semantics ==External links== * [http://plato.stanford.edu/entries/logic-intuitionistic/ Stanford Encyclopedia of Philosophy entry] Logic Logic in computer science Mathematical logic
Intuitionistic logic
Very nice start to the article. A bit POV, though, it's kind of obvious it's written by an advocate of intuitionism. But still good start. Ummm ... isn't it a bit narrow-based around the assumption of that old chestnut, intuitionism as one of the three main philosophies of mathematics? The Kolmogorov interpretation may have been the first step clear of that. Certainly the Brouwer not not not = not result needs a mention, too. Goedel used IL at one juncture, and after that, historically speaking, wasn't IL respectable in a technical sense? What happened then in relation to Markov was perhaps confusing. Anyway, there are several strands to disentangle here: this is a bit ahistorical for me. User:Charles Matthews 10:36, 15 Oct 2003 (UTC) ==my take== Terms should not be equivocated. Speakers end up suggesting that not isn't not, so classical logicians should use a term meaning the exact opposite: un. User:Lysdexia 00:16, 13 Nov 2004 (UTC) == I don't get it. How is this an example? == In the "law of the excluded middle" example under "Heyting algebra", is divvied up into a set A and its complement, the first comprising . Now, it would seem to me that the complement of A would be . However, it's given as , which is then used to show that the plane isn't included in the union of A and not-A. How can this be? User:Grendelkhan|User_talk:Grendelkhan 03:45, 2005 Jan 14 (UTC) :It's really badly explained. But the idea is that if you consider subsets of , they form a Heyting algebra if you consider "or" and "and" to be set union and intersection, and (this is they key point) the complement of ''X'' to be the ''interior'' of . Then the complement of the open upper half-plane is the ''open'' lower half-plane. The axioms of the Heyting algebra are satisfied in this case, but the law that doesn't hold. -- User:Dominus 12:30, 14 Jan 2005 (UTC)
See other meanings of words starting from letter:
I
IA | IB | IC | ID | IE | IF | IG | IH | IJ | IK | IL | IM | IN | IO | IP | IR | IS | IT | IU | IW | IX | IY | IZ |Words begining with Intuitionistic_logic:
Intuitionistic_logic
Intuitionistic_logic
These materials are based on Wikipedia and licensed under the GNU FDL
YouTube.com videos better site than Turbo Tax 2007
