The Sources of Certainty in Computation and Formal Systems

TL;DR

This paper explores how formal systems, as concrete artifacts, provide a high level of certainty in mathematics and rational discourse, drawing connections from Descartes and Hilbert to modern logic and computer science.

Contribution

It offers a detailed explanation of formal systems as artifacts and analyzes their role in achieving certainty, linking historical philosophical methods to contemporary formal logic.

Findings

Formal systems provide a high level of certainty in mathematics.

Mathematical logic and computer science deepen understanding of formal systems.

Formal systems serve as artifacts that underpin rigorous rational analysis.

Abstract

In his Discourse on the Method of Rightly Conducting the Reason, and Seeking Truth in the Sciences, Rene Descartes sought ``clear and certain knowledge of all that is useful in life.'' Almost three centuries later, in ``The foundations of mathematics,'' David Hilbert tried to ``recast mathematical definitions and inferences in such a way that they are unshakable.'' Hilbert's program relied explicitly on formal systems (equivalently, computational systems) to provide certainty in mathematics. The concepts of computation and formal system were not defined in his time, but Descartes' method may be understood as seeking certainty in essentially the same way. In this article, I explain formal systems as concrete artifacts, and investigate the way in which they provide a high level of certainty---arguably the highest level achievable by rational discourse. The rich understanding of formal systems achieved by mathematical logic and computer science in this century illuminates the nature of programs, such as Descartes' and Hilbert's, that seek certainty through rigorous analysis.