arXiv 2109.062582021-09math.LO

Unprovability in Mathematics: A First Course on Ordinal Analysis

Anton Freund

英文摘要：

These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskal's theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assume a solid introduction to mathematical logic but no specialized knowledge of proof theory. The material in these notes is intended for 12 lectures and 6 exercise sessions of 90 minutes each.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

逆向数学与无排中证明的一致性

Reverse mathematics and uniformity in proofs without excluded middle

我们表明，当某些语句是可证明的子系统的建设性分析，使用直觉谓词演算，相关的顺序语句是可证明的弱经典子系统。特别地，如果一个特定形式的$Π^1_2$语句可以使用E-HA ${}^ω$连同选择选择公理和前提独立性原则来证明，则该语句的序列形式在经典系统RCA中是可证明的。我们得到这个和类似的结果使用修改的可实现性和\textit{Dialectica}解释的应用。这些结果使我们能够使用技术的经典逆向数学证明的不可证明性的几个数学原理的子系统的建设性分析。

2010-10-25math.LO

The Foundations of Mathematics in the Physical Reality

In this article we present an axiomatic definition of sets with individuals and a definition of natural numbers and ordinals. We use the axioms pairs, union, power, regularity and separation. We define the equality of sets and of individuals. There is no empty set. A single shoe is not a singleton set but an individual, a pair of shoes is a set. We call limit ordinals first numbers, that is a first number of the Peano axioms. An axiom of infinity is postulated and we prove the Peano axioms for ordinals with a first number up to a first $ω^ω$-number. Then we prove a first $ω^ω$-number notequal …

2022-05-30math.LO

构造性序数理论

Constructive theory of ordinals

本文提出一种仅基于两种序关系的构造性序数理论，利用上确界运算与序关系的相互作用逼近线性序概念，证明其满足构造性性质，加入经典逻辑可恢复通常序数但会损失可计算性。

2024-12-10math.LO

序数分析讲义

Lectures on Ordinal Analysis

本文档是根特大学数学系于2023年3月14日至25日开设的关于序数分析的微型课程的讲义。

2023-04-01math.HOmath.LO

Well-Ordering Principles in Proof Theory and Reverse Mathematics

Several theorems about the equivalence of familiar theories of reverse mathematics with certain well-ordering principles have been proved by recursion-theoretic and combinatorial methods (Friedman, Marcone, Montalban et al.) and with far-reaching results by proof-theoretic technology (Afshari, Freund, Girard, Rathjen, Thomson, Valencia Vizcano, Weiermann et al.), employing deduction search trees and cut elimination theorems in infinitary logics with ordinal bounds in the latter case. At type level one, the well-ordering principles are of the form (*) "if X is well-ordered then f(X) is well-ord…

2020-10-23math.LO

数理逻辑导论-问题解决课程

Introduction to mathematical logic - A problem solving course

这是一套288道题，为摩尔式的数理逻辑课程而写。我在一门研究生入门课程中使用过四次这些（或一些变体）。涵盖的主题包括：ZFC的命题逻辑公理以及AC序数和基数算术的等价物一阶逻辑，以及紧致性定理Lowenheim-Skolem定理图灵机，Church的论文完备性定理和第一不完备性定理不可判定理论第二不完备性定理

1996-01-16math.LO

更多相关论文收起更多论文

Reducing $ω$-model reflection to iterated syntactic reflection

In mathematical logic there are two seemingly distinct kinds of principles called "reflection principles." Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic reflection principles assert that every provable sentence from some complexity class is true. In this paper we study connections between these two kinds of reflection principles in the setting of second-order arithmetic. We prove that, for a large swathe of theories, $ω$-model reflection is equivalent to the claim that arbitrary iterations of uniform $Π^1_1$ r…

2022-06-14math.LO

The Cohomology of the Ordinals I: Basic Theory and Consistency Results

In this paper, the first in a projected two-part series, we describe an organizing framework for the study of infinitary combinatorics. This framework is Čech cohomology. We show in particular that the Čech cohomology groups of the ordinals articulate higher-dimensional generalizations of Todorcevic's walks and coherent sequences techniques, and begin to account for those techniques' `unreasonable effectiveness' on $ω_1$. This discussion occupies the first half of our paper and is written with a general mathematical audience in mind. We turn in the paper's second half to more properly set-theo…

2019-04-15math.ATmath.LO

Proof Theory of Constructive Systems: Inductive Types and Univalence

In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky's univalence axiom. A further goal is to investigate the strength of intuitionistic theories …

2018-01-05math.LO