Logic-ml

logic-ml@fos.kuis.kyoto-u.ac.jp

1792 discussions

教員公募（名古屋大学情報科学研究科・准教授）
by Jacques Garrigue 05 Mar '15

05 Mar '15

PPLおよびlogic-mlの皆様、名古屋大学のGarrigueです。名古屋大学の結縁先生のご依頼で、教員公募（名古屋大学情報科学研究科・准教授）をお送りします。 ====================================== （重複してお受け取りの場合はご容赦ください。）名古屋大学の結縁です。メーリングリストをお借りして公募情報をお送りいたします。名古屋大学情報科学研究科情報システム学専攻准教授　１名応募期限　4/28(消印有効) ------------------------------------------- 平成 27 年 2 月 4 日関係各位名古屋大学大学院情報科学研究科研究科長　坂部俊樹教員の公募について（依頼）謹啓　時下ますますご清祥のことお慶び申し上げます．さて，この度当研究科では，下記の要領により，教員を公募いたします．つきましては，貴学（機関）関係者にご周知いただければ幸いです．謹白記 1. 公募対象：准教授 1 名（名古屋大学大学院情報科学研究科情報システム学専攻ソフトウェア論講座） 2. 専門分野：ソフトウェア科学 (プログラムの検証理論，検証技術など) 3. 担当科目：情報科学研究科情報システム学専攻の講義および大学院学生の指導，工学部電気電子・情報工学科の講義および学生の指導，全学教育の講義 4. 応募資格：博士の学位を有する方 5. 任期：なし 6. 着任時期：2015 年 10 月 1 日以降のできるだけ早い時期 7. 提出書類： (1) 履歴書（写真付き） (2) 研究業績リスト（著書，学術論文誌，国際会議などを区分して記述） (3) 主要論文別刷（主要なもの 3 編以内，コピーも可） (4) これまでの研究概要（A4 用紙 2 枚程度） (5) 今後の研究計画および教育についての抱負（A4 用紙 1 枚程度） (6) その他選考に役立つ情報（教育実績，学会および社会活動，獲得した外部資金，受賞，特許，ソフトウェア開発実績など） (7) 応募者の業績について問い合わせることのできる方 2 名の氏名と連絡先 8. 応募期限：2015 年 4 月 28 日（火）(郵送の場合，当日消印有効) 9. 書類提出先および問い合わせ先：〒 464-8603 名古屋市千種区不老町 C3-1（631）名古屋大学大学院情報科学研究科平成 26 年度情報システム学専攻長　高田広章 TEL: 052-789-5887 Email: hiro ＠ is.nagoya-u.ac.jp ★封筒に「情報システム学専攻教員応募書類在中」と朱書し，持参または書留で郵送して下さい． 10. 備考： (1) 応募書類は原則として返却しません． (2) 応募書類は本選考のみに使用し，他の目的には使用しません． (3) 選考の過程でプレゼンテーションをお願いすることがあります． (4) 本学では採用に際して男女共同参画に配慮しております． -- Shoji Yuen, Graduate School of Information Science, Nagoya Univ., Japan 結縁祥治　名古屋大学大学院情報科学研究科 +81-52-789-3649

1 0

情報処理学会全国大会企画「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」のご案内
by Kazutaka Matsuda 03 Mar '15

03 Mar '15

logic-ml関係者の皆様，東京大学の松田です．複数受け取られた場合はご容赦ください．この場をお借りして，情報処理学会全国大会の企画の一つとして 3/17の13:00〜15:30より京都大学吉田キャンバス吉田南総合館 2F 共北26で開催される「計算に潜む数理，計算としての数理 --- 証明はプログラミング！」 http://www.gakkai-web.net/gakkai/ipsj/77program/html/event/A-6.html のご案内をさせていただきたく存じます．情報処理学会全国大会は当日のご参加も受けつけており，企画セッションのみの聴講は無料です．詳しくは以下をご欄下さい． http://www.ipsj.or.jp/event/taikai/77/on_site_registration.html 本セッションでは，論理と計算に関する以下の3件の講演を企画しております． # 田中一之（東北大学大学院理学研究科教授）「決定問題の相転移について」 1920年代にヒルベルト学派が数理論理学の中心テーマとして掲げた「決定問題」は，狭義には1階論理における真偽を判定する手続きを求める問題である．これはゲーデルやチューリングによってすぐに否定的に解かれたが，その後も様々な角度から類似の問題が提起され，肯定的にも否定的にも豊富な結果と解決手法が生れた．肯定的な手法としては，オートマトンの強化がしばしば有効であるが，それをさらに非決定性にすると顕著に決定不能な結果が得られることがある．たとえば，決定性ω文脈自由言語のゲームは（計算的に）決定可能だが，非決定性の場合は通常の集合論で決定できない．本講演では，決定問題の大きな流れを振り返りつつ，決定可能性と不可能性の相転移現象についていくつかの例をもとに考察する．文献：田中一之『チューリングとメタパズル』東京大学出版会2013．田中一之『無限ゲームとオートマトン』数学セミナー2014年11月号． # 佐藤雅彦（京都大学名誉教授）「計算と論理」プログラミングという行為の背景にある計算と論理について解説する．特に，「プログラム」，「計算」，「論理」という3つの概念に共通するキーワードである「証明」に焦点を合せて，これら3概念の共通点，相異点を明きらかにし，プログラミングという行為の本質に迫ることを目標とする．直観主義的型理論において発見された「カリー・ハワード同型対応」は，命題と型の同型性に基づき，（命題の）「証明」と（型の要素としての）「プログラム」を同一視するという「証明」の見方を与えた．これは確かに有力な「ものの見方」であり，型を持つプログラミング言語や型理論に基づく Coq 等の証明支援系の理論的基盤を与えている．本講演では，このような「カリー・ハワード同型対応」によるプログラム観を紹介し，その有用性と同時にそれが抱える問題点を指摘する．上の型理論的証明観の問題点を理解するために，型理論誕生の動機となった18世紀末から19世紀初頭にかけての，「数学の危機」とよばれた数学の基礎付けをめぐる問題とその解決策が何であったかを説明する．これにより型理論を絶対視することなく，より広い観点からプログラミングという行為の本質に迫りたい． # AFFELDT　Reynald （産業技術総合研究所セキュアシステム研究部門・高信頼ソフトウェア研究グループ主任研究員）「定理証明支援系Coqによる形式検証」ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究課題である．1970年代からカリー＝ハワード同型対応に基づく形式体系の研究が継続的に行われてきた．その形式体系が定理証明支援系という形式検証ツールとして実現された結果，厳密で現実的な形式検証が可能となった．例えば，クリティカルな基盤ソフトウェア（コンパイラやオペレーティングシステム等）と大規模な数学の証明（四色定理やケプラー予想等）の形式検証が近年相次いで成功し，IT業界でも形式検証はスマートカードの厳密な安全性評価に応用されている．本発表では，ソフトウェアと数学の形式検証の実例を通じて，定理証明支援系による形式検証の基本を説明する．特に，ACMによる受賞を契機に注目を集めているフランス国立情報学自動制御研究所（INRIA）で開発されているCoqという定理証明支援系を紹介する．どうぞご参加を検討いただけますと幸いです．

1 0

Workshop on secure quantum computing
by NISHIMURA Harumichi 02 Mar '15

02 Mar '15

logic-mlの皆様，名古屋大学の西村です．群馬大学の森前先生に代わって secure quantum computingのワークショップのご案内を以下に投稿させていただきます．参加費無料，レジストレーション不要です．ご興味のある皆様の参加をお待ちしております．名古屋大学大学院情報科学研究科西村治道 ---------------------------------------- メーリングリストの皆様、群馬大の森前と申します。３月１９，２０日に東大本郷キャンパスで行われるWorkshop on secure quantum computingについてご案内させて頂きます。 http://tomoyukimorimae.web.fc2.com/Workshop_on_secure_quantum_computing.html 宜しくお願いします。森前 -------------------------------------

1 0

CSL 2015 - call for papers
by Kazushige TERUI 28 Feb '15

28 Feb '15

みなさま Computer Sicence Logic 2015のご案内をさせていただきます。アブストラクト締切は４月３日となっております。どうぞ奮ってご投稿ください。照井 ______________________________________________________________________________________________ CSL 2015 COMPUTER SCIENCE LOGIC 2015 Berlin, 7 - 10 September 2015 http://logic.las.tu-berlin.de/csl2015/ Call for Papers _______________________________________________________________________________________________ AIM AND SCOPE Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. LOCATION The 24th EACSL Annual Conference on Computer Science Logic will be held at the Technical University Berlin from Monday, 7 September 2015 to Thurday, 10 September 2015. LIST OF TOPICS OF INTEREST (NON EXHAUSTIVE) • automated deduction and interactive theorem proving • constructive mathematics and type theory • equational logic and term rewriting • automata and games, game semantics • modal and temporal logic • model checking • decision procedures • logical aspects of computational complexity • finite model theory • computational proof theory • bounded arithmetic and propositional proof complexity • logic programming and constraints • lambda calculus and combinatory logic • domain theory • categorical logic and topological semantics • database theory • specification, extraction and transformation of programs • logical aspects of quantum computing • logical foundations of programming paradigms • verification and program analysis • linear logic • higher-order logic • nonmonotonic reasoning INVITED SPEAKERS * Martín Abadi (Santa Cruz) * Elham Kashefi (Edinburgh) * Markus Lohrey (Siegen) * Ryan Williams (Standford) IMPORTANT DATES Abstract submission: 3 April 2015 Paper Submission: 10 April 2015 Paper Notification: 13 June 2015 Conference: 7 - 10 September 2015 SUBMISSION Authors are invited to submit papers of not more than 15 pages in LIPIcs style presenting work not previously published. Papers are to be submitted through Easychair. Submitted papers must be in English and must provide sufficient detail to allow the PC to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewers' discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the program committee. The submission is in two stages. Abstract submissions are due on 3 April 2015. Full paper submissions must be done on or before 10 April 2015. Papers must not be submitted concurrently to another conference with refereed proceedings. The PC chair should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the Programme Committee are not allowed. SATELLITE EVENTS * The 11th International Workshop on Fixed Points in Computer Science (FICS'15) will be held on 11 and 12 September 2015 as a co-located event of CSL’15. * YuriFest: we will celebrate Yuri Gurevich’s 75th birthday with a symposium in his honour on 11 and 12 September 2015 as a co-located event of CSL’15. * The annual meeting of the GI Fachgruppe Logik will be organised at the Technical University Berlin in conjunction with CSL'15. PROGRAMME COMMITTEE • Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) • Achim Blumensath (Technical University Darmstadt) • Mikolaj Bojanczyk (Warsaw University) • Maria Paola Bonacina (Università degli Studi di Verona) • Patricia Bouyer-Decitre (LSV, CNRS & ENS de Cachan) • Ugo Dal Lago (Università di Bologna) • Maribel Fernández (King's College London) • Richard Garner (Macquarie University, Sydney) • Rajeev Goré (Australian National University, Canberra) • Stéphane Graham-Lengrand (CNRS & École Polytechnique, Paris-Saclay) • Martin Grohe (RWTH Aachen University) • Lauri Hella (University of Tampere) • Martin Hofmann (Ludwig-Maximilians-University Munich) • Stephan Kreutzer (Technical University Berlin, pc chair) • Martin Lange (University of Kassel) • Luigi Santocanale (LIF, Aix-Marseille Université & CNRS) • Alexandra Silva (Radboud University Nijmegen) • Alex Simpson (University of Edinburgh) • Sonja Smets (University of Amsterdam) • Makoto Tatsuta (National Institute of Informatics, Tokyo) • Kazushige Terui (Kyoto University) • James Benjamin Worrell (University of Oxford) • Nobuko Yoshida (Imperial College London) ORGANISING COMMITTEE: • Christoph Dittmann (Technical University Berlin) • Viktor Engelmann (Technical University Berlin) • Stephan Kreutzer (Technical University Berlin, Chair) • Jana Pilz (Technical University Berlin) • Roman Rabinovich (Technical University Berlin) • Sebastian Siebertz (Technical University Berlin) ------------------------------------------ Kazushige TERUI Research Institute for Mathematical Sciences, Kyoto University. Kitashirakawa Oiwakecho, Sakyo-ku, Kyoto 606-8502, JAPAN. Phone: +81-75-753-7235 Fax: +81-75-753-7276 terui(a)kurims.kyoto-u.ac.jp http://www.kurims.kyoto-u.ac.jp/~terui/

1 0

JAIST Logic Seminar Series
by Hajime Ishihara 28 Feb '15

28 Feb '15

皆様ストックホルム大学のErik Palmgren先生の連続講義のお知らせです。ふるってご参加ください。問合せ先：石原　哉北陸先端科学技術大学院大学情報科学研究科 e-mail: ishihara(a)jaist.ac.jp -------------------------------------------------- * JAIST Logic Seminar Series * * This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project CORCON (http://corcon.net/). Date: Lecture 1. Monday 9 March, 2015, 15:10-16:40 Lecture 2. Tuesday 10 March, 2015, 15:10-16:40 Lecture 3. Wednesday 11 March, 2015, 15:10-16:40 Place: JAIST, Lecture room I3-I4 (Access: http://www.jaist.ac.jp/english/location/access.html) Speaker: Professor Erik Palmgren (Department of Mathematics, Stockholm University) Title: Lectures on type theory with a view towards formalizing Bishop-style mathematics Abstract: In this series of three lectures we give an introduction to Martin-Lof type theory and the tools it provides for formalizing Bishop-style constructive mathematics. The first lecture will cover basic principles of type theory and give an introduction to its manifestation in the well-known proof assistant Coq. In the second lecture we consider "Bishop's set theory" (Bishop and Bridges 1985) from the point of view of type theory, which will involve a development the theory of setoids and subsetoids. The third lecture will cover models constructive set theory (CZF) in type theory, and how it can be used to solve the problem of universes of setoids and development of category theory. Throughout the lectures we provide examples and suggestions how you can yourself experiment with the Coq system in the formalization of constructive mathematics. References E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985. E. Palmgren. Lecture notes on Type Theory. Stockholm 2014. URL: http://kurser.math.su.se/course/view.php?id=48 E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25.

1 1

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 25 Feb '15

25 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップをお知らせさせていただきます。重複して受け取られた場合はどうかご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (Basement 4F), South Building, Mita campus of Keio University. ( http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map. ) ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

KusatsuSeminar3/16--20: just a reminder
by Fujita Kenetsu 24 Feb '15

24 Feb '15

皆様，『ラムダ計算と論理の早春セミナー』のご案内　（再送）日程：2015年3月16日(月) 午後5時から3月20日(金) 正午まで場所：国立大学草津セミナーハウス　　　〒377-1711 群馬県吾妻郡草津町大字草津字白根737 詳細：http://www.cs.gunma-u.ac.jp/~fujita/2015.03LLSinKusatsu.htm 申込・質問などは藤田（群馬大学）までご連絡をお願いします．興味をお持ちのみなさまのご参加をお待ちしております． ----------- 群馬大学　藤田憲悦

1 0

論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri)
by Yuta Takahashi 24 Feb '15

24 Feb '15

みなさま、こんにちは、慶応大学の高橋優太と申します。この場をお借りして、次のワークショップのご案内をさせていただきます。重複して受け取られた場合はご容赦ください。 ---- 論理哲学ワークショップ 2月27日(金) / Workshop on Philosophy of Logic, Feb 27th (Fri) 次のような「論理哲学ワークショップ」を予定しております。今回は特に、現代論理の歴史的背景についても議論します。参加自由です。 The following Workshop on Philosophy of Logic is scheduled. The historical background of some modern logic will be discussed among others. 日時/Date&Time: 2015年2月27日(金) 14:00-17:00, Feb 27 (Fri), 2015 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. ---- 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs --------------------------------------------------------------------- 問合せ先: Mita Logic Seminar 思考と行動判断の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ABSTRACTS ENCLOSED BELOW: 1. Speaker: Juan Luis Gastaldi (IRePH, Université Paris Ouest Nanterre La Défense) Title: The relation between logical content and arithmetic in the semiotic constitution of Boolean logic Abstract: After the publication of his Begriffsschrift, Frege distanced himself from the Booleans by insistently opposing the content that his logic was able to express to the abstraction of Boolean logic. Frege’s commitment to the notion of content would last until the end of his work, becoming in particular the source of his famous distinction between sense and denotation. But what did Frege exactly mean by this opposition between “contentual” (inhaltlich) and abstract, as a properties of logical systems? A semiotic perspective on the constitution of Boolean logic shows that this distinction can be associated with the one between Arithmetic and Algebra, considered as different mathematical practices on signs respectively underpinning the constitution of these two logical systems. Moreover, a particular attention paid to Boole's own voluntary deviations from what would soon become the standard Boolean system permits to identify different figures of what can be seen as a content dimension arising as a logical effect of the semiotic properties of Arithmetic. 2. Speaker: Yuta Takahashi (Keio University) Title: The Intuitionistic Background of Gentzen's 1935/36 Consistency Proofs Abstract: Gerhald Gentzen gave three consistency proofs for number theory. These consistency proofs have a common aim that originates from Hilbert's Program. Hilbert, in his program, aimed to justify the use of ideal propositions in mathematics, by showing that no contradiction can be derived in a formal system of the ideal parts of mathematics. Gentzen aimed to justify the use of ideal propositions in number theory, and this aim is prominent especially in Gentzen's 1938 consistency proof. In Gentzen's 1935/36 consistency proofs, there is another aim that is not found in Hilbert's Program. The aim is to formulate a ``finitary'' interpretation that gives a meaning to every ideal proposition of number theory and makes the theory sound. In this talk, first we argue that what motivated Gentzen to give such an interpretation is an intuitionists' objection against the significance of consistency proofs. Second, we show that his way of the interpretation appealed to a notion being very close to the notion of spreads, which was introduced in intuitionistic mathematics. As a consequence, we claim that intuitionism was deeply related to both Gentzen's motivation and method for the interpretation. END OF ANNOUNCEMENT------------------------------------------------

1 0

千葉 logic seminar
by arai toshiyasu 23 Feb '15

23 Feb '15

みなさま新井@千葉大学です。千葉 logic seminar の第5回のお知らせです。どなたでも参加できますのでどうぞ気軽にいらっしゃって下さい。問合せ先新井敏康（千葉大学） tosarai(a)faculty.chiba-u.jp ------------------------------------------ 日時：3月13日(金)13:30-15:00 場所：千葉大学理学部2号館105号室アクセスは http://www.chiba-u.ac.jp/campus_map/nishichiba/index.html の地図の黄色い理学部の中で数字2が付いている建物の1階です。 Speaker: Stan Wainer (Leeds UK) Title: A miniaturized predicativity Abstract: This talk attempts to characterize those recursive functions which are "predictably terminating" according to a finitistic point of view. The basis of the work is Leivant's (1995) theory of ramified induction over N, which has elementary recursive strength. It has been redeveloped and extended in various ways by many people. Eg. Spoors & W. (2012) built a hierarchy of ramified "input-output" theories whose strengths correspond to the levels of the Grzegorczyk hierarchy. Here, a further extension of this hierarchy is developed, with one additional input level on top (level omega). The underlying logic is an autonomously generated infinitary calculus with arbitrary finitely-many stratification levels of numerical inputs and a ramified Repetition Rule. The autonomous control on allowable ordinals is based on a weak (finitistic) notion of "pointwise transfinite induction". It turns out that the ordinal of this theory is then Gamma-0; the provably computable functions are those which are resource-bounded by the slow growing hierarchy; and these are the functions elementary recursive in the Ackermann function. ------------------------------------------------------------------------------------------

1 0

鈴木右京のセミナー (名古屋大学にて)
by Jacques Garrigue 19 Feb '15

19 Feb '15

logic-mlの皆さん、名古屋大学多元数理科学研究科のJacques Garrigueです。突然ですが、以下のセミナーを開催しますので、ご案内申し上げます。講演者:　鈴木佑京（東京大学大学院広域科学科）日時:　　2月24日（火）　10:30--12:00と13:00--14:30 会場:　　名古屋大学　理学A館　A328号室タイトル:　可述算術の世界アブストラクト: エドワード・ネルソンは、古典的算術に対するオルタナティブでありながら、直観主義的算術や有限主義的算術とも異なる――より徹底した構成主義の立場に立つ ――自然数論として、「可述算術」と呼ばれる理論を提案した。彼の理論は、後の限定算術の研究に影響をあたえるとともに、数学的帰納法に関する独特な分析を含んでおり、極めて興味深い。この講演では、１）まずネルソンの構成主義的な思想を説明した後、２）可述算術の数学的展開を解説することで、まず可述算術に対するイントロダクションを行う。そののち、３）ネルソンのような改訂主義とは異なる、講演者自身の観点から、可述算術の持つ概念的な興味を解説する。ここでは、可述算術が、ウィトゲンシュタインなどが展開した「概念形成としての数学」という描像をモデル化したものであることが主張される。

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml