Akademik

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.