• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Revisiting ordinal notation systems in proof theory: from the viewpoint of linear logic

Research Project

Project/Area Number 21K12822
Research Category

Grant-in-Aid for Early-Career Scientists

Allocation TypeMulti-year Fund
Review Section Basic Section 01010:Philosophy and ethics-related
Research InstitutionOchanomizu University

Principal Investigator

高橋 優太  お茶の水女子大学, 文理融合 AI・データサイエンスセンター, 特任助教 (70826990)

Project Period (FY) 2021-04-01 – 2026-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2025: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2024: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Keywords型理論 / 証明論 / 順序数 / 構成的集合論 / 項書換え / 論理学の哲学 / 数学の哲学 / 数学基礎論
Outline of Research at the Start

数理論理学の一分野である証明論は、数学における証明を抽象化した上で「証明の大きさ」の概念を数学的に定義し、小さいものから順に際限なく構成されるものとして証明を捉える。そして、この観点のもとで数学における無限を解明しようとする。しかし、ここでいう「構成」とは何なのかという問いは数学の中だけで扱えるものではなく、この問いを探究するためには哲学的研究も必要になる。本研究は、同じく数理論理学の一分野である線形論理がもたらす相互作用という観点を援用し、この問いに取り組む。以上の探究を通して、数学における無限およびそれを捉える人間の論理的思考を解明し、その成果を情報科学などの他分野へ応用することを目指す。

Outline of Annual Research Achievements

19世紀末に創始された数理論理学は、閉じて完成している集まりとして無限を扱う実在論と、際限なく続く開いたプロセスとして無限を扱う反実在論という二つの立場に厳密な数学的定式化を与えた。特に、数理論理学の一分野である証明論は、順序数表記系と呼ばれる数体系を導入し、公理系の中の形式的証明をこの表記系の中の数に対応付けることで、当の公理系を反実在論的立場から解釈する方法を与えた。一方で、同じく数理論理学の一分野である線形論理は、形式的証明をゲームの観点から捉える数学的・概念的枠組みを証明論にもたらした。この枠組みにおいては、ゲームにおけるエージェントどうしの相互作用に焦点が当てられ、ここでの相互作用は言語行為を介するものとみなすこともできる。
本研究の目的は、線形論理がもつこのゲーム的・言語行為的観点から、形式的証明を順序数に対応づける従来の証明論的反実在論を反省し分析することである。
本年度は、前年度に引き続き、順序数とゲームを共存させることのできる枠組みとして型理論に着目し、特にマーティン・レーフ型理論(MLTT)に関する研究を行なった。前年度に従事した、ユニバース型と呼ばれるデータ型の構成についての研究を発展させ、構成的集合論(constructive set theory)をMLTTへと埋め込む試みに着手した。構成的集合論は反実在論の立場に基づく集合論であり、順序数を集合の一種として捉える点は古典的集合論と変わらないが、構成的集合論においては、集合から成る無限領域は際限なく構成されるプロセスとして捉えられる。こうした構成的集合論にさらに巨大集合に関する公理を加えることで得られる集合領域を、対応するユニバース型の構成をさらに強力にすることでMLTTに埋め込む方法を精査し、新たな方法につながる部分的な成果を得ることができた。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本年度は、線形論理がもたらすゲーム的観点についての研究は行なえなかったものの、構成的集合論とMLTTとの関係性を精査することで集合一般の反実在論的な理解を深められたことが主な理由である。前述の通り集合論において順序数は集合の一種となるため、本年度の成果は、証明論における順序数表記系をMLTTの中で構成する際に新たな知見を提供しうる。
また、MLTTの中で順序数表記系をゲーム的観点から構成している先行研究の手法は、MLTTを代数的に定式化する枠組みに基づくものであるが、この枠組みについてのサーベイも進めることができた。

Strategy for Future Research Activity

次年度からは、本年度までに蓄積した線形論理に関する研究および型理論に関する研究に基づき、MLTTの中で順序数表記系を線形論理的方法でもって構成する研究に着手する。そのためにまず、MLTTの中で順序数表記系をゲーム的観点から構成している前述の先行研究の成果を線形論理的方法により分析する。特に、この先行研究におけるゲームの概念と線形論理におけるゲームの概念とを比較し、前者を後者によって捉えることができるかどうか精査する。
以上に加え、線形論理分野での最先端の研究もサーベイし、本研究課題の構想時にはなかったアイデアおよび観点を加えることを試みる。

Report

(3 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • 2021 Research-status Report
  • Research Products

    (10 results)

All 2024 2023 2022 2021

All Journal Article (2 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 2 results,  Open Access: 2 results) Presentation (8 results) (of which Int'l Joint Research: 6 results)

  • [Journal Article] Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus2022

    • Author(s)
      Yuta Takahashi
    • Journal Title

      27th International Conference on Types for Proofs and Programs (TYPES 2021), Leibniz International Proceedings in Informatics (LIPIcs)

      Volume: 239

    • Related Report
      2022 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Harmony in the Light of Computational Ludics2021

    • Author(s)
      Alberto Naibo, Yuta Takahashi
    • Journal Title

      Electronic Proceedings in Theoretical Computer Science

      Volume: 353 Pages: 132-156

    • DOI

      10.4204/eptcs.353.7

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] Type Checking for Logical Approach to Natural Language Inference2024

    • Author(s)
      Yuta Takahashi
    • Organizer
      French-Japanese Colloquium Disagreement in logic and reasoning
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Towards an Interpretation of Inaccessible Sets in Martin-Loef Type Theory with One Mahlo Universe2023

    • Author(s)
      Yuta Takahashi
    • Organizer
      TYPES 2023: 29th International Conference on Types for Proofs and Programs
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Higher-Order Universe Operators in Martin-Loef Type Theory with one Mahlo Universe2022

    • Author(s)
      Yuta Takahashi
    • Organizer
      TYPES 2022: 28th International Conference on Types for Proofs and Programs
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] 論理推論とは何か―証明論的意味論の観点から―2022

    • Author(s)
      高橋優太
    • Organizer
      慶應義塾大学論理と感性のグローバル研究センター2021年度末成果報告会
    • Related Report
      2021 Research-status Report
  • [Presentation] On Gentzen's Consistency Proofs: A Case of Disagreement between Intuitionism and Formalism2022

    • Author(s)
      Yuta Takahashi
    • Organizer
      Aspects of Logic Study: An event organized as a series of "Disagreement in Logic and Reasoning" research
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] マーティン-レーフ型理論における対象の同一性基準について2021

    • Author(s)
      高橋優太
    • Organizer
      日本論理哲学会第25回大会
    • Related Report
      2021 Research-status Report
  • [Presentation] Fixed-point operators: from proof-theoretic semantics to computation2021

    • Author(s)
      Alberto Naibo, Yuta Takahashi
    • Organizer
      EXPRESS-IHPST workshop: Truth, proof and communication
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Size-Based Termination for Non-Positive Types2021

    • Author(s)
      Yuta Takahashi
    • Organizer
      TYPES 2021: 27th International Conference on Types for Proofs and Programs
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2021-04-28   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi