Proof Theory| Proof Theory |
In General
* Methods of proof: By contradiction,
by construction, by induction, by exhaustion; Disproof by counterexample.
* Constructive vs contradiction:
(Jan Brouwer) If numbers and other mathematical objects do not exist in a Platonic
realm–if they are constructed–then the only acceptable existence proofs
must be recipes for constructing them; 1960s (Errett A Bishop), Most of classical
mathematical analysis can be proved constructively–but one has to abandon the
idea of an infinite set.
* Checking proofs: Computer-based proofs
are very difficult/tedious to check; Even in traditional proofs, reviewers rarely check
every step, instead focusing mostly on the major points, and relying also on the author's
track record; In the end, they either believe the proof or not (according to mathematics
historian Akihiro Kanamori "It's like osmosis; More and more people say it's a proof
and you believe them"); > s.a. computation.
> Online resources:
see Wikipedia page.
References
> s.a. conjectures; Theorems.
@ Intros: Lakatos 63 [classic on mathematical discovery and methodology,
Worrall & Zahar ed-15];
Solow 82;
Pohlers 89,
08;
Hayes AS(07).
@ Textbooks, II:
Penner 99 [and combinatorics];
Beck & Geoghegan 10;
Gerstein 12;
Cunningham 13 [logical introduction];
Oliveira & Stewart 15;
Meier & Smith 17 [and doing mathematics];
Velleman 19.
@ Other general references: Takeuti 75;
Schütte 77 [not standard framework];
Simmons 00 [III, and computation];
Toelstra & Schwichtenberg 00 [III];
Hanna et al ed-10;
Stillwell 10.
@ Related topics:
Maclane Syn(97) [physicists and mathematics];
Hughes AM(06) [combinatorics as opposed to syntax].
@ Proof by computer: Horgan SA(93)oct;
MacKenzie 01;
Simpson LMP(04) [overview];
Witzel et al a2012
[Python-based interactive theorem-proving assistant];
> s.a. computation.
@ Quantum proofs: Aaronson & Kuperberg qp/06 [vs classical proofs].
Physics-Related and Other Topics
> see philosophy of science [explanations].
@ References: Cohen JSP(09) [example of failure of common opinions and intuitive arguments];
Bolotin APR(16)-a1509 [examples of non-constructive proofs in quantum theory].
main page
– abbreviations
– journals – comments
– other sites – acknowledgements
send feedback and suggestions to bombelli at olemiss.edu – modified 9 feb 2021