Mathematical Sciences: A Model-Theoretic Approach to Proof Theory

数学科学：证明论的模型理论方法

• 批准号: 9614851
• 负责人: Jeremy Avigad
• 金额: $ 6万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-08-01 至 1999-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9614851&HistoricalAwards=false
• 关键词: Mathematical; Sciences; Model; Theoretic; Approach

While Zermelo-Fraenkel set theory provides a broad and flexible framework for the formalization of mathematics, recent proof-theoretic research has shown that a good deal of day-to-day mathematical argumentation correlates more closely with much weaker subsystems of second-order arithmetic. In this project Avigad will use model-theoretic techniques to explore the finitary combinatorial consequences of these theories. This includes finding Ramsey-theoretic independences akin to the Paris-Harrington theorem, and developing a combinatorial, model-theoretic approach to ordinal analysis. The aim of mathematical logic is to create formal models that describe various aspects of mathematical practice, and apply mathematical techniques to the analysis of these models. Since the beginning of this century, two conflicting and antagonistic views of mathematics have shared an uneasy coexistence. From a classical point of view, mathematics is "about" the infinite, yielding powerful and compelling abstractions. From a constructive point of view, mathematics must always have some concrete, computational meaning, from which it derives its applicability. This project aims to obtain a better understanding of the interplay between these two aspects of mathematical practice, through the formal exploration of infinitary assumptions and their finite, combinatorial consequences.

虽然Zermelo-Fraenkel集合理论提供了一个广泛而灵活的框架， 对于数学的形式化，最近的证明理论研究 大量的日常数学论证 与二阶算术的弱得多的子系统更接近。在 该项目将使用模型理论技术来探索 这些理论的有限组合结果。这包括 发现拉姆齐理论的独立性类似于巴黎-哈林顿 定理，并开发一种组合，模型理论的方法， 序分析 数理逻辑的目的是建立形式化的模型， 数学实践的各个方面，并应用数学 这些模型的分析方法。年初以来 这个世纪，两种相互冲突和对立的数学观点 共同生活在一个不和谐的环境中从经典的观点来看， 数学是“关于”无限的，产生强大的和令人信服的 抽象从建设性的角度来看，数学必须 总是有一些具体的，计算的意义， 得出其适用性。该项目旨在获得更好的 理解这两个方面之间的相互作用， 数学实践，通过形式探索无穷 假设及其有限的组合后果。