Brown's lemma in second-order arithmetic

TL;DR

This paper explores the logical strength of Brown's lemma within second-order arithmetic, establishing its equivalence to Sigma02-induction over RCA0* and analyzing the provability of its finite version.

Contribution

It demonstrates the equivalence of Brown's lemma to Sigma02-induction over RCA0* and clarifies the provability boundaries of its finite form within subsystems.

Findings

Brown's lemma is equivalent to Sigma02-induction over RCA0*

The finite version of Brown's lemma is provable in RCA0

The finite version is not provable in RCA0*

Abstract

We show that Brown's lemma is equivalent to Sigma02-induction over RCA0* and that the finite version of Brown's lemma is provable in RCA0 but not in RCA0*.