The Nature of Mathematical Proof

Cover......Page 1
Editorial board......Page 2
Preface......Page 3
Introduction......Page 7
Mechanized and non-mechanized proofs; formal and rigorous proofs......Page 9
Cultures of proving......Page 11
Conflicts over ‘proof’......Page 13
Disciplines and applications......Page 16
References......Page 18
Additional reference......Page 22
The nature of mathematical proof......Page 23
Computation versus intuition......Page 25
Computer science proofs......Page 26
Logic......Page 27
Ontology......Page 30
Computability......Page 32
Computer mathematics......Page 33
State of the art: systems......Page 36
What is needed?......Page 38
Romantic versus cool mathematics......Page 42
References......Page 43
Introduction......Page 49
Lakatoss discussion of Eulers Theorem......Page 50
Cauchys ‘proof’ of Eulers Theorem......Page 51
Schematic proofs......Page 52
Implementation of the constructive omega-rule......Page 53
The relative difficulty of proofs......Page 54
Schematic proofs as a cognitive model......Page 56
Comparison to type theory......Page 57
Rigorous proof as Hilbertian proof highlights......Page 58
References......Page 59
What can and do we prove about programs?......Page 65
References......Page 66
Panelist position statement: reasoning about the design of programs......Page 67
References......Page 68
Panelist position statement: logic and models in computer science......Page 69
References......Page 71
Highly complex proofs and implications of such proofs......Page 73
Discussion......Page 76
Introduction......Page 79
Questions concerning the predicate calculus......Page 82
Consistency questions......Page 85
Set theory, the ultimate frontier......Page 87
The ultimate pessimism deriving from Skolems views......Page 89
References......Page 90
Proofs of novel complexity......Page 91
Idealized proofs......Page 92
Incompleteness......Page 93
Unprovability theory......Page 94
The fundamental theorems......Page 96
Complex methods in arithmetic......Page 98
Isabelle......Page 99
Texts on unwinding......Page 100
Examples......Page 101
Girard unwinding......Page 102
Kohlenbachs work......Page 104
Closing remarks......Page 105
References......Page 106
The justification of mathematical statements......Page 109
Appendix A......Page 116
References......Page 117
Introduction......Page 121
What is constructive mathematics?......Page 122
What significance do the differences have?......Page 123
Computer-assisted mathematics......Page 127
References......Page 129
ReferencesBillinge 2003H.BillingeDid Bishop have a philosophy of mathematics?Phil. Math.112003176194Bishop 1967E.BishopFoundations of constructive analysis1967McGraw-HillNew YorkBishop and Bridges 1985E.BishopD.BridgesConstructive analysisGrundlehren d.........Page 130
Abstracts of additional presentations made at the Royal Society Discussion Meeting ‘The nature of mathematical proof’......Page 133
Contents [Back cover]......Page 134