Harrington's principle over higher order arithmetic

TL;DR

This paper investigates Harrington's Principle in higher order arithmetic, establishing its consistency strength and its relation to the existence of remarkable cardinals and $0^{ atural}$, revealing differences across second, third, and fourth order systems.

Contribution

It shows that Harrington's Principle over second and third order arithmetic has the same consistency strength as ZFC and ZFC plus a remarkable cardinal, respectively, clarifying its logical strength.

Findings

$Z_2 + HP$ is equiconsistent with ZFC.

$Z_3 + HP$ is equiconsistent with ZFC plus a remarkable cardinal.

$Z_4 + HP$ implies the existence of $0^{ atural}$.

Abstract

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(\Sigma_1^1)$ implies $0^{\sharp}$ exists" are done in two steps: first show that $Det(\Sigma_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 that $Z_3\, + \, {\sf HP}$ is equiconsistent with ${\sf ZFC} \, +$ there exists a remarkable cardinal. As a corollary, $Z_3\, + \, {\sf HP}$ does not imply $0^{\sharp}$ exists, whereas $Z_4\, + \, {\sf HP}$ does. We also study strengthenings of Harrington's Principle over $2^{\rm nd}$ and $3^{\rm rd}$ order arithmetic.