2019年度年会(於:東京工業大学)

SUMMARY: In the history of mathematics, Islamic science played an important role in reviving Greek mathematics by translating almost all Greek mathematical texts into Arabic. We must note that the Arabic translation activity was finished in the early Abbasid period, and afterwards, Islamic scholars studied Greek mathematics by examining the Arabic versions of Greek mathematical works without reading the Greek original texts. Thus, revealing the process of composing these Arabic versions in the Abbasid period is obviously important for us when we consider the formation of “studying Greek mathematics” tradition among Islamic scholars; however, until now there are not enough studies on how Abbasid scholars translated Greek mathematical texts into Arabic. To make a start of examining their translation technique, I will choose the case of the Arabic version of Apollonius’ Conics. In the period of the seventh Abbasid caliph al-Ma’mūn (786–833), Banū Mūsā brothers, high officials in the court, endeavored to obtain the entire books of the Conics which originally consisted of 8 books. Despite of their enthusiasm, they only got book 1–7, and then they translated 7 books into Arabic. Today, owing to their Arabic translation, we know the contents of book 5–7 whose Greek texts are lost. In this paper, I will compare the Arabic version of some propositions with the Greek original texts, and scrutinize how Banū Mūsā rendered the Greek text into Arabic, and show their aim of compiling the Arabic version.

SUMMARY: Hoare logic is a proof system to deduce some correctness of programs. The correctness of programs is represented by Hoare triples \(\{A\}P\{B\}\), which mean the assertions \(A\) and \(B\) hold respectively before and after execution of the program \(P\).

Separation logic is an extension of the Hoare logic to verify programs operating heap memories. In order to represent quantitative properties of allocated memory blocks, the assertion language is extended by separating conjunctions \(A*B\), which corresponds to multiplicative conjunctions in the linear logic.

In this talk, we give a brief introduction of the Hoare logic and the separation logic, and introduce our recent results on the separation logic, in particular, on the logical systems for assertions in the separation logic with inductively defined predicates.

SUMMARY: Providing capillary action in the equilibrium, Poisson assures that the rise of the surface of water is due to the abrupt variation of density in the neighborhood of the wall and of the surface. Poisson discusses this problem in 1831, in the rivalry to the paper/book of Laplace 1806–7 and Gauss 1831. We show Poisson’s modeling and calcuration.

SUMMARY: Legendre’s integrals are based on the arcs of ellipsoid and the number theory. He criticizes Euler’s integrals. He proposes the function (H) of arc is expressed with H = A’F + B’E + C’\(\Pi \). (F, E and \(\Pi \) are the three elliptic functions, A’,B’ and C’ are arbitraries.) Legendre says, this theorem (\(\Pi \) is expressed moreover with F and E), is very important in the theory of the elliptic functions. [1, chapter 23, a.107, p.134]. We discuss Legendre’s integrals in emphasizing these points.

SUMMARY: We discuss Legendre’s elliptic functions in 1825. Poisson contrives his method of integral beginning with the paper 1802, and up to the last works, he appreciates fully Legendre’s integral method. But for it, Poisson confesses, he couldn’t have succeeded in these sorts of integrals. Legendre shows the guide for application in geometry and in mechanics. Poisson adopts Legendre’s formulae only after five years since the publication of Legendre’s functions and tables in 1825–6ish.

SUMMARY: Modern textbooks of mechanics develop their arguments based on the so-called Hamilton’s principle. It is inferable 19th-century mathematician W. R. Hamilton introduced this formation. But it not true. This paper shows David Hilbert’s lectures in 1922–23 unified Hamilton’s optical and dynamical theories and based on the variational principles. His assistant Nordheim showed mechanical theory based on Hamilton’s principle in 1927 and gave a standard description on this area.

SUMMARY: The diagrams of solid geometry (Books XI-XIII) in Euclid’s Elements are often drawn by orthogonal projection to one of the planes of the figures treated in the proposition. When a straight line necessary in the demonstration is reduced to one point in such drawing, this line is drawn as if it were viewed from a different angle. This happens in the propositions treating octahedron (XIII.14), icosahedron (XIII.16) and dodecahedron (XIII.17). Such mixture of viewpoints in one diagram suggests that there was no standard way of drawing solid figures, and perhaps there was only very vague concept of three dimensional space independent of each solid figures.

SUMMARY: We can find a word “bun jutsu” in Seki Takakazu’s book Byoudai Meichi (Correction of Abnormal Problems). It seems certainly to be related to the side writing system which is a traditional method to describe a polynomial in East Asia. The meaning of this word, however, wasn’t discussed until now. I will introduce a problem including the word “bun jutsu” and consider its meaning and then clarify that Seki broke with tradition modestly.

SUMMARY: The Taisei Sankei, one of the most important works on Mathematics in Edo period, was compiled during the period (1683–1695–1710). This 20 volumes work was not published, instead, copied carefully. Nowadays we have more than twenty manuscripts of the Taisei Sankei conserved at several libraries in Japan. We propose to enumerate them according to H. Komatsu’s article published at the RIMS kôkyûroku (2007) and to number each of manuscripts by the Komatsu number, which H. Komatsu used to enumerate manuscripts in his article. He enumerate only twenty manuscripts but mentioned several more. We propose here to number these not yet numbered manuscript. For example, manuscripts of the Taisei Sankei conserved at Tsu City Library, Mie Prefecture were not mentioned in Komatsu’s paper and hence not yet numbered.

SUMMARY: The solutions presented by Liu Hui in the chapter 9 of “The Nine Chapters on the Mathematical Art” and “The Sea Island Mathematical Manual” used two methods: by area of rectangles and by similarity of triangles. The Yuelu “Shu” also has the same problem as the problem 9 of “Nine Chapters,” so they stated in [1] that “If this problem was solved using the Pythagorian theorem, the people in the late Zhou and the Qin era has already knew the general definition of the theorem”. We have not agreed with them easily, however, the solution using similarity of triangles we suggested in [2] was invalid.

SUMMARY: In this talk, we will present some formulae to give the area of circles in the ancient chinese books of mathematics.

SUMMARY: In general, there is no proof system which is sound and complete for standard second-order semantics. We found that in strictly monadic second-order logic, which admits only monadic predicate constants and predicate variables, usual second-order proof systems are sound and complete for standard semantics.

SUMMARY: We introduce a formal system of reduction paths for parallel reduction. Our motivation behind this work comes from a quantitative analysis of reduction systems based on the two viewpoints, computational cost and computational orbit (paths). For the first perspective we have shown a quantitative form of the Church–Rosser theorem with respect to parallel reduction. Next, for the second point we will show that there exists a common reduct leading to which we have a unique path of parallel reduction. Following the notion of normal paths, a graphical representation of reduction paths is provided. In order to prove the unique path property, path matrices are defined as block matrices of adjacency matrices for counting reduction orbits.

SUMMARY: Cut elimination is one of the important problems in sequent systems and there are several methods to prove the cut elimination theorem. In 1989, Dunn and Meyer succeeded to prove the cut elimination theorem for LK-like system of classical logic by using metavaluation, which is introduced in relevant logic. In this talk, we consider a proof of the cut elimination theorem of the sequent calculus GS4 for modal logic S4 by Dunn and Meyer’s method.

SUMMARY: Let \(\kappa \) be a cardinal number. The category \(\mathbf {CAMA}_{\kappa }\) of \(\kappa \)-additive complete atomic modal algebras is dually equivalent to the category \(\mathbf {MRKF}_{\kappa }\) of \(\kappa \)-downward directed multi-relational Kripke frames, since the category \(\mathbf {NFr}_{\kappa }\) of \(\kappa \)-complete neighborhood frames is dually equivalent to \(\mathbf {CAMA}_{\kappa }\) and is equivalent to \(\mathbf {MRKF}_{\kappa }\). We present another direct proof of this duality for any regular cardinal \(\kappa \).

SUMMARY: The disjunction and existence properties are regarded as characteristic features of constructivity of intuitionistic logic. These properties are proved to be independent in intermediate predicate logics. Thus, there are intermediate predicate logics having disjunction property but lacking existence property. We present a simple axiom schema with which we can construct an intermediate predicate logic having disjunction property but lacking existence property. Using this result, we can give a slightly simple proof that there are uncountably many predicate extensions of intuitionistic logic.

SUMMARY: A propositional modal logic \(L\) is said to have the Craig interpolation property iff for any formulas \(\varphi , \psi \), if \(L \vdash \varphi \to \psi \), then there exists a formula \(\theta \) containing only propositional variables that occur in both \(\varphi \) and \(\psi \) such that \(\varphi \to \theta \) and \(\theta \to \psi \) are provable in \(L\). Two stronger versions of interpolation property are known, namely, the Lyndon interpolation property (LIP) and the uniform interpolation property (UIP). We introduced the notion of the uniform Lyndon interpolation property (ULIP) which is a strengthening of both UIP and LIP. We proved several propositional modal logics including \(\mathbf {K}\), \(\mathbf {KT}\), \(\mathbf {KB}\), \(\mathbf {GL}\) and \(\mathbf {Grz}\) enjoy ULIP.

SUMMARY: In 1976, de Jongh and Sambin independently proved the fixed point theorem for the provability logic \(\mathsf {GL}\). In particular, Sambin’s proof gives an effective procedure for constructing fixed points in \(\mathsf {GL}\) which is known as Sambin’s algorithm. In 2001, Sacchetti introduced the modal logics \(\mathsf {wGL}_{n} = \mathsf {K} + (\Box (\Box ^{n}p \to p) \to \Box p)\) \((n > 1)\) which are weaker than \(\mathsf {GL}\), and proved that the fixed point theorem also holds for these logics. However, his proof gives no effective procedure for constructing fixed points in these logics, and he asked the question of the existence of such a procedure. We solved Sacchetti’s problem affirmatively, that is, we found an effective procedure for constructing fixed points in Sacchetti’s logics.

SUMMARY: Sacchetti introduced the modal logics \({\mathsf {wGL}}_n\) which are fragments of the Gödel–Löb logic \(\mathsf {GL}\). Sacchetti’s logics have remarkably similar properties to \(\mathsf {GL}\), for example, the Craig interpolation property, fixed-point property, having arithmetical interpretations, and so on. Recently Shamkanov proved the Lyndon interpolation property for \(\mathsf {GL}\) using the circular proof system. In this talk, we apply Shamkanov’s argument to the case of \({\mathsf {wGL}}_n\), and prove the Lyndon interpolation property for these logics.

SUMMARY: Quantum logic has been studied with orthomodular lattices. The semantics required for quantum logic can also be provided by possible worlds semantics (OM-models), whose nature is almost equivalent to the notion of orthomodular lattices. However, OM-models are still under development because some important notions of quantum physics are not included. Thus, in this presentation, an evolutionary form of OM-models is introduced and how it is used will be explained.

SUMMARY: The orthomodular lattice of subspaces of \(\mathbb {R}^3\) has two intermediate layers, one is the layer of atoms and the other is the layer of coatoms. Some tautology which is not valid in quantum logic has a counter examples in the class of orthomodular lattices with two intermediate layers. We discuss some properties of orthomodular lattices with two intermediate layers.

SUMMARY: We will give a simple survey for an essence of our division by zero.

We would like to answer for the old and general question:

Can we divide the numbers by zero?

For this question, we would like to give a simple and definite answer as in the talk title. We, of course, have to give a simple meaning of division.

SUMMARY: I define new special functions called Hyper exponential functions with the symbol exph. The main feature of n-order Hyper exponential functions is that n-order derivatives of the functions are the product of any function and the functions. As one of applications, it will be shown that the second-order Hyper exponential functions can be used to describe the solutions of linear homogeneous differential equations of the second order with variable coefficients. Several graphs of the Hyper exponential functions of second-order are shown. It will be shown how to generate the Hyper exponential functions of n-order. Computers are used to generate the Hyper exponential functions. The list of the differential equations that describe the solutions by using the Hyper exponential functions will be given. The Hyper exponential functions are used to represent solutions for the wave equations and for nonlinear differential equations.

SUMMARY: We show that if \(\kappa \) is strongly compact then there is a forcing extension in which \(\kappa \) remains strongly compact and GCH fails at \(\kappa \).

SUMMARY: Using Laver’s technique, Kibedi proved that it is consistent that there exists a maximal saturated linear order in \((\omega ^\omega , <^*)\). Moreover, he extended Laver’s techinique and proved that it is consistent that there exists a maximal saturated linear order in \((\omega ^\omega , <^*)\) and Martin’s Axiom holds. Proper Forcing Axiom implies that there are no maximal saturated linear orders in \((\omega ^\omega , <^*)\), however, by use of Kibedi’s idea, it can be proved that it is consistent that there exists a maximal saturated linear order in \((\omega ^\omega , <^*)\) Martin’s Axiom holds, and any two \(\aleph _1\)-dense sets of reals are order-isomorphic.

SUMMARY: We show that sets of finitely approximated subsets of the reals form sigma-algebras.

SUMMARY: Modal \(\mu \)-calculus, introduced by Kozen, is an extension of modal propositional logic by adding a greatest fixpoint operator \(\mu \) and a least fixpoint operators \(\nu \). In this talk, first, we show the relationship between one-variable \(L_{\mu }\)-formulas and weak alternating tree automata. Next, we introduce a transfinite extension of parity games.

SUMMARY: We introduce a variant of an AND-OR tree in which leaves are connected to internal nodes via communication channels. These communication channels possibly have high probability of interruption. We give a sufficient condition for interruption probability setting to have the following property: There is no optimal algorithm that is depth-first search (provided that it obeys a certain communication protocol). We give a concrete example of such an interruption setting by means of Riemann zeta functions.

SUMMARY: For the pair (r, R) of a reducibility and a randomness notion, we consider the following property: if A is r-reducible to B and A is R-random, then B is R-random. In this case we say these are coherent. Some pairs are coherent but others are not. In particular, Schnorr reducibility is not coherent with computable randomness. Dm-reducibility and tm-reducibility are coherent with n-randomness.

SUMMARY: The notion of probability plays a crucial role in quantum mechanics. It appears as the Born rule. In modern mathematics which describes quantum mechanics, however, probability theory means nothing other than measure theory, and therefore any operational characterization of the notion of probability is still missing in quantum mechanics. In our former works, based on the toolkit of algorithmic randomness, we presented an alternative rule to the Born rule for specifying the property of results of measurements in an operational way. In this talk, we make an application of our framework to quantum teleportation and superdense coding in order to demonstrate how properly our framework works in practical problems in quantum mechanics.