Abstract
The idea that science can be automated is so deeply related to the view that the method of mathematics is the axiomatic method, that confuting the claim that mathematical knowledge can be extended by means of the axiomatic method is almost equivalent to confuting the claim that science can be automated. I argue that the axiomatic view is inadequate as a view of the method of mathematics and that the analytic view is to be preferred. But, if the method of mathematics and natural sciences is the analytic method, then the advancement of knowledge cannot be mechanized, since non-deductive reasoning plays a crucial role in the analytic method, and non-deductive reasoning cannot be fully mechanized.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
On CTM, see Rescorla (2017).
- 2.
For a survey on Gödel’s theorems, see Raatikainen (2018).
- 3.
This approach seems to forget that Hilbert did not seek formalization for the sake of formalization. Formalization was not an end, rather it was a means in Hilbert’s view. His main aim was to give a secure foundation to mathematics through the formalization of a part of it. And this goal cannot be reached because of Gödel’s results. So, it is difficult to overstate the relevance of those results for Hilbert’s view. That some limited portion of mathematics can be formalized or shown to be complete, but it is not possible to formalize the all of mathematics or prove its completeness in general, it is not something that can salvage Hilbert’s perspective “by changing its goals slightly,” rather it is a complete defeat of Hilbert’s view, since it shows the unfeasibility of its main goal. For example, according to Weyl, the relevance of Gödel’s results cannot be overstated, since because of those results the “ultimate foundations and the ultimate meaning of mathematics remain an open problem [...]. The undecisive outcome of Hilbert’s bold enterprise cannot fail to affect the philosophical interpretation” (Weyl 1949, p. 219).
- 4.
The origin of the analytic method may be traced back to the works of the mathematician Hippocrates of Chios and the physician Hippocrates of Cos, and was firstly explicitly formulated by Plato in Meno, Phaedo and the Republic. Here I can only give a sketch of the analytic method. For an extensive presentation of the analytic view, see Cellucci (2013, 2017).
- 5.
- 6.
The claim that in deduction the conclusion is contained in the premises has to be understood as meaning that the conclusion either is literally a part of the premises or implies nothing that is not already implied by the premises. The claim that deduction is non-ampliative has been disputed by some philosophers. For example, Dummett famously objects that, if deductive rules were non-ampliative, then, “as soon as we had acknowledged the truth of the axioms of a mathematical theory, we should thereby know all the theorems. Obviously, this is nonsense” (Dummett 1991, p. 195). On this issue, which cannot be treated here for reason of space, and for a possible rejoinder to Dummett’s objection, see Cellucci (2017, Sect. 12.7), and Sterpetti (2018, Sect. 6).
- 7.
This view is controversial. For a defense of the claim that a logic of discovery has to be deductive, see e.g. Jantzen (2015).
- 8.
On this sort of asymmetry between deductive and non-deductive reasoning with respect to mechanizability, cf. Cellucci (2017, p. 306): “there is no algorithm for discovering hypotheses, and hence for obtaining the solution [of a given mathematical problem] by analysis, while [...] there is an algorithm for enumerating all deductions from given axioms, and hence for obtaining the solution [of that problem] by synthesis.”
- 9.
This view can, at least in part, be traced back to Lakatos (1976), where Lakatos, by relying on the work of Pólya, strongly criticized the occultation of the heuristic steps that are crucial to the development of mathematics.
- 10.
- 11.
I cannot analyse here the discoveries allegedly made by computer programs. This is a topic for future research. Briefly, the main questions one has to address when dealing with this issue are: (1) whether hypotheses are really produced by programs, since often either a set of hypotheses or a set of heuristic strategies to routinely produce hypotheses from given inputs are already present in the so-called background knowledge of programs (see e.g. Marcus 2018); (2) whether programs can only produce results that can be obtained through a merely exploratory search of a well-defined space of possibilities, or they are also able to make innovative discoveries, i.e. discoveries that originate from the formulation of new concepts, i.e. concepts that cannot easily be derived from current ones, and modify the very space of possibilities (see e.g. Wiggins 2006).
- 12.
On whether mathematics is theorem proving or problem solving, see Cellucci (2017, Chap. 20).
- 13.
For a defense of the claim that the axiomatic view is inadequate also because there is no non-circular way of proving that deduction is truth-preserving, see Cellucci (2006).
- 14.
In fact, things are more complicated. When one climbs the hierarchy of sets, the stronger axioms that become available lead to “more intractable instances of undecidable sentences” (Koellner 2011, Sect. 1). For example, at the third infinite level one can formulate Cantor’s Continuum Hypothesis. These instances of independence “are more intractable in that no simple iteration of the hierarchy of types leads to their resolution” (Ibidem). I will not address this issue here.
- 15.
On disagreement in mathematics, see Sterpetti (2018).
- 16.
On this issue, see Sterpetti (2018).
- 17.
For an account of the resolution of Fermat’s Last Theorem inspired by the analytic view, see (Cellucci 2017, Sect. 12.13).
- 18.
This claim might appear disputable to those who claim that ampliative reasoning is actually performed by machines. As already said, for reason of space, I have to leave the analysis of the claim that machines do autonomously perform ampliative reasoning for future work.
References
Alama, J., and J. Korbmacher. 2018. The Lambda Calculus. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/fall2018/entries/lambda-calculus/.
Allen, J.F. 2001. In Silico Veritas. Data-Mining and Automated Discovery: The Truth Is in There. EMBO Reports 2: 542–544.
Anderson, C. 2008. The End of Theory: The Data Deluge Makes the Scientific Method Obsolete. Wired Magazine, 23 June.
Bacon, F. 1961–1986. Works. Stuttgart Bad Cannstatt: Frommann Holzboog.
Baker, A. 2016. Non-Deductive Methods in Mathematics. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/win2016/entries/mathematics-nondeductive/.
Bell, J., and G. Hellman. 2006. Pluralism and the Foundations of Mathematics. In: Scientific Pluralism, ed. S.H. Kellert, H.E. Longino, and C.K. Waters, 64–79. Minneapolis: University of Minnesota Press.
Boolos, G. 1990. On “Seeing” the Truth of the Gödel Sentence. Behavioral and Brain Sciences 13: 655–656.
———. 1995. Introductory Note to *1951. In: Kurt Gödel. Collected Works. Volume III, ed. S. Feferman et al., 290–304. Oxford: Oxford University Press.
Byers, W. 2007. How Mathematicians Think. Princeton: Princeton University Press.
Calude, C.S., and D. Thompson. 2016. Incompleteness, Undecidability and Automated Proofs. In: Computer Algebra in Scientific Computing. CASC 2016, ed. V. Gerdt et al., 134–155. Cham: Springer.
Cellucci, C. 2006. The Question Hume Didn’t Ask: Why Should We Accept Deductive Inferences? In: Demonstrative and Non-Demonstrative Reasoning, ed. C. Cellucci and P. Pecere, 207–235. Cassino: Edizioni dell’Università degli Studi di Cassino.
———. 2008. Why Proof? What is a Proof? In: Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, ed. R. Lupacchini and G. Corsi, 1–27. Berlin: Springer.
———. 2011. Si può meccanizzare l’induzione? In: Vittorio Somenzi. Antologia e Testimonianze 1918-2003, B. Continenza et al. (a cura di), 362–364. Mantova: Fondazione Banca Agricola Mantovana.
———. 2013. Rethinking Logic. Dordrecht: Springer.
———. 2017. Rethinking Knowledge. Dordrecht: Springer.
Colton, S. 2002. Automated Theory Formation in Pure Mathematics. London: Springer.
Curry, H.B. 1934. Functionality in Combinatory Logic. Proceedings of the National Academy of Science 20: 584–590.
Davis, M. 1990. Is Mathematical Insight Algorithmic? Behavioral and Brain Sciences 13: 659–660.
———. 1995. Introductory Note to *193? In: Kurt Gödel. Collected Works. Volume III, ed. S. Feferman et al., 156–163. Oxford: Oxford University Press.
Dummett, M. 1991. The Logical Basis of Metaphysics. Cambridge, MA: Harvard University Press.
Dybjer, P., and E. Palmgren. 2016. Intuitionistic Type Theory. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/win2016/entries/type-theory-intuitionistic/.
Feferman, S. 1998. In the Light of Logic. Oxford: Oxford University Press.
Gigerenzer, G. 1990. Strong AI and the Problem of “Second-Order” Algorithms. Behavioral and Brain Sciences 13: 663–664.
Glymour, C. 1991. The Hierarchies of Knowledge and the Mathematics of Discovery. Minds and Machines 1: 75–95.
Gödel, K. *193?. Undecidable Diophantine Propositions. In: Kurt Gödel. Collected Works. Volume III (1995), ed. S. Feferman et al., 164–175. Oxford: Oxford University Press.
———. 1951. Some Basic Theorems on the Foundations of Mathematics and Their Implications. In: Kurt Gödel. Collected Works. Volume III (1995), ed. S. Feferman et al., 304–323. Oxford: Oxford University Press.
———. *1961/?. The Modern Development of the Foundations of Mathematics in the Light of Philosophy. In: Kurt Gödel. Collected Works. Volume III (1995), ed. S. Feferman et al., 374–387. Oxford: Oxford University Press.
———. 1964. What Is Cantor’s Continuum Problem? In: Kurt Gödel. Collected Works. Volume II (1990), ed. S. Feferman et al., 254–270. Oxford: Oxford University Press.
Goodman, N. 19834. Fact, Fiction, and Forecast. Cambridge, MA: Harvard University Press.
Hamming, R.W. 1980. The Unreasonable Effectiveness of Mathematics. The American Mathematical Monthly 87: 81–90.
Hayes, P.J. 1973. Computation and Deduction. In: Proceedings of the 2nd Mathematical Foundations of Computer Science Symposium, 105–118. Prague: Czechoslovak Academy of Sciences.
Hilbert, D. 1970. Axiomatic Thinking. Philosophia Mathematica, ser. 1, 7: 1–12, 1st ed., 1918.
Hintikka, J., and U. Remes. 1974. The Method of Analysis. Dordrecht: Reidel.
Horsten, L. 2015. Philosophy of Mathematics. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. http://plato.stanford.edu/archives/spr2015/entries/philosophy-mathematics/.
Horsten, L., and P. Welch. 2016. Introduction. In: Gödel’s Disjunction, ed. L. Horsten and P. Welch, 1–l5. Oxford: Oxford University Press.
Howard, W.A. 1980. The Formulae-as-Types Notion of Construction. In: To H.B. Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism, ed. J.R. Hindley and J.P. Seldin, 479–490. New York: Academic Press.
Jantzen, B.C. 2015. Discovery Without a ‘Logic’ Would Be a Miracle. Synthese. https://doi.org/10.1007/s11229-015-0926-7.
Kant, I. 1992. Lectures on Logic. Cambridge: Cambridge University Press.
King, R.D., et al. 2009. The Automation of Science. Science 324: 85–89.
Koellner, P. 2011. Independence and Large Cardinals. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/sum2011/entries/independence-large-cardinals/.
———. 2014. Large Cardinals and Determinacy. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/spr2014/entries/large-cardinals-determinacy/.
———. 2016. Gödel’s Disjunction. In: Gödel’s Disjunction, ed. L. Horsten and P. Welch, 148–188. Oxford: Oxford University Press.
Kowalski, R.A. 1979. Algorithm = Logic + Control. Communications of the ACM 22: 424–436.
Kripke, S.A. 2013. The Church-Turing ‘Thesis’ as a Special Corollary of Gödel’s Completeness Theorem. In: Computability, ed. B.J. Copeland, C.J. Posy, and O. Shagrir, 77–104. Cambridge, MA: MIT Press.
Lakatos, I. 1976. Proofs and Refutations. Cambridge: Cambridge University Press.
———. 1978. Philosophical Papers. In 2 Vol. Cambridge: Cambridge University Press.
Laplace, P.S. 1951. A Philosophical Essay on Probabilities, 1st French edition, 1814. New York: Dover Publications
Laudan, L. 1981. A Confutation of Convergent Realism. Philosophy of Science 48: 19–49.
Leach-Krouse, G. 2016. Provability, Mechanism, and the Diagonal Problem. In: Gödel’s Disjunction, ed. L. Horsten and P. Welch, 211–242. Oxford: Oxford University Press.
Longo, G. 2003. Proofs and Programs. Synthese 134: 85–117.
———. 2011. Reflections on Concrete Incompleteness. Philosophia Mathematica 19: 255–280.
Lucas, J.R. 1961. Minds, Machines, and Gödel. Philosophy 36: 112–127.
Maddy, P. 1988. Believing the Axioms I. The Journal of Symbolic Logic 53: 481–511.
Mäenpää, P. 1997. From Backward Reduction to Configurational Analysis. In Analysis and Synthesis in Mathematics: History and Philosophy, ed. M. Otte and M. Panza, 201–226. Dordrecht: Springer.
Marcus, G. 2018. Innateness, AlphaZero, and Artificial Intelligence. arXiv:1801.05667v1.
Matiyasevič, Y. 2003. Enumerable Sets Are Diophantine. In: Mathematical Logic in the 20th Century, ed. G.E. Sacks, 269–273. Singapore: Singapore University Press.
Mazzocchi, F. 2015. Could Big Data Be the End of Theory in Science? A Few Remarks on the Epistemology of Data-Driven Science. EMBO Reports 16: 1250–1255.
Muggleton, S., and L. De Raedt. 1994. Inductive Logic Programming. Theory and Methods. Journal of Logic Programming 19–20: 629–679.
Newell, A., J.C. Shaw, and H.A. Simon. 1957. Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristic. In: Proceedings of the 1957 Western Joint Computer Conference, 218–230. New York: ACM.
Penrose, R. 1989. The Emperor’s New Mind. Oxford: Oxford University Press.
Pólya, G. 1941. Heuristic Reasoning and the Theory of Probability. The American Mathematical Monthly 48: 450–465.
———. 1954. Mathematics and Plausible Reasoning. Princeton: Princeton University Press.
Popper, K.R. 2005. The Logic of Scientific Discovery. London: Routledge.
Portoraro, F. 2019. Automated Reasoning. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/spr2019/entries/reasoning-automated/.
Prawitz, D. 2008. Proofs Verifying Programs and Programs Producing Proofs: A Conceptual Analysis. In: Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, ed. R. Lupacchini and G. Corsi, 81–94. Berlin: Springer.
———. 2014. The Status of Mathematical Knowledge. In: From a Heuristic Point of View. Essays in Honour of Carlo Cellucci, ed. E. Ippoliti and C. Cozzo, 73–90. Newcastle Upon Tyne: Cambridge Scholars Publishing.
Raatikainen, P. 2005. On the Philosophical Relevance of Gödel’s Incompleteness Theorems. Revue internationale de philosophie 4: 513–534.
———. 2018. Gödel’s Incompleteness Theorems. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/.
Rathjen, M., and W. Sieg. 2018. Proof Theory. In: The Stanford Encyclopedia of Philosophy. ed. E.N. Zalta. https://plato.stanford.edu/archives/fall2018/entries/proof-theory/.
Rescorla, M. 2017. The Computational Theory of Mind. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/spr2017/entries/computational-mind/.
Rodin, A. 2014. Axiomatic Method and Category Theory. Berlin: Springer.
Schickore, J. 2014. Scientific Discovery. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. http://plato.stanford.edu/archives/spr2014/entries/scientific-discovery/.
Shapiro, S. 2016. Idealization, Mechanism, and Knowability. In: Gödel’s Disjunction, ed. L. Horsten and P. Welch, 189–207. Oxford: Oxford University Press.
Sørensen, M.H., and P. Urzyczyn. 2006. Lectures on the Curry-Howard Isomorphism. Amsterdam: Elsevier.
Sparkes, A., et al. 2010. Towards Robot Scientists for Autonomous Scientific Discovery. Automated Experimentation 2: 1. https://doi.org/10.1186/1759-4499-2-1.
Sterpetti, F. 2018. Mathematical Knowledge and Naturalism. Philosophia. https://doi.org/10.1007/s11406-018-9953-1.
Sterpetti, F., and M. Bertolaso. 2018. The Pursuit of Knowledge and the Problem of the Unconceived Alternatives. Topoi. An International Review of Philosophy. https://doi.org/10.1007/s11245-018-9551-7.
von Plato, J. 2018. The Development of Proof Theory. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/win2018/entries/proof-theory-development/.
Wadler, P. 2015. Propositions as Types. Communications of the ACM 58: 75–84.
Weyl, H. 1949. Philosophy of Mathematics and Natural Science. Princeton: Princeton University Press.
Wiggins, G.A. 2006. Searching for Computational Creativity. New Generation Computing 24: 209–222.
Williamson, T. 2016. Absolute Provability and Safe Knowledge of Axioms. In: Gödel’s Disjunction, ed. L. Horsten and P. Welch, 243–253. Oxford: Oxford University Press.
Wos, L., F. Pereira, R. Hong, et al. 1985. An Overview of Automated Reasoning and Related Fields. Journal of Automated Reasoning 1: 5–48.
Zach, R. 2016. Hilbert’s Program. In: The Stanford Encyclopedia of Philosophy, ed. E.N. Zalta. https://plato.stanford.edu/archives/spr2016/entries/hilbert-program/.
Acknowledgements
I wish to thank Carlo Cellucci for careful reading and commenting on an earlier draft of this chapter.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Sterpetti, F. (2020). Mathematical Proofs and Scientific Discovery. In: Bertolaso, M., Sterpetti, F. (eds) A Critical Reflection on Automated Science. Human Perspectives in Health Sciences and Technology, vol 1. Springer, Cham. https://doi.org/10.1007/978-3-030-25001-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-25001-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-25000-3
Online ISBN: 978-3-030-25001-0
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)