Does Science Progress Towards Ever Higher Solvability Through Feedbacks Between Insights and Routines?


axiomatic formalized theory
insight (intuition)
routine procedure



The affirmative answer to the title question is justified in two ways: logical and empirical. (1) The logical justification is due to Gödel’s discovery (1931) that in any axiomatic formalized theory, having at least the expressive power of PA (Peano Arithmetic), at any stage of development there must appear unsolvable problems. However, some of them become solvable in a further development of the theory in question, owing to subsequent investigations. These lead to new concepts, expressed with additional axioms or rules. Owing to the so-amplified axiomatic basis, new routine procedures like algorithms, can be reached. Those, in turn, help to gain new insights which lead to still more powerful axioms, and consequently again to ampler algorithmic resources. Thus scientific progress proceeds to an ever higher scope of solvability. (2) The existence of such feedback cycles –in a formal way rendered with Turing’s systems of logic based on ordinal (1939) – gets empirically supported by the history of mathematics and other exact sciences. An instructive instance of such a process is found in the history of the number zero. Without that insight due to some ancient Hindu mathematicians there could not arise such an axiomatic theory as PA. It defines the algorithms of arithmetical operations, which in turn help intuitions; those, inturn, give rise to algorithmic routines, not available in any of the previous phases of the process in question. While the logical substantiation of the point of this essay is a well-established result of logico-semantic inquiries, its empiricalclaim, based on historical evidences, remains open for discussion. Hence the author’s intention to address philosophers and historians of science, and to encourage their critical responses.



Ajdukiewicz, K (1934). Sprache und Sinn. Erkenntnis, 4(1), 100–138.

Bancerek, G., et al. (2018). The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. Journal of Automated Reasoning, 61(1–4), 9–32.

Benzmüller, C. E., Brown, C. E. (2007). The Curious Inference of Boolos in Mizar and OMEGA. Studies in Logic, Grammar and Rhetoric, 23, 299–386.

Benzmüller, C., Woltzenlogel Paleo, B. (2013). Gödel’s God on the computer. Retrieved from:

Benzmüller, C. (2015). Gödel’s Ontological Argument Revisited. Findings from a Computer-Supported Analysis. In: R. S. Silvestre, J. Y. Béziau (Eds.), Handbook of the 1st World Congress on Logic and Religion. Joao Pessoa, Brazil.

Benzmüller, C. (2017). Universal Reasoning, Rational Argumentation and Human-Machine Interaction”. arXiv, retrieved from:

Boston, N. (2003). The proof of Fermat’s Last Theorem, retrieved from:

Braselmann, P., Koepke P. (2005). Gödel’s Completeness Theorem. Formalized Mathematics, 13(1), 49–53.

Boolos, G. (1987). A Curious Inference. Journal of Philosophical Logic, 16(1), 1–12.

Buss, S. R. (1994). On Gödel’s Theorems on Lengths of Proofs I: Number of Lines and Speedup for Arithmetic. Journal of Symbolic Logic, 59(3), 737–756.

Church, A. (1936). An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics, 58(2), 345–363.

Fitting, M. (1975). Types, Tableaus, and Gödel’s God. Dordrecht: Kluwer.

Fodor, J. A. (1975). The Language of Thought. Cambridge (Mass.): Harvard University Press.

Frege, G. (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: Nebert.

Frege, G. (1880–1881). Booles rechnende Logik und die Begriffsschrift. In: L. Kreiser (Ed.), Schriften zur Logik. Aus dem Nachlass mit einer Einleitung von Lothar Kreiser (172–226). Berlin: Akademie Verlag.

Frege, G. (1973). Schriften zur Logik Aus dem Nachlass mit einer Einleitung von Lothar Kreiser. Berlin: Akademie Verlag.

Fraenkel, A. A. (1976). Abstract Set Theory. Amsterdam: North Holland.

Gödel, K. (1930). Die Vollständigkeit der Axiome des logischen Funktionenkalküls, 349–360. Monatshefte für Mathematik, 37(1). English translation: The completeness of the axioms of the functional calculus of logic. In: S. Feferman et al. (Eds.), Kurt Gödel Collected Works. Vol I. Publications 1929–1936 (pp. 61–101). Oxford: Oxford University Press.

Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38(1), 173–198.

Gödel, K. (1936). Über die Länge von Beweisen. Ergeb. Math. Kolloquiums, 7, 23–24.

Gödel, K. (1995). Some Basic Theorems on the Foundations of Mathematics and Their Implications. In: S. Feferman (Ed.), Collected Works: Volume III: Unpublished Essays and Lectures of Kurt Gödel (pp. 304–323). Oxford: Oxford University Press.

Grzegorczyk, A. (1974). An Outline of Mathematical Logic. Fundamental Results and Notions Explained with All Details. Warszawa: PWN.

Hilbert, D., Ackermann, W. (1928). Grundzüge der theoretischen Logik. Berlin: Springer.

Hodges, A. (2013). Alan Turing, retrieved from:, W., Kneale, M. (1962). The Development of Logic, Oxford: Clarendon Press.

Laplace, P. S. (1951). A Philosophical Essay on Probabilities. New York: Dover Publications.

Marciszewski, W. (Ed.). (1981). Dictionary of Logic as Applied in the Study of Language. Concepts, Methods, Theories. Hague, Nijhoff.

Marciszewski, W., Murawski, R. (1995). Mechanization of Reasoning in a Historical Perspective. Amsterdam: Rodopi.

Marciszewski, W. (2006). The Gödelian Speed-up and Other Strategies to Address Decidability and Tractability. Studies in Logic, Grammar and Rhetoric, 22, 9–29.

Mares, E. D. (2004). Relevant Logic: A Philosophical Interpretation. Cambridge: Cambridge University Press.

Parsons, C. (2010). Gödel and Philosophical Idealism. Philosophia Mathematica, 18(2), 166–192.

Placek, T. (2013). Mathematical Intuitionism and Intersubjectivity: A Critical Exposition of Arguments for Intuitionism. Berlin: Springer Science & Business Media.

Popper, K. (1959). The Logic of Scientific Discovery. New York, Basic Books.

Rukavicka, J. (2014). Rejection of Laplace’s Demon. The American Mathematical Monthly, 121(6).

Tarski, A., Mostowski, A., Robinson, R. (1968). Undecidable Theories. Amsterdam: North Holland.

Turing, A. (1936). On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1), 230–265.

Turing, A. (1938). Systems of Logic Based on Ordinals. Retrieved from:

Turing, A. (1939). Systems of Logic Based on Ordinals. Proceedings of the London Mathematical Society, s2-24(1), 161–228.

Webb, J. C. (1980). Mechanism, Mentalism, and Metamathematics. Dordrecht, Reidel.

Wiles, A. (1995). Modular Elliptic Curves and Fermat’s Last Theorem. Annals of Mathematics, 141(3), 443–551.

Wittgenstein, L. (1922). Tractatus Logico-Philosophicus. London: Routledge & Kegan Paul.