## General Information

Date and Time: |
March 9, 2012 9:00–17:00 |

Venue: |
Hirosaka-Bekkan of Ishikawa Prefectural Museum of Art 2-1 Dewa-machi, Kanazawa, Ishikawa 920-0963, Japan |

This workshop is held as part of the JAIST Spring School 2012.

## Program

09:00 – 09:05 | Opening Yasuhiro Awatsuji (MEXT, Deputy Director, Mathematical Innovation Unit) |

09:05 – 10:05 | Bootstrapping Mathematics Masahiko Sato (Kyoto University) 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. |

10:20 – 11:20 | Reverse Mathematics and Nonstandard Methods Kazuyuki Tanaka (Tohoku University) 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. |

11:20 – 13:20 | – Lunch Break – |

13:20 – 14:20 | Logical Dynamics of Speech Acts in Social Communication Tomoyuki Yamada (Hokkaido University) 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. |

14:35 – 15:35 | Equivocal If-Then Structure in Legal Reasoning Satoshi Tojo (JAIST) 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. |

15:50 – 16:50 | An Analysis of Graphical Meanings in Channel Theory Atsushi Shimojima (Doshisha University) 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). |

## Speakers

- Masahiko Sato (Kyoto University)
- Atsushi Shimojima (Doshisha University)
- Kazuyuki Tanaka (Tohoku University)
- Satoshi Tojo (JAIST)
- Tomoyuki Yamada (Hokkaido University)

## Organizing Committee

- Hajime Ishihara (JAIST)
*chair* - Nao Hirokawa (JAIST)
- Mizuhito Ogawa (JAIST)
- Katsuhiko Sano (JAIST)
- Satoshi Tojo (JAIST)

## Sponsors

- Ministry of Education,Culture,Sports,Science & Technology in Japan
- Japan Advanced Institute of Science and Technology (JAIST)

## Supporters

- Mathematical Society of Japan
- Japan Society for Industrial and Applied Mathematics
- Japanese Federation of Statistical Science Associations
- Japan Science and Technology Agency

## Related Workshop

- Workshop on Proof Theory and Computability Theory 2012 (February 20 – 23, 2012)