Book contents
- Frontmatter
- Contents
- Foreword
- Preface
- Acknowledgements
- Greek alphabet
- 1 Untyped lambda calculus
- 2 Simply typed lambda calculus
- 3 Second order typed lambda calculus
- 4 Types dependent on types
- 5 Types dependent on terms
- 6 The Calculus of Constructions
- 7 The encoding of logical notions in λC
- 8 Definitions
- 9 Extension of λC with definitions
- 10 Rules and properties of λD
- 11 Flag-style natural deduction in λD
- 12 Mathematics in λD: a first attempt
- 13 Sets and subsets
- 14 Numbers and arithmetic in λD
- 15 An elaborated example
- 16 Further perspectives
- Appendix A Logic in λD
- Appendix B Arithmetical axioms, definitions and lemmas
- Appendix C Two complete example proofs in λD
- Appendix D Derivation rules for λD
- References
- Index of names
- Index of definitions
- Index of symbols
- Index of subjects
12 - Mathematics in λD: a first attempt
Published online by Cambridge University Press: 05 November 2014
- Frontmatter
- Contents
- Foreword
- Preface
- Acknowledgements
- Greek alphabet
- 1 Untyped lambda calculus
- 2 Simply typed lambda calculus
- 3 Second order typed lambda calculus
- 4 Types dependent on types
- 5 Types dependent on terms
- 6 The Calculus of Constructions
- 7 The encoding of logical notions in λC
- 8 Definitions
- 9 Extension of λC with definitions
- 10 Rules and properties of λD
- 11 Flag-style natural deduction in λD
- 12 Mathematics in λD: a first attempt
- 13 Sets and subsets
- 14 Numbers and arithmetic in λD
- 15 An elaborated example
- 16 Further perspectives
- Appendix A Logic in λD
- Appendix B Arithmetical axioms, definitions and lemmas
- Appendix C Two complete example proofs in λD
- Appendix D Derivation rules for λD
- References
- Index of names
- Index of definitions
- Index of symbols
- Index of subjects
Summary
An example to start with
Logic, a fundamental part of many sciences, can be fruitfully expressed and used in an appropriate type-theory-with-definitions such as λD. We have demonstrated this extensively in Chapter 11. Our conclusion is that a flag-style approach, which is still fully formal, is very similar to the common informal style of deduction which is standard for reasoning in both logic and mathematics. The type theory λD can be fruitfully exploited for expressing the logical system of natural deduction in a feasible and practical manner.
In the present chapter, we turn to mathematics. The deductive framework of logic is essential for doing mathematics, since it embodies the principles of reasoning, but mathematics itself is much more than logic (or reasoning) alone.
In order to explore these matters, we start with some illustrative examples, showing the possibilities and the problems connected with doing mathematics in type theory. Our purpose is to investigate whether (or rather: to show how) λD ‘works’ in mathematical practice.
It will turn out that a formal translation of a mathematical text into the λD-format may demand more effort than expected. This is due, of course, to the very precise nature of the ‘formal language’ λD, requiring all aspects to be spelled out, sometimes even to an annoying degree of detail; although the flag style alleviates the burden to some extent.
- Type
- Chapter
- Information
- Type Theory and Formal ProofAn Introduction, pp. 257 - 278Publisher: Cambridge University PressPrint publication year: 2014