Mathematical Logic: Development and Evolution into Various Sciences

It is well-known that any formal mathematical system can be faithfully encoded within PRA. It is also commonly accepted that any well-established part of mathematics can be presented as a formal system. Thus, it seems that we can bootstrap mathematics, within a computer, simply by implementing PRA in it. However, we will show that this view is too naïve both from computer science point of view and from foundational point of view. We also discuss an alternative approach to this problem by giving an overview of a proof assistant system we are developing.

Goedel's incompleteness theorem stranded Hilbert's attempt to reduce all of classical mathematics to finitary reasonings. But the following question has remained to be investigated: how much of classical mathematics can be reduced to finitary or constructive mathematics? To this end, the program of reverse mathematics was initiated by H. Friedman in the 1970's and extensively developed by S. Simpson in the 80's.

A nonstandard proof method for reverse mathematics was first introduced by the speaker in the mid-90's, and it has been greatly improved and applied to many areas by several people during the past few years. With the method, we can, for instance, show that the fundamental theorem of algebra, which ordinarily follows from a non-constructive argument of compactness, can be already proved without such an argument. In other words, we can claim that a (computable) polynomial has computable solutions without designing a cumbersome algorithm for solving it. In this talk, presenting an overview of our results on reverse mathematics, we especially discuss their relation to methodological instrumentalism originated with Hilbert.

The development of various systems of DEL (dynamic epistemic logic) suggests a possibility of developing logics that can capture effects of various speech acts in social communication. Thus, acts of commanding and promising are modeled as events that change the deontic statuses of alternative courses of action available to agents in dynamified deontic logics. Similarly, acts of asserting and conceding are modeled as events that updates the propositional commitments agents bear in a dynamic logic of propositional commitments. We will review the developments of these logics and present a general recipe for developing logics that can capture effects of various other specific speech acts.

If we could translate `if--then' structures in legal documents in a uniform way into formal language, we would construct a reasoning system or would inspect the soundness of the whole code, implementing them in Prolog, for example. However, unfortunately this is not the case. There appear various kinds of`if--then' structure, including indicative/counterfactual causalities, conceptual subsumption, temporal relation, as well as the distinction of classical and intuitionistic implications. We discuss the variety and the difference of these in terms of Kripke semantics, and then we especially pay attention to the counterfactual conditional. We show that the statements with counterfactuality nullify syllogisms, contraposition, and conditional weakening; we illustrate this with natural language phenomena.

Graphical representations such as maps, charts, and graphs convey meanings in a distinctive way sentential representations do not. a clouds of dots in a scatter plot means a correlation between two variables, a pattern formed by contour lines in a contour map means a valley, and a sequence of circles in a round-robin table means a sequence of wins by a particular team. These meanings, which are justifiably called ``graphical meanings,'' largely account for the functions and ill-functions of graphical representations as communicational and inferential tools. I will show how the graphical meanings can be analyzed logically, as something based on a ``parallel abstraction'' over two logical systems. The key notion is formalized in channel theory (Barwise and Seligman 1997).