Practical Foundations of Mathematics
Practical Foundations of Mathematics
复制标题
DOI：
10.5860/choice.37-4551
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
P. Taylor
中科院分区：
文献类型：
--
作者：
P. Taylor
这本书提出了一个非常精心挑选的数学概念和技术的选择，因为它们与数学和计算机科学的基础有关。标题中有些神秘的“实用”一词只是暗示作者不希望“基础”被理解为任何“基础”的意义。其目的是展示和研究逻辑和归纳背后的数学原理，并用于数学和计算机科学的形式化（主要部分）。然而，而不是经典逻辑和集合论，这本书是基于并提供了介绍建设性逻辑和类型理论，后者更接近数学实践比集合论。构造逻辑也讨论了从命题的角度来看，作为类型的证明出现作为一种功能程序，从而弥合逻辑和计算之间的差距。用于提供数学基础的数学结构在本质上主要是分类的，从而允许一般和简洁的公式。而直到最后一章的基本逻辑是直觉主义高阶逻辑（一拉教堂，即基于功能和一种类型的命题）在最后一章nds一个彻底的讨论集理论公理的替代和强有力的论据，有利于类型论的宇宙捕捉的本质公理的替代在一个类型理论的框架。相对于大多数文本的建设性类型理论是非常语法倾向于在目前的书使用类型理论的语言是更加非正式这是按照非正式的方式集理论是用于数学。接下来，我们将更详细地介绍这本书的内容。第一章介绍了一阶推理的基础知识，重点介绍了一个盒子演算，它提供了自然演绎中处理上下文的图形可视化。第二章“类型与归纳法”讨论了和、积、函数类型、命题类型的范式以及以自然数和列表为例的结构归纳艾德技巧。
The book presents a very well-chosen selection of mathematical notions and techniques as they are relevant for the foundations of Mathematics and Computer Science. The somewhat mysterious word “practical” in the title simply insinuates that the author doesn’t want “foundations” to be understood in any “foundational” sense. The aim rather is to exhibit and study the mathematical principles behind logic and induction as needed and used for the formalisation of (the main parts of) Mathematics and Computer Science. However, instead of classical logic and set theory, the book is based on and provides an introduction to constructive logic and type theory, the latter being much closer to mathematical practice than set theory. Constructive logic is also discussed from the point of view of propositions-as-types where proofs appear as sort of functional programs thus bridging the gap between logic and computation. The mathematical structures employed for providing a mathematical underpinning are mainly categorical in nature thus allowing for general and concise formulations. Whereas till the last chapter the underlying logic is intuitionistic higher-order logic ( a la Church, i.e. based on functions and a type of propositions) in the nal chapter one nds a thorough discussion of the set-theoretic axiom of Replacement and strong arguments in favour of type-theoretic universes as capturing the essence of the axiom of Replacement in a type theoretic framework. As opposed to most texts on constructive type theory which are very syntactically inclined in the current book the use of type-theoretic language is much more informal which is in accordance with the informal way set theory is used in mathematics. Next, we survey the contents of the book in more detail. The rst chapter introduces the basics of First-Order Reasoning with an emphasis on a box calculus providing a graphical visualisation of the handling of contexts in natural deduction. The second chapter on Types and Induction discusses sum, product and function types, the paradigm of propositions-as-types and the technique of structural induction exempli ed by natural numbers and lists.