intuitionistic logic

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 can be obtained from standard natural deduction treatments of the propositional calculus by dropping this rule, provided there is added a rule that from a contradiction anything follows). It should be noticed that intuitionism does not assert the negation of p ∨ ¬ p . On the contrary, its double negation, ¬¬(p ∨ ¬ p ), is itself a theorem of intuitionistic logic. A further important property is that from ¬(∀x )F x it cannot be shown that (∃x )¬F x . This accords with the constructivist instincts behind intuitionism, since the premise gives us no way of constructing an instance of a thing that is not F. Gödel showed that intuitionistic logic can be mapped into the modal logic S4 by various translations of which this is an example. Here v is a propositional variable; A, B are any well-formed formulae of the intuitionistic logic, and Tr(α) is the translation of any formula into S4:
Tr(v )= ⎕v
Tr(A ∨ B) = TrA ∨ TrB
Tr(A & B) = TrA & TrB
Tr(A → B) = TrA → TrB
Tr ¬A = ¬⋄TrA.
This suggests that Heyting was guided by the thought that making a statement is equivalent to stating that the statement is provable or constructible. Denying a statement would be claiming that it is not possible that it should be constructed, or that a contradiction can be derived from the claim that it has been constructed. However, although these equivalences may help classical logicians to understand intuitionism, philosophically intuitionists would not accept that the classical modal logic is fundamental, or that such an explanation in classical terms is appropriate. An interesting property of intuitionistic logic is that no finite truth-tables can be given for the connectives.

Philosophy dictionary. . 2011.

Look at other dictionaries:

  • 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 well formed statements are assumed to be either true or… …   Wikipedia

  • 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

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.