Logic-ml September 2016

15 participants
22 discussions

homotopy type theory
by logic＠math.tsukuba.ac.jp 30 Oct '16

30 Oct '16

> 圏論に関して質問があります。 > 種々の圏の存在はどのようにして主張されますか？ > > 例えば、公理的集合論では、論理式f(x),集合Xに関して、Xの元xでf(x)を満たすもの > から成る集合{x \in X|f(x)}が存在することが分出公理によって言えますが、圏論に > おいても、圏の存在を主張する公理群が定められていますか？ > 上記のような質問をいただいていますが、これはこの質問者以外の広い範囲の方に関心があることと思われますので、ここにお答えします。質問者の名前等は削除してあります。まず質問を Homotopy type theoryはZFCにかわる数学の基礎づけになるという話であるが、集合論はたとえばComprehensionのような豊かな構成原理をもっているが、HTTはどうなのか？と変形させていただきます。まずHTTのなかではn-typeというHierarchyが定義されます。ｎは−２以上の整数です。これはHomotopy theoryから借用された概念で、n-typeというのはｎを越える次元ではhomotopicalにはtrivialであることを意味します。Homotopy theoryの言葉づかいで言うならば、ｎを越える次元のhomotopy groupsはすべてtrivialであることを意味します。０-typeがいわゆるsetで、ここに話を限定するならば comprehensionをはじめとする集合論的構成はだいたいそのまま行えます。一般にはdependent function typeやdependent pair typeという構成原理を最初から内臓していますが、これだけではもちろん足りません。HTTがもつ強力な構成原理はinductionで、特に higher inductionが重要な役割を演じます。計算機言語のCOQや AGDAは通常にinductionを組み込んでいますが、higher inductive typesはまだ持っておりません。少しslogan的な言い方を許していただければ、 inductive typesはfree monadsに、higher inductive typesはmonadsの表現に対応します。 Inductiveな構成のいい例はCauchy realsの構成です。自然数から有理数を作るのは、古典的な話とあまりかわりません。それで有理数から実数を作るには、Dedekindのやり方とCauchyのやり方がありますが、後者の構成をinductiveにやるとどうなるかが、 https://homotopytypetheory.org/book/ の１１．３節に縷説されています。あるいはcirclesやspheresやsuspensionsはどのようにinductiveに構成されるか、第６章に縷説されています。是非ご覧になってください。にしむら筑波大学数学追伸：オマケです。手持無沙汰な折にどうぞ。 https://www.youtube.com/watch?v=VY01dVHvlFE

2 2

ワークショップ「2階論理の意味論」
by Makoto Kikuchi 30 Sep '16

30 Sep '16

皆様，以下の要領でワークショップを開催しますのでお知らせします．神戸大学菊池誠日時：2016年11月5日（土）15:45〜17:45 場所：東京大学駒場キャンパス1号館1階108室題目：ワークショップ「 2階論理の意味論」　　科学基礎論学会2016年度秋の研究例会（非会員は参加費1,000円が必要です）　　科学基礎論学会 Web Page：http://phsc.jp オーガナイザ：菊池誠（神戸大学）提題者：　佐藤智哉　2階論理的妥当性の新しい意味論的特徴づけ　池上大祐（東京電機大学）2階論理とブール値2階論理　新井敏康（千葉大学）竹内の基本予想の意味論的証明ワークショップ趣旨：「すべて」や「存在」という量化の対象が「個物」に限定される形式的論理が 1階論理，「個物と概念」であるのが2階論理，そして「個物，概念，概念上の概念，…」のすべてであるのが高階論理である．1階論理が形式的論理の現在の事実上の標準理論である．ただし，BoolosやShapiro，Vaananenの哲学的な議論やFriedmanの逆数学の研究プログラムにも見られるように，今でも2階論理それ自身や2階論理の上で展開される公理系に関心が持たれている． 2階論理の意味論を考える際に問題になるのが「概念」を対象とする2階量化子の解釈である．2階量化子の解釈は「個物全体の集合」の部分集合族を与えることで定められる．最も自然な2階論理の意味論は2階量化子の解釈を与える部分集合族を「個物全体の集合」の冪集合とすることで定められるが，この意味論では通常の公理と推論規則で2階論理の完全性定理は成り立たない． Henkinは2階量化子の解釈を与える部分集合族を「個物全体の集合」の任意に選ばれた部分集合族とすれば，通常の公理と推論規則で2階論理の完全性定理が成り立つことを示した． Henkin流の意味論が2階論理の現在の事実上の標準的な意味論である．しかし，このHenkin流の意味論に基づく2階論理とは実質的には1階論理の特別な場合であり，他の意味論の可能性や必要性がない訳ではない．本ワークショップではHenkin流の意味論以外の2階論理の意味論について，佐藤智哉が哲学の立場から，池上大祐が集合論の立場から最近の研究を紹介し，新井敏康が証明論の立場から古典的な議論を紹介する．提題要旨：提題1：2階論理的妥当性の新しい意味論的特徴づけ　佐藤智哉二階述語論理の標準意味論に関する一つの問題は、標準意味論においては特定の集合の特定の性質に依存するような論証が妥当となることである。そのような集合論の結果に基づく論証は「集合論的妥当」とでも呼ばれるべきで、「論理的妥当」な論証とは区別されなければならない。標準意味論の中で妥当となる論証のうち、どの論証が真の意味での論理的妥当であり、どの論証が集合論的妥当なのか。二階述語言語の論理的妥当性を特徴づけるためには、標準意味論とは別の新しい意味論システムが必要である。本発表の主目的は、そのような標準意味論に代わる新しい意味論システムの紹介である。新しい意味論システムのための一つのアイデアは、論理定項とは何かという哲学的議論が、論理的妥当性と集合論的妥当性の区別に応用できるということである。Tarskiに始まる近年の論理定項研究を紹介した後で、それを使ってどのように二階論理的妥当性が参考文献 D. Bonnay, Logicality and invariance, The Bulletin of Symbolic Logic, 14, 29–68, 2008. S. Feferman, Logic, logics, and logicism, Notre Dame Journal of Formal Logic, 40, 31–54, 1999 G. Sher, The Bounds of Logic: A Generalized View Point, Cambridge, MA: MIT Press, (1991). T. Sato, A new semantic characterization of second-order logical validity (unpublished). A Tarski, What are logical notions? J. Corcoran (Ed.), History and Philosophy of Logic, 7, 143–154, 1986. 提題2：2階論理とブール値2階論理　池上大祐（東京電機大学）二階述語論理の代表的な意味論としてタルスキ意味論（完全意味論）とヘンキン意味論の二つがある。タルスキ意味論を用いると、一階述語論理で表現できない様々な性質を記述できるが、一階述語論理において成り立つ定理（完全性定理、コンパクト性定理など）がことごとく成り立たず、二階述語論理は非常に複雑になる。一方、ヘンキン意味論を用いると、一階述語論理において成り立つ多くの定理が成り立つが、論理の表現力は一階述語論理と全く同じで、一階述語論理と比べて二階述語論理に新しい現象は見られない。本講演では、二階述語論理の意味論としてブール値意味論を導入し、 1) V = L の下ではブール値意味論はタルスキ意味論と同じ複雑さを持つこと 2) 巨大基数とウディンのΩ論理についての適切な仮定をすると、ブール値意味論は、　タルスキ意味論より単純でヘンキン意味論より複雑な意味論になることの二点について論じる。本講演で述べる多くの研究成果は Jouko Vaananen 氏との共同研究によるものである。参考文献 D. Ikegami and J. Vaananen, Boolean-Valued Second-Order Logic, Notre Dame Journal of Formal Logic, 56 (1), 167–190, 2015. 提題3：基本予想の意味論的証明　新井敏康（千葉大学）竹内外史は1953に高階論理GLCを定め，GLCについてCut除去定理が成り立つという基本予想を提示した．GLCの部分体系である2階論理がG1LCであり，竹内外史はG1LCの部分体系で基本予想が成り立つことを構文論的に示した．意味論的には，まずCutを持たない体系の3値モデルに対する完全性がSchutteによって示され，その後，3値モデルを2値モデルに完備化する方法で，G1LCについてはTaitによって，GLCについては高橋元男とPrawitzによって独立に，竹内の基本予想が成り立つことが証明された．その意味論的な議論を紹介する．参考文献新井敏康「竹内の基本予想とは何か，何であるべきか」数理解析研究所講究録, 1442, 1-7, 2005.

1 0

Talk by Yoriyuki Yamagata (6 Oct 11:00-)
by Tetsuya Sato 29 Sep '16

29 Sep '16

京都大学数理解析研究所の佐藤です。 10月6日11:00から、産業技術総合研究所の山形頼之氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 6 Oct, 2016 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Yoriyuki Yamagata (National Institute of Advanced Industrial Science and Technology) (Website: http://staff.aist.go.jp/yoriyuki.yamagata/en/) Title: Consistency proof of an arithmetic with substitution inside a bounded arithmetic Abstract: Bounded arithmetics are systems of arithmetic in which induction is restricted to bounded formulas. Bounded formulas are formulas in which all quantifiers are bounded by some terms. Among many such systems, Buss's hierarchy of bounded arithmetics have particular interest, because their provably total functions exactly correspond polynomial-time hierarchy. A major open problem on bounded arithmetics is whether Buss's hierarchy collapses or not. If it collapses, for example, it implies P=NP. One strategy to differentiate the hierarchy is to use Gödel sentence of some theories. In this talk, we consider a theory PV by Cook and Urquhart and its restrictions. PV is an equational system, which has roughly the same strength to Buss's S12. Beckmann proved that when induction and substitution are removed from PV, the consistency of the system can be proved by S12. On the other hand, Buss and Ignjatović proved that S12 cannot prove the consistency of the system which obtained by removing just induction, but adding propositional logic and BASIC axioms, from PV. In this talk, we improve the Beckmann by proving that S22 can prove the consistency of the system which obtained by removing just induction from PV. By delineating bounded arithmetics which can prove consistency of various restrictions of PV, we hope to prove non-collapse of Buss's hierarchy, and relatedly, polynomial-time hierarchy.

1 0

締切延長：第51回MLG数理論理学研究集会（10/27-30箱根）
by Kazushige TERUI 26 Sep '16

26 Sep '16

みなさま先日来ご案内しているMLG研究集会についてですが、宿泊・講演ともまだ余裕がありますので、締切を９月２９日（木）まで延長したいと思います。なお今回はチェコ科学アカデミーから以下の方々が参加されます。 Petr Cintula（数理ファジィ論理・抽象代数論理など） Zuzana Hanikova（ファジィ集合論など） Rostislav Horcik（部分構造論理など） Carles Noguera（数理ファジィ論理・抽象代数論理など） Tommaso Moraschini, Adam Prenosil, Igor Sedlar, Amanda Vidal うち数名の方には入門的な講演をお願いする予定です。３泊４日ですが、部分参加も歓迎します。どうぞよろしくお願いします。照井 --------------------------------------------------- 第51回MLG数理論理学研究集会締切延長 MLG数理論理学研究集会は，1971年開始された，この分野の多くの研究者が参加している40年以上続く研究集会です。成果を発表し合ったり，アイデアを交換したりと，ザックバランな雰囲気で行われています。数学の他分野や，広く数理科学，情報科学，哲学の方々や，外国からの研究者を迎えるなど，オープンに運営されています。（昨年度の様子：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2015.html ）日時：2016年10月27日（木）午後 − 30日（日）午前場所：四季の湯強羅静雲荘（ http://gora-seiunsou.jp/ ）参加費用：全参加の場合30,000円（3食つき、懇親会費は別途）参加・講演申し込み： 9月29日（木）までウェブページ：http://www.kurims.kyoto-u.ac.jp/~terui/mlg2016.html 詳細は上記Web Pageをご覧ください。みなさまの参加をお待ちしております。京都大学数理解析研究所照井　一成 ------------------------------------------ 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

correction again
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信＠名古屋大学大学院情報科学研究科です。すでに何人の方からご指摘いただきましたように、セミナーご案内の日時も誤っておりました。重ねてお詫びいたしますとともに、訂正したものを改めて投稿させていただきます。名古屋数学基礎論セミナーのご案内日時：9月23日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

correction
by 吉信康夫 21 Sep '16

21 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。先ほどお送りしたセミナーのご案内で、講演者のお名前の字が誤っておりました。お詫びいたしますとともに、訂正したものを改めてお送りいたします。名古屋数学基礎論セミナーのご案内日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴行 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

nagoya logic seminar
by 吉信康夫 20 Sep '16

20 Sep '16

皆様：吉信康夫＠名古屋大学大学院情報科学研究科です。以下の要領で名古屋数学基礎論セミナーを開催します。奮って御参加下さい。日時：9月13日(金) 15:30- 場所：名古屋大学大学院情報科学研究科棟 2F 206号室講演者：木原貴之 (University of California, Berkeley) タイトル：　多対一次数の一様Martin予想とWadge次数アブストラクト：　多対一次数は，決定問題の計算論的複雑性を測る指標の一つであり，Wadge次数は，ベール空間の部分集合の位相的複雑性を測る指標の一つである．両者の定義は酷似している一方，多対一次数構造は混沌として掴み所がなく，Wadge次数構造は美しく整然としており単純明快である．したがって，それらの酷似した定義とは対照的に，それらの構造は如何なる意味でも同型ではない．それにも関わらず，「自然」な多対一次数の構造と Wadge次数構造が同型であることを示す．　より正確には，Woodinによって提案された決定性公理の拡張であるAD+の下で，任意の better-quasi-order Q に対して，一様次数不変な Q 値多対一次数の構造と Q 値Wadge次数構造が同型であることを示す．

1 0

公募
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください

1 0

(no subject)
by 泉英明 19 Sep '16

19 Sep '16

皆様千葉工業大学教育センター数学教室の泉です。現在、当数学教室では助教１名の公募を行っております。締切は 2016年10月20日(必着)となっております。詳細については http://www.it-chiba.ac.jp/institute/adoption/ をご覧ください。

1 0

数学基礎論とその応用
by Makoto Kikuchi 17 Sep '16

17 Sep '16

皆様，以前にもご案内しましたが，2016年9月26日（月）から29日（木）まで， RIMS 研究集会「数学基礎論とその応用」を開催しますのでお知らせします． http://www2.kobe-u.ac.jp/~mkikuchi/mla2016.html 事前登録なしで参加できます．また，以下の要領で懇親会を開きます．日時：2016年9月28日（水）午後6時から会場：マーブルルーム https://www.hotpepper.jp/strJ000040535/ 場所：京都府京都市中京区先斗町通三条下ル橋下町135先斗町ビル4F 交通：京阪三条駅から徒歩5分，阪急河原町駅から徒歩10分内容：立食（飲み放題）会費：3,000円（当日会場で支払い） 8月に研究集会への参加申し込みをお送り下さった方で，懇親会への出欠の変更のない方はご連絡くださる必要はありません．出欠を変更される方，未定とお答えになられた方，また，参加申し込みをなさっていない方で懇親会への出席をご希望の方は，2016年9月24日（土）までに，研究代表者（菊池）宛に件名「mla2016」として e-mail でご連絡ください．なお，本研究集会は研究交流を目的とするものですが，学部学生を含む学生の方の研究集会および懇親会への参加を歓迎します．午前中の講演は全て日本語です．ご興味をお持ちの方はご遠慮なくご参加ください．菊池誠記 RIMS研究集会　数学基礎論とその応用日時：2016年9月26日(月)11:00 ~ 9月29日(木)15:00 場所：京都大学数理解析研究所111室研究代表者：菊池誠(神戸大)mkikuchi(a)kobe-u.ac.jp プログラム： 9月26日(月) 11:00-11:50 宮元忠敏(南山大) 集合論で試される構造と構成のいくつか 13:30-14:20 Joel David Hamkins(CUNY) The Modal Logic of Set-Theoretic Potentialism 14:30-15:20 樋口幸治郎(日大工) Computably Represented Structures 15:30-16:20 竹内耕太(筑波大) Properties Characterized by Generalized Indiscernible 9月27日(火) 10:00-10:50 新井敏康(千葉大) 角田先生, 証明論を分かって下さい 11:00-11:50 板井昌典(東海大) 1980年代半ば,米国中西部のモデル理論,そして未来-モデル理論賛歌 13:30-14:20 Frank Wager (Lion 大) Recent Interactions between Model Theory and Combinatorics 14:30-15:20 横山啓太(JAIST) On the Proof-Theoretic Strength of Ramsey's Theorem for Pairs 15:30-16:20 丸山善宏(京大) Dynamics of Duality: How Duality Emerges, Changes, and Breaks 9月28日(水) 10:00-10:50 向井国昭(慶応大) Barwiseのモデル論的意味論の周辺と抽象設計学 11:00-11:50 金井康雄(大和大) 公理的集合論の一角を彷徨って 13:30-14:20 Bakh Khoussainov(Auckland 大/京都大) Computably Enumerable Structures: Domain Dependence 14:30-15:20 星野直彦(京都大) Geometry of Interaction and Higher Order Functions 15:30-16:20 Diego Mejia(静岡大) Several Values in Cichon's Diagram 9月29日(木) 10:00-10:50 佐藤洋祐(東理大) 限量子記号消去アルゴリズムとその計算の現状について 11:00-11:50 隈部正博(放送大) Generic Sets の Turing Degrees について 13:30-14:20 Philip Welch(Bristol 大) Generalised Squares and Higher Stationarity

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml September 2016