Pith. sign in

REVIEW 1 cited by

The tree pigeonhole principle in the Weihrauch degrees

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2312.10535 v2 pith:Q375ICYV submitted 2023-12-16 math.LO

classification math.LO
keywords mathsfprinciplepigeonholeanalogueanswerfirst-orderquestiontree
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
abstract

We study versions of the tree pigeonhole principle, $\mathsf{TT}^1$, in the context of Weihrauch-style computable analysis. The principle has previously been the subject of extensive research in reverse mathematics. Two outstanding questions from the latter investigation are whether $\mathsf{TT}^1$ is $\Pi^1_1$-conservative over the ordinary pigeonhole principle, $\mathsf{RT}^1$, and whether it is equivalent to any first-order statement of second-order arithmetic. Using the recently introduced notion of the first-order part of an instance-solution problem, we formulate, and answer in the affirmative, the analogue of the first question for Weihrauch reducibility. We then use this, in combination with other results, to answer in the negative the analogue of the second question. Our proofs develop a new combinatorial machinery for constructing and understanding solutions to instances of $\mathsf{TT}^1$.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Effectiveness and strong graph indivisibility

    math.LO 2024-11 accept novelty 6.0 of 10

    The paper shows Cameron's classification of strongly indivisible graphs is effective up to a change of computable presentation, partially holds in the omega-model REC, and requires the induction scheme I-Sigma-0-2 in ...

Pith tools