二阶算术子理论的可容许扩张

Interpretations of Presburger Arithmetic in Itself

Presburger arithmetic PrA is the true theory of natural numbers with addition. We study interpretations of PrA in itself. We prove that all one-dimensional self-interpretations are definably isomorphic to the identity self-interpretation. In order to prove the results we show that all linear orders that are interpretable in (N,+) are scattered orders with the finite Hausdorff rank and that the ranks are bounded in terms of the dimension of the respective interpretations. From our result about self-interpretations of PrA it follows that PrA isn't one-dimensionally interpretable in any of its fi…

Constructive Ackermann's interpretation

The main goal of this paper is to formulate a constructive analogue of Ackermann's observation about finite set theory and arithmetic. We will see that Heyting arithmetic is bi-interpretable with $\mathsf{CZF^{fin}}$, the finitary version of $\mathsf{CZF}$. We also examine bi-interpretability between subtheories of finitary $\mathsf{CZF}$ and Heyting arithmetic based on the modification of Fleischmann's hierarchy of formulas, and the set of hereditarily finite sets over $\mathsf{CZF}$, which turns out to be a model of $\mathsf{CZF^{fin}}$ but not a model of finitary $\mathsf{IZF}$.

A weak set theory that proves its own consistency

In the paper we introduce a weak set theory $\mathsf{H}_{<ω}$ . A formalization of arithmetic on finite von Neumann ordinals gives an embedding of arithmetical language into this theory. We show that $\mathsf{H}_{<ω}$ proves a natural arithmetization of its own Hilbert-style consistency. Unlike some previous examples of theories proving their own consistency, $\mathsf{H}_{<ω}$ appears to be sufficiently natural. The theory $\mathsf{H}_{<ω}$ is infinitely axiomatizable and proves existence of all individual hereditarily finite sets, but at the same time all its finite subtheories have finite mo…

Calibrating the negative interpretation

The minimum classical extension S$^{+g}$ of a classically sound theory S based on intuitionistic logic, defined by adding to S the Gentzen negative interpretations of its mathematical axioms, contains a faithful translation S$^g$ of the classical version S + (--A -> A) of S. S$^g$ may be called the classical content of S. First and second order intuitionistic arithmetic contain their classical contents, but intuitionistic recursive analysis cannot prove the negative interpretation of its quantifier-free countable choice axiom. Variants of Kuroda's double negation shift principle (including the…

Harrington's principle over higher order arithmetic

Let $Z_2$, $Z_3$, and $Z_4$ denote $2^{\rm nd}$, $3^{\rm rd}$, and $4^{\rm th}$ order arithmetic, respectively. We let Harrington's Principle, {\sf HP}, denote the statement that there is a real $x$ such that every $x$--admissible ordinal is a cardinal in $L$. The known proofs of Harrington's theorem "$Det(Σ_1^1)$ implies $0^{\sharp}$ exists" are done in two steps: first show that $Det(Σ_1^1)$ implies {\sf HP}, and then show that {\sf HP} implies $0^{\sharp}$ exists. The first step is provable in $Z_2$. In this paper we show that $Z_2 \, + \, {\sf HP}$ is equiconsistent with ${\sf ZFC}$ and th…

力迫构造$Z_3$ + Harrington原理的集合模型

Force a set model of $Z_3$ + Harrington's Principle

本文在存在remarkable基数且其上有弱不可达基数的假设下，通过无需重塑的集合力迫方法，构造了满足三阶算术（$Z_3$）加Harrington原理（HP）的集合模型。