Book contents
- Frontmatter
- Contents
- Preface
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Function Types
- Part IV Finite Data Types
- Part V Infinite Data Types
- Part VI Dynamic Types
- Part VII Variable Types
- Part VIII Subtyping
- Part IX Classes and Methods
- Part X Exceptions and Continuations
- Part XI Types and Propositions
- 30 Constructive Logic
- 31 Classical Logic
- Part XII Symbols
- Part XIII State
- Part XIV Laziness
- Part XV Parallelism
- Part XVI Concurrency
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendix
- Bibliography
- Index
30 - Constructive Logic
from Part XI - Types and Propositions
Published online by Cambridge University Press: 05 February 2013
- Frontmatter
- Contents
- Preface
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Function Types
- Part IV Finite Data Types
- Part V Infinite Data Types
- Part VI Dynamic Types
- Part VII Variable Types
- Part VIII Subtyping
- Part IX Classes and Methods
- Part X Exceptions and Continuations
- Part XI Types and Propositions
- 30 Constructive Logic
- 31 Classical Logic
- Part XII Symbols
- Part XIII State
- Part XIV Laziness
- Part XV Parallelism
- Part XVI Concurrency
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendix
- Bibliography
- Index
Summary
Constructive logic codifies the principles of mathematical reasoning as they are actually practiced. In mathematics a propositionmay be judged to be true exactly when it has a proof and may be judged to be false exactly when it has a refutation. Because there are, and always will be, unsolved problems, we cannot expect in general that a proposition is either true or false, for in most cases we have neither a proof nor a refutation of it. Constructive logic may be described as logic as if people matter, as distinct from classical logic, which may be described as the logic of the mind of god. From a constructive viewpoint the judgment “ϕ true” means that “there is a proof of ϕ.”
What constitutes a proof is a social construct, an agreement among people as to what a valid argument is. The rules of logic codify a set of principles of reasoning that may be used in a valid proof. The valid forms of proof are determined by the outermost structure of the proposition whose truth is asserted. For example, a proof of a conjunction consists of a proof of each of its conjuncts, and a proof of an implication consists of a transformation of a proof of its antecedent to a proof of its consequent. When spelled out in full, the forms of proof are seen to correspond exactly to the forms of expression of a programming language.
- Type
- Chapter
- Information
- Practical Foundations for Programming Languages , pp. 241 - 248Publisher: Cambridge University PressPrint publication year: 2012