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

古典述語論理に対応する項計算体系の研究

Research Project

Project/Area Number 12740077
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionHosei University

Principal Investigator

安東 祐希  法政大学, 第一教養部, 助教授 (40277687)

Project Period (FY) 2000 – 2001
Project Status Completed (Fiscal Year 2001)
Budget Amount *help
¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 2001: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2000: ¥600,000 (Direct Cost: ¥600,000)
Keywords自然演繹 / 古典論理 / 合流性 / 正規化定理
Research Abstract

自然演繹計算はゲンツェンにより導入された形式的論理体系の一つであり、通常の数学において用いられる推論と密接な関係を持つ。その論理体系の基本的性質の一つとして、最大論理式の縮約方法に関する諸定理がある。その中の合流性定理、すなわち始点を共有する縮約列に関してそれを合流する縮約列を構成することができるという定理については、直観主義論理の特に可換性縮約を含まない体系について良く知られていたが、それ以外の体系については直接的な証明が必ずしも得られていなかった。それは、可換性縮約が縮約点の増長をもたらし、単純な合流性証明の適用ができないためである。本研究においては、この困難を克服する方法の改良を行った。そこでは、直観主義論理の可換性縮約のみならず、古典主義論理の二重否定除去に起因する縮約に関しても、構造的縮約として統一的に扱われている。表現の簡略化のためには、項計算体系を、伸縮性を持つ縮約点の連続的な縮約を表現できるように拡張する手法が用いられている。その際、特に古典論理に特有な、縮約点による木構造が項の生成規則に関して飛躍を持ち、それが互いに分離されない場合に関して、拡張された項表現を用いた代入形式を整備した。特に、構造的な縮約の連続において生成される木構造を、元の証明図あるいは項の部分構造に制限した場合、本来の木構造とはなり得ぬ集合を、潜在的な木構造として扱うことが必要となるが、それに対してさらに拡張された代入形式を定義し、その代入形式間の可換性に関する研究を進めた。

Report

(2 results)
  • 2001 Annual Research Report
  • 2000 Annual Research Report
  • Research Products

    (2 results)

All Other

All Publications (2 results)

  • [Publications] ANDOU Yuuki: "Church-Rosser property of a simple reduction for full first order classical natural deduction"Annals of Pure and Applied Logic. (発表予定).

    • Related Report
      2001 Annual Research Report
  • [Publications] ANDOU,Yuuki: "Strong normalization of classical natural deduction (abstract)"Bulletin of Symbolic Logic. vol.7,no.1(発刊予定). (2001)

    • Related Report
      2000 Annual Research Report

URL: 

Published: 2000-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi