Logic-ml September 2015

11 participants
15 discussions

JAIST Logic Seminar Series
by Hajime Ishihara 05 Sep '15

05 Sep '15

皆様ジーゲン大学のDieter Spreen先生の講演のお知らせです。どうぞふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp ----------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/). Date: Thursday 7 May, 2015, 13:30-15:00 Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Dieter Spreen (University of Siegen) Title: Digit Spaces - Topological Foundations Abstract: Digit spaces have been introduced by Ulrich Berger as a framework for extracting programs that deal with continuous data from formal proofs. The essential idea was to represent objects as streams of unary contractions on a complete metric space and to use coinduction on the logical side. In recent joint work on an extension of this approach to hyperspaces like the space of nonempty compact subsets of a digit space, it turned out that compact cannot be represented by such streams in general: instead one has to deal with infinite trees the nodes of which are labeled by contraction similar to the stream case. It was realized, however, that one will obtain a uniform theory, if the contractions, also called digits, are allowed to be multi-ary.

2 2

第33回量子情報技術研究会 (QIT33) のご案内
by Yasuhiro Takahashi 03 Sep '15

03 Sep '15

皆様，（重複して受け取られた場合はご容赦ください） NTT の高橋と申します．第33回量子情報技術研究会 (QIT33) の案内を転送させて頂きます．よろしくお願い致します． ---------------------------------------------------------- 第33回量子情報技術研究会(QIT33) 研究会の内容：　情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．　第33回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2015年11月24日(火)-25日(水) 会場: NTT厚木研究開発センタ講堂　　（〒243-0198 神奈川県厚木市森の里若宮3-1）発表募集分野 (申し込み状況によっては査読の可能性あり) 　量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，　実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．チュートリアル・招待講演者　中村泰信 (東京大学) 　小芦雅斗（東京大学）　西村治道（名古屋大学）定員: 200名程度参加費: 事前振込み一般2,500円，学生1,000円　　　　　（当日会場払いは一般3,500円，学生2,000円）懇親会費: 事前振込み一般3,500円，学生2,000円　　　　　　（当日会場払いは余裕がある限り．一般4,000円，学生2,500円）研究会参加申込要領　参加申込は下記 Web にて受付けます　https://staff.aist.go.jp/s-kawabata/qit/qit33/ 　講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，　電子情報通信学会の Web システムを使用．【口頭講演申込締切】2015年10月9日(金) 【ポスター講演申込締切】2015年10月23日(金) 【予稿原稿提出締切】2015年10月23日(金) 【参加申込締切】2015年10月30日(金) 【問合せ先】　河野泰人 (NTTコミュニケーション科学基礎研究所) 　高橋康博 (NTTコミュニケーション科学基礎研究所) 　森越文明 (NTT物性科学基礎研究所) 　東　浩司 (NTT物性科学基礎研究所) 　Email:[email protected] 主催: 量子情報技術時限研究専門委員会 (委員長: 富田章久(北海道大学)) 共催: 応用物理学会量子エレクトロニクス研究会 ---------------------------------------------------------- -- 高橋康博 (Yasuhiro Takahashi) NTT コミュニケーション科学基礎研究所メディア情報研究部情報基礎理論研究グループ〒243-0198 神奈川県厚木市森の里若宮3-1 Tel: 046-240-3678 Fax: 046-240-4709 Email: takahashi.yasuhiro(a)lab.ntt.co.jp

1 0

「数学の哲学と証明論」ワークショップ、9月10日(木)-11日(金)、慶應義塾大学
by Yuta Takahashi 03 Sep '15

03 Sep '15

慶應義塾大学非常勤講師の高橋優太と申します。ワークショップ「数学の哲学と証明論」のご案内をお送りいたします。ぜひご参加ください。 --------------------------------------------------------------------- We apologize if you receive this message more than once. --------------------------------------------------------------------- カーネギーメロン大学W.Sieg教授をお招きして次のようなワークショップ「Philosophy of Mathematics and Proof Theory」を予定しております。参加自由です。（なお、次回はG-Y Girard教授をお招きして、11月28日-29日に開催する予定です。 Sieg教授は9月18日にも早稲田大学で別テーマの講演をなさいます。 URL:http://www.waseda.jp/wias/event/symposium/sym_150918.html ） ---- "Philosophy of Mathematics and Proof Theory" Workshop 「数学の哲学と証明論」ワークショップ Date: September 10th(Thu)-21th(Fri), 2015 日時: 2015年9月10日(木)-11日(金) Place: Hall (8F), East Building, Mita campus of Keio University. 場所: 慶應大学三田キャンパス東館8階ホール (http://www.keio.ac.jp/en/maps/mita.html ) 講演アブストラクトを始め会議のupdated informationについてはつぎのURLをご覧ください。 http://abelard.flet.keio.ac.jp/seminar/sieg2015.html ---- Tentative Program: 9/10: 13:00-13:10 Opening Remark, Mitsuhiro Okada and Ryota Akiyoshi 13:00-14:00 Kengo Okamoto (Tokyo Metropolitan University) "TBA" 14:00-15:00 Mamoru Kaneko (Waseda University) "Game Theoretic Decidability and Undecidability" (with Tai-Wei Hu) 15:00-15:20 Break 15:20-16:20 Ryota Akiyoshi (Waseda Institute for Advanced Study) "Some results in proof-theory for $\Pi^{1}_{1}$-$CA$" 16:20-17:50 Wilfried Sieg (Carnegie Mellon University) "Dedekind’s structuralism: creating concepts and deriving theorems" 17:50-18:20 Discussion 9/11: 13:30-14:20 Yuta Takahashi (Keio University) "Gentzen's 1935/36 Consistency Proofs as Means of Ascribing Constructive Senses" 14:20-15:00 Mitsuhiro Okada (Keio University) "Husserl's universal arithmatic and his proof theoretical view of formal mathematics" 15:00-15:20 Break 15:20-16:50 Wilfried Sieg (Carnegie Mellon University) "The ways of Hilbert's axiomatics: structural and formal" 16:50-17:20 Concluding Discussion --------------------------------------------------------------------- Organisers: Mitsuhiro Okada (co-chair) Ryota Akiyoshi (co-chair) Yutaro Sugimoto Yuta Takahashi 主催: 三田ロジックセミナー共催: 慶應義塾大学論理と感性のグローバル研究センター問合せ先: Mita Logic Seminar 事務局 logic(a)abelard.flet.keio.ac.jp --------------------------------------------------------------------- ABSTRACTS 9/10: Mamoru Kaneko (Waseda University) "Game Theoretic Decidability and Undecidability" (with Tai-Wei Hu) Abstract: We study the possibility of prediction/decision making in a finite 2--person game with pure strategies, following the Nash-Johansen noncooperative solution theory. We adopt the infinite-regress logic EIR² (a fixed-point extension) of the epistemic logic KD² to capture individual decision making from the viewpoint of logical inference. In the logic EIR², prediction/decision making is described by the belief set Δ_{i}(g) for player i, where g specifies a game. Our results on prediction/decision making differ between solvable and unsolvable games. For the former, we show that player i can decide whether each of his strategies is a final decision or not. For the latter, we obtain undecidability, i.e., he can neither decide some strategy to be a possible decision nor disprove it. Thus, the theory (EIR²;Δ_{i}(g)) is incomplete in the sense of Gödel's incompleteness theorem for an unsolvable game g. This result is related to "self-referential", but its main source is a discord generated by interdependence of payoffs and independent prediction/decision making. Ryota Akiyoshi (Waseda Institute for Advanced Study): "Some results in proof-theory for $\Pi^{1}_{1}$-$CA$" Abstract: In 2000's, Tait asked the question whether we can prove without ordinal notations that all proofs in $\Pi^{1}_{1}$-$CA$ with (Sch\"{u}tte's) $\omega$-rule are transformed into cut-free ones. Inspired by this, the author and Mints formulated an extension of Buchholz' $\Omega$-rule using Takeuti's distinction of explicit/implicit inference and proved the complete cut-elimination theorem for it. An answer to Tait's question is given by combining this with the author's work on "finite notations for infinitary derivations" for this kind of $\Omega$-rule. In the first part of the talk, we will explain the result with Mints. Next, we explain a connection between the $\Omega$-rule and the computability predicate by Tait-Girard. In 2008, Mints suggested that there should be a connection between these two methods because they would have a common aim to solve the difficulty how to deal with the substitution of a set term $T$ into a free second-order variable $X$ in $A(X)$. The author and Terui recently found this connection by formulating the $\Omega$-rule in the framework of the computability. We report and discuss our result. Wilfried Sieg (Carnegie Mellon University) "Dedekind's structuralism: creating concepts and deriving theorems" Abstract: Dedekind's structuralism is a crucial source for the structuralism of mathematical practice with its focus on abstract concepts like groups and fields. It plays an equally central role for the structuralism of philosophical analysis with its focus on particular mathematical objects like natural and real numbers. Tensions between these structuralisms are palpable in Dedekind's work, but are resolved in his essay Was sind und was sollen die Zahlen? In a radical shift, Dedekind extends his mathematical approach to “the” natural numbers. He creates the abstract concept of a simply infinite system, proves the existence of a “model”, insists on the stepwise derivation of theorems, and defines structure-preserving mappings between different systems that fall under the abstract concept. Crucial parts of these considerations were added only to the penultimate manuscript, for example, the very concept of a simply infinite system. The methodological consequences of this radical shift are elucidated by an analysis of Dedekind's metamathematics. Our analysis provides a deeper understanding of the essay and, in addition, illuminates its impact on the evolution of the axiomatic method and of “semantics” before Tarski. This understanding allows us to make connections to contemporary issues in the philosophy of mathematics and science. (This reports on work with Rebecca Morris.) 9/11: Yuta Takahashi (Keio University) "Gentzen's 1935/36 Consistency Proofs as Means of Ascribing Constructive Senses" Abstract: Gentzen's three consistency proofs for number theory have a common aim that originates from Hilbert's Program, namely, the aim to justify the application of classical reasoning to quantified propositions in number theory. In addition to this common aim, Gentzen gave a constructive interpretation to every number-theoretic proposition in his 1935/36 consistency proofs, while Hilbert's Program included no such interpretation. In this talk, we claim that Gentzen's interpretation took a part of his response to an objection posed by Brouwer against the significance of consistency proofs. Specifically, we argue as follows. According to Brouwer, consistency proofs for classical mathematics are of no significance, because its theorems have no sense whether or not its consistency is proved by using the methods of the Hilbert School. In order to respond to this objection, Gentzen aimed at ascribing a constructive sense to each theorem of classical number theory by means of his interpretation. Mitsuhiro Okada (Keio University) "Husserl's universal arithmatic and his proof theoretical view of formal mathematics" Abstract: We discuss Husserl's development of the conception of universal arithmatic,, with the special focus on his Double-Lecture and other manuscripts in 1901. We can see how his work is influenced from former formalists' work and, at the same time, how it is sharply contrasted to those,. such as Hankel's and Hilbert's former work. We discuss Husserl's view of proof-theoretic and computational notion of "manifold (in his own sense), and his term-rewrite theoretic notion of "definiteness" of manifold. We also discuss some significance of the Husserlian proof theoretic view of mathematics as well as some limitation (for which Wittgenstein partly solved much later). Wilfried Sieg (Carnegie Mellon University) "The ways of Hilbert's axiomatics: structural and formal" Abstract: It is a remarkable fact that Hilbert's programmatic papers from the 1920s still shape, almost exclusively, the standard contemporary perspective of his views concerning (the foundations of) mathematics; even his own, quite different work on the foundations of geometry and arithmetic from the late 1890s is often understood from that vantage point. My essay pursues one main goal, namely, to contrast Hilbert's formal axiomatic method from the early 1920s with his existential axiomatic approach from the 1890s, deeply influenced by Dedekind. Such a contrast illuminates the circuitous beginnings of the finitist consistency program and connects the complex emergence of existential axiomatics with transformations in mathematics and philosophy during the 19th century; the sheer complexity and methodological difficulties of the latter development are partially reflected in the well known, but not well understood correspondence between Frege and Hilbert. Taking seriously the goal of formalizing mathematics in an effective logical framework leads also to contemporary tasks, not just historical and systematic insights.

1 0

第33回量子情報技術研究会 (QIT33) のご案内
by Yasuhiro Takahashi 03 Sep '15

03 Sep '15

皆様， NTT の高橋と申します．第33回量子情報技術研究会 (QIT33) の案内を転送させて頂きます．よろしくお願い致します． ---------------------------------------------------------- 第33回量子情報技術研究会(QIT33) 研究会の内容：　情報科学と量子力学を融合させた新しい分野，量子情報科学に関する研究会です．情報を担う物理系の量子力学的側面を積極的に活かした新しい情報処理原理の研究とそこから開かれる新しい学問体系の構築および新しい情報技術パラダイムの創生を目指して，情報科学，物理学，光エレクトロニクスを含む理学，工学，数理科学に携わる研究者間に自由な討論の場を提供し，この研究分野の発展を図ることを目的としています．　第33回研究会を下記のように開催いたします．現在この分野で活躍する研究者は勿論，自分の研究資産が何らかの形で使えそうだと予感している研究者・技術者など，広く関連する分野の研究者・技術者からの発表を募集致します．聴講のみの参加も歓迎致しますので，奮ってお申し込みください．日時: 2015年11月24日(火)-25日(水) 会場: NTT厚木研究開発センタ講堂　　（〒243-0198 神奈川県厚木市森の里若宮3-1）発表募集分野 (申し込み状況によっては査読の可能性あり) 　量子情報，量子計算，量子暗号など広く量子情報技術に関わる理論的研究，　実験的研究，計算機科学的研究，数学的研究，および，その他関連分野．チュートリアル・招待講演者　中村泰信 (東京大学) 　小芦雅斗（東京大学）　西村治道（名古屋大学）定員: 200名程度参加費: 事前振込み一般2,500円，学生1,000円　　　　　（当日会場払いは一般3,500円，学生2,000円）懇親会費: 事前振込み一般3,500円，学生2,000円　　　　　　（当日会場払いは余裕がある限り．一般4,000円，学生2,500円）研究会参加申込要領　参加申込は下記 Web にて受付けます　https://staff.aist.go.jp/s-kawabata/qit/qit33/ 　講演 (口頭，ポスター) の申込，予稿集原稿 PDF の提出は，　電子情報通信学会の Web システムを使用．【口頭講演申込締切】2015年10月9日(金) 【ポスター講演申込締切】2015年10月23日(金) 【予稿原稿提出締切】2015年10月23日(金) 【参加申込締切】2015年10月30日(金) 【問合せ先】　河野泰人 (NTTコミュニケーション科学基礎研究所) 　高橋康博 (NTTコミュニケーション科学基礎研究所) 　森越文明 (NTT物性科学基礎研究所) 　東　浩司 (NTT物性科学基礎研究所) 　Email:[email protected] 主催: 量子情報技術時限研究専門委員会 (委員長: 富田章久(北海道大学)) 共催: 応用物理学会量子エレクトロニクス研究会 ---------------------------------------------------------- -- 高橋康博 (Yasuhiro Takahashi) NTT コミュニケーション科学基礎研究所メディア情報研究部情報基礎理論研究グループ〒243-0198 神奈川県厚木市森の里若宮3-1 Tel: 046-240-3678 Fax: 046-240-4709 Email: takahashi.yasuhiro(a)lab.ntt.co.jp

1 0

ワークショップ「Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics」
by Ryota Akiyoshi 01 Sep '15

01 Sep '15

早稲田大学高等研究所の秋吉と申します。以下の要領でワークショップ「Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics」(WIAS Top Runners’ Lecture Collection of Science) 開催のご案内をさせて頂きます。ご都合よろしければぜひご参加ください。 ------------------------------------------------------------------------------------------------------------------------ ***Please accept our apologies if you receive multiple copies of this email. *** ワークショップご案内：“Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics” We are pleased to invite you to a workshop titled “Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics” (WIAS Top Runners’ Lecture Collection). ワークショップ「Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics」(WIAS Top Runners’ Lecture Collection of Science) 開催のご案内をさせて頂きます。参加自由です。お気軽にご参加ください。 ---- Title: Computations, Proofs, and Intuitions: A Workshop on Philosophy of Mathematics 「計算，証明，直観」：数学の哲学ワークショップ Date: September 18 (Fri.), 2015 Time: 10:00 – 18:00 Place: International Conference Center (Meeting Room 2, 3rd floor), Waseda University. 日時: 2015年9月18日(金) 10:00 – 18:00 会場: 早稲田大学早稲田キャンパス国際会議場 3階第2会議室 *（*https://www.waseda.jp/top/access/waseda-campus#anc_8*）* http://www.waseda.jp/top/assets/uploads/2015/08/waseda-campus-map.pdf * Bldg. 18 on the map. PROGRAM ************* 10:00-10:10 Opening Remarks 10:10-11:10 “Game Theory and "Symbolic" Logic” Speaker: Mamoru Kaneko (Waseda University) 11:10-12:10 “Proof theory of the lambda-calculus” Speaker: Masahiko Sato (Kyoto University) 12:10-14:00 Lunch Break 14:00-15:20 “The *concept* of computation - an axiomatic characterization” Speaker: Wilfried Sieg (Carnegie Mellon University) 15:20-15:40 Break 15:40-16:40 “Kant on mathematical intuition: from an educational point of view” Speaker: Yasuo Deguchi (Kyoto University) 16:40-17:00 Break 17:00-18:00 “Aspects of the notion of computability” Speaker: Makoto Kikuchi (Kobe University) --------------------------------------------------------------------- 世話人: 秋吉亮太（早稲田高等研究所助教）主催: 早稲田高等研究所問合せ先: 秋吉亮太 georg.logic(a)gmail.com --------------------------------------------------------------------- ABSTRACTS ************* [Speaker] Mamoru Kaneko (Waseda University) [Title] Game Theory and "Symbolic" Logic [Abstract] In game theory, a player chooses/adjusts his behavior based on his understanding of the game situation and his decision/prediction criterion. In logic, a (ideal) mathematician calculates/proves a target theorem from his assumptions. An engine for such adjustments and calculations is logical inference. Such behavior is of a highly symbolic nature. However, it has been customary in the fields of mathematics as well as game theory that real targets are actual models but not symbolic expressions (axiomatizations). This attitude should be reversed when we take game theory as a serious study of human behavior/decision-making in social contexts including considerations of experiential sources for individual beliefs. This is very compatible with the basic idea of “symbolic” logic. In this presentation, we discuss various problems related to this interpretation. [Speaker] Masahiko Sato (Kyoto University) [Title] Proof theory of the lambda-calculus [Abstract] We present a new representation of lambda-terms as a subalgebra of a free algebra. As elements of the free algebra, lambda-terms are constructed without employing the abstraction operation, and this construction of lambda-terms enables us to study lambda-terms as natural finitary objects. In this setting, we will develop the lambda-calculus by defining reductions as derivations and study the proof theory of the lambda-calculus. We will develop the theory in the Minlog proof assistant developed by Helmut Schwichtenberg. [Speaker] Wilfried Sieg (Carnegie Mellon University) [Title] The *concept *of computation - an axiomatic characterization [Abstract] Computations are pervasive in contemporary science and life; they are visible everywhere. However, the *concept *of computation emerged in an almost invisible corner of our intellectual life. I will describe the context for the emergence of computability as a crucial notion in mathematics and logic with a normative philosophical component. My analysis of the emergence of this concept provides a novel perspective on *the central methodological issue *that surrounds computations, the “Church-Turing Thesis”. We focus on *calculable functions *on natural numbers and *mechanical operations *on syntactic configurations. The latter analysis leads to boundedness and locality conditions that motivate axioms for *computable dynamical systems*. Models of these axioms are all reducible to Turing machines. Cellular automata and a variety of artificial neural nets can be shown to satisfy them. Finally, I draw connections and point out directions for fascinating work. As to connections, I will emphasize that my novel perspective is rooted in the radical transformation of mathematics of the 19th century; especially, in the new form of structural axiomatics introduced by Dedekind and Hilbert. [Speaker] Yasuo Deguchi (Kyoto University) [Title] Kant on mathematical intuition: from an educational point of view [Abstract] Kantian notion of mathematical intuition has been criticized, notably by Frege, as too psychological or private to be the proper base of mathematics. This talk will challenge such an allegation by paying attentions to its historical backgrounds, especially that of German mathematical education. First, it focuses on Kantian notion of arithmetical intuition, and identifies one of its main resources; ’Segner’s arithmetic'. Since Vaihinger published his influential commentary of the first critique, Kantians of many variants have almost unanimously believed that it was one of his books; i.e., ‘Principle’. But this talk claims that it is his another book; i.e., ‘Lectures’. Segner’s ‘Lecture’ rather than ‘principle’ occupies a significant position in German history of mathematical education: it is a complement to the pedagogical tradition, so called, 'formal cultivation’ that was initiated by Ch. Wolff. In ‘Lectures', Segner employed such intuitive representations of numbers as points and asterisks, to make the rigid formality of mathematical thinking more approachable to the younger audiences. Since Segner’s intuitive examples of numbers and arithmetic operations were intended to be used in the context of classroom education, they should be publicly available for both teachers and students, and therefore visible and even manipulatable. Based on those observations, this talk claims that Kantian notion of mathematical intuition inherited this visibility, manipulability and public nature of Segner’s exemplars, and is not to be interpreted as being psychological or private. [Speaker] Makoto Kikuchi (Kobe University) [Title] Aspects of the notion of computability [Abstract] There are two important subclasses of the set of partial recursive functions. One is the set of primitive recursive functions and the other is the set of general or total recursive functions. The notion of computability had been scrutinized and expanded in 1930's and nowadays it is widely believed that we have succeeded in formulating the notion of computability accurately and adequately by reaching the concept of partial recursive functions. In this talk, we observe the two gaps of the three classes of computable functions and argue that the former expansion from primitive recursive functions to general recursive functions is somewhat mathematical while the latter enlargement from general recursive functions to partial recursive functions is rather philosophical. We discuss also consequences of observations of the discontinuity in the latter transition in the notion of computability.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml September 2015