Abstract
During the past century, a majo debate in the philosophy of mathematics has centered on the question of how to regard noneffective or nonconstructive proofs in mathematics. Is it legitimate to claim to have proven the existence of a number with some property without actually being able, even in pöontplo, to produce one? Is it legitimate to claim to have proven the existence of a function without providing any way to calculate it? L. E. J. Brouwer is perhaps the best known early proponent of an extreme constructivist point of view. He rejected much of early twentieth century mathematics on the grounds that it did not provide acceptable existence proofs. He held that a proof of p ⋁ q must consist of either a proof of p or one of q and that a proof of ∃xP(x) must contain a construction of a witness c and a proof that P(c) is true. At the heart of most nonconstructive proofs lies the law of the excluded middle: For every sentence A, A ⋁ ⌝A is true. Based on this law of classical logic one can prove that ∃xP(x) by showing that its negation leads to a contradiction without providing any hint as to how to find an x Satisfying P. Similarly, one can prove ⌝ (⌝p ⋁ q by proving ⌝(⌝p ⋀ ⌝q) without knowing which of p and q is true.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media New York
About this chapter
Cite this chapter
Nerode, A., Shore, R.A. (1997). Intuitionistic Logic. In: Logic for Applications. Graduate Texts in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-0649-1_6
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0649-1_6
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-6855-0
Online ISBN: 978-1-4612-0649-1
eBook Packages: Springer Book Archive