Formalizing Common Sense in Mathematical Logic

Leibniz hoped to devise a mathematical logic adequate for human affairs. Since the 1950s progress has been made in formalizing limited common sense domains in first order logic for the purposes of artificial intelligence (AI). However, we argue that extensions to the reasoning methods of first order logic are need to reach human-level common sense. These include nonmonotonic reasoning, reasoning with approximately (or partially) defined entities, reification of propositions and individual concepts, reification of contexts. Even these extensions are probably insufficient.

Dogmas and the Changing Images of the Foundations of Mathematics

I'll offer a critical review of several different conceptions of the activity of foundational research, from the time of Gauss to the present. These will be:

(1) the traditional image, guiding Gauss, Dedekind, Frege and others, that views the search for more adequate basic systems as a logical excavation of a priori structures;

(2) the program to find sound formal systems for so-called clasical mathematics that can be proved consistent, associated with the name of Hilbert; and

(3) the historicist alternative, guiding Riemann, Poincaré, Weyl and others, that seeks to perfect available conceptual systems with the aim to avoid conceptual limitations and expand the range of theoretical options.

I shall contend that assumptions about thefoundational enterprise frequently emerge from certain dogmas that are inherited from previous, outdated images. To round the discussion, I mention some traits of an alternative program that investigates the epistemology of mathematical knowledge.

The Furture of Proof

Gödel showed us many things. Among others he showed us the *possibility* of proof (via the Completeness Theorem for First-Order Logic); and then quite soon thereafter he showed us the *impossibility* of proof (via the Incompleteness Theorem for (suitable) Higher-Order Logics). These results are well known and famous, but their impact on the practice of mathematics has perhaps not been very noticeable. To be sure, related recursive unsolvability results have a clear explanatory value in keeping people from searching for algorithms where none can exist. And modern developments in complexity theory show no quick solutions. But again, many commentators agree that there has not been a big shift in main-stream mathematics as a consequence of Gödel's fundamental work. However, the insight into formalization sparked by Gödel's original work is now having major payoffs in mechanized mathematics and proof systems. The lecture will survey some developments, but it will also bring up the questions of what we should now regard as a proof and of how new proof methods develop.