Decision Problems
The problem of whether a given equation holds in every Heyting algebra was shown to be decidable by S. Kripke in 1965. The precise computational complexity of the problem was established by R. Statman in 1979, who showed it was PSPACE-complete and hence at least as hard as deciding equations of Boolean algebra (shown NP-complete in 1971 by S. Cook) and conjectured to be considerably harder. The elementary or first-order theory of Heyting algebras is undecidable. It remains open whether the universal Horn theory of Heyting algebras, or word problem, is decidable. Apropos of the word problem it is known that Heyting algebras are not locally finite (no Heyting algebra generated by a finite nonempty set is finite), in contrast to Boolean algebras which are locally finite and whose word problem is decidable. It is unknown whether free complete Heyting algebras exist except in the case of a single generator where the free Heyting algebra on one generator is trivially completable by adjoining a new top.
Read more about this topic: Heyting Algebra
Famous quotes containing the words decision and/or problems:
“How could a man be satisfied with a decision between such alternatives and under such circumstances? No more than he can be satisfied with his hat, which he’s chosen from among such shapes as the resources of the age offer him, wearing it at best with a resignation which is chiefly supported by comparison.”
—George Eliot [Mary Ann (or Marian)
“Our young people are diseased with the theological problems of original sin, origin of evil, predestination, and the like. These never presented a practical difficulty to any man,—never darkened across any man’s road, who did not go out of his way to seek them. These are the soul’s mumps, and measles, and whooping- coughs, and those who have not caught them cannot describe their health or prescribe a cure. A simple mind will not know these enemies.”
—Ralph Waldo Emerson (1803–1882)