This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice (ZFC). This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics?
Author(s): Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm (eds.)
Series: Logic, Epistemology, and the Unity of Science 27
Publisher: Springer
Year: 2012
Language: English
Pages: 415
Tags: Logic; Mathematical Logic and Foundations; Epistemology; Ontology; History of Mathematical Sciences
Front Matter....Pages i-xxvii
Front Matter....Pages 1-1
Kant and Real Numbers....Pages 3-23
Wittgenstein’s Diagonal Argument: A Variation on Cantor and Turing....Pages 25-44
Truth and Proof in Intuitionism....Pages 45-67
Real and Ideal in Constructive Mathematics....Pages 69-85
In the Shadow of Incompleteness: Hilbert and Gentzen....Pages 87-127
Evolution and Logic....Pages 129-138
The “Middle Wittgenstein” and Modern Mathematics....Pages 139-159
Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections....Pages 161-180
Front Matter....Pages 181-181
Type Theory and Homotopy....Pages 183-201
A Computational Interpretation of Forcing in Type Theory....Pages 203-213
Program Testing and the Meaning Explanations of Intuitionistic Type Theory....Pages 215-241
Normativity in Logic....Pages 243-263
Constructivist Versus Structuralist Foundations....Pages 265-279
Machine Translation and Type Theory....Pages 281-311
Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions....Pages 313-349
Coalgebras as Types Determined by Their Elimination Rules....Pages 351-369
Second Order Logic, Set Theory and Foundations of Mathematics....Pages 371-380
Back Matter....Pages 381-385
