Intuitionistic logic
From The Art and Popular Culture Encyclopedia
(Difference between revisions)
| Revision as of 05:40, 8 October 2014 Jahsonic (Talk | contribs) ← Previous diff |
Current revision Jahsonic (Talk | contribs) |
||
| Line 1: | Line 1: | ||
| {{Template}} | {{Template}} | ||
| - | The '''principle of explosion''' ([[Latin]]: ''ex falso quodlibet'', "from a falsehood, anything follows", or ''ex contradictione sequitur quodlibet'', "from a contradiction, anything follows"), or the '''principle of Pseudo-Scotus''', is the law of [[classical logic]], [[intuitionistic logic]] and similar logical systems, according to which any statement can be proven from a contradiction. That is, once a contradiction has been asserted, any proposition (or its negation) can be inferred from it. | + | '''Intuitionistic logic''', sometimes more generally called '''constructive logic''', is a system of [[Mathematical logic|symbolic logic]] that differs from [[classical logic]] by replacing the traditional concept of truth with the concept of [[constructive proof|constructive provability]]. For example, in classical logic, [[propositional formula]]e are always assigned a [[truth value]] from the two element set of trivial [[proposition (mathematics)|propositions]] <math>\{\top, \bot\}</math> ("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 set|inhabited]] by a proof in the [[Curry-Howard correspondence|Curry-Howard]] sense.) Operations in intuitionistic logic therefore preserve [[Theory of justification|justification]], with respect to evidence and provability, rather than truth-valuation. |
| - | + | ||
| - | As a demonstration of the principle, consider two contradictory statements - “All lemons are yellow” and "Not all lemons are yellow", and suppose (for the sake of argument) that both are simultaneously true. If that is the case, anything can be proven, e.g. "Santa Claus exists", by using the following argument: | + | |
| - | # We know that "All lemons are yellow" as it is defined to be true. | + | |
| - | # Therefore the statement that (“All lemons are yellow" OR "Santa Claus exists”) must also be true, since the first part is true. | + | |
| - | # However, if "Not all lemons are yellow" (and this is also defined to be true), Santa Claus must exist - otherwise statement 2 would be false. It has thus been "proven" that Santa Claus exists. The same could be applied to any assertion, including the statement "Santa Claus does not exist". | + | |
| ==See also== | ==See also== | ||
| - | * [[Consequentia mirabilis]] - Clavius's Law | + | * [[BHK interpretation]] |
| - | * [[Dialetheism]] – belief in the existence of true contradictions | + | * [[Intuitionistic Type Theory]] |
| - | * [[Law of excluded middle]] – every proposition is either true or not true | + | * [[Intermediate logics]] |
| - | * [[Law of noncontradiction]] – no proposition can be both true and not true | + | * [[Linear logic]] |
| - | * [[Paraconsistent logic]] – a family of logics used to address contradictions | + | * [[Constructive proof]] |
| - | * [[Paradox of entailment]] – a seeming paradox derived from the principle of explosion | + | * [[Curry–Howard correspondence]] |
| - | * [[Reductio ad absurdum]] – concluding that a proposition is false because it produces a contradiction | + | * [[Computability logic]] |
| - | * [[Trivialism]] – the belief that all statements of the form "P and not-P" are true | + | * [[Game semantics]] |
| - | + | * [[Smooth infinitesimal analysis]] | |
| {{GFDL}} | {{GFDL}} | ||
Current revision
|
Related e |
|
Featured: |
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 <math>\{\top, \bot\}</math> ("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.
[edit]
See also
- BHK interpretation
- Intuitionistic Type Theory
- Intermediate logics
- Linear logic
- Constructive proof
- Curry–Howard correspondence
- Computability logic
- Game semantics
- Smooth infinitesimal analysis
Unless indicated otherwise, the text in this article is either based on Wikipedia article "Intuitionistic logic" or another language Wikipedia page thereof used under the terms of the GNU Free Documentation License; or on research by Jahsonic and friends. See Art and Popular Culture's copyright notice.
