BZPEERSource author record
Explore this author’s publications, collaborators and research topics. This catalog record has not been claimed by its author.
Catalog footprint
Published work
We show that RT(2,4) cannot be proved with one typical application of RT(2,2) in an intuitionistic extension of RCA0 to higher types, but that this does not remain true when the law of the excluded middle is added. The argument uses Kohlenbach's axiomatization of higher order reverse mathematics, results related to modified reducibility, and a formalization of Weihrauch reducibility.
Matroids generalize the familiar notion of linear dependence from linear algebra. Following a brief discussion of founding work in computability and matroids, we use the techniques of reverse mathematics to determine the logical strength of some basis theorems for matroids and enumerated matroids. Next, using Weihrauch reducibility, we relate the basis results to combinatorial choice principles and statements about vector spaces. Finally, we formalize some of the Weihrauch reductions to extract related reverse mathematics results. In particular, we show that the existence of bases for vector spaces of bounded dimension is equivalent to the induction scheme for Σ20 formulas.
We prove that the statement "there is a k such that for every f there is a k-bounded diagonally non-recursive function relative to f" does not imply weak König's lemma over RCA0+BΣ20. This answers a question posed by Simpson. A recursion-theoretic consequence is that the classic fact that every k-bounded diagonally non-recursive function computes a 2-bounded diagonally non-recursive function may fail in the absence of IΣ20.
We study the reverse mathematics and computability of countable graph theory, obtaining the following results. The principle that every countable graph has a connected component is equivalent to ACA0 over RCA0. The problem of decomposing a countable graph into connected components is strongly Weihrauch equivalent to the problem of finding a single component, and each is equivalent to its infinite parallelization. For graphs with finitely many connected components, the existence of a connected component is either provable in RCA0 or is equivalent to induction for Σ20 formulas, depending on the formulation of the bound on the number of components.
The enterprise of comparing mathematical theorems according to their logical strength is an active area in mathematical logic. In this setting, called reverse mathematics, one investigates which theorems provably imply which others in a weak formal theory roughly corresponding to computable mathematics. Since the proofs of such implications take place in classical logic, they may in principle involve appeals to multiple applications of a particular theorem, or to non-uniform decisions about how to proceed in a given construction. In practice, however, if a theorem Q implies a theorem P, it is usually because there is a direct uniform translation of the problems represented by P into the problems represented by Q, in a precise sense. We study this notion of uniform reducibility in the context of several natural combinatorial problems, and compare and contrast it with the traditional notion of implication in reverse mathematics. We show, for instance, that for all n,j,k≥1, if j<k then Ramsey's theorem for n-tuples and k many colors does not uniformly reduce to Ramsey's theorem for j many colors. The two theorems are classically equivalent, so our analysis gives a genuinely finer metric by which to gauge the relative strength of mathematical propositions. We also study Weak König's Lemma, the Thin Set Theorem, and the Rainbow Ramsey's Theorem, along with a number of their variants investigated in the literature. Uniform reducibility turns out to be connected with sequential forms of mathematical principles, where one wishes to solve infinitely many instances of a particular problem simultaneously. We exploit this connection to uncover new points of difference between combinatorial problems previously thought to be more closely related.
We present some results about generics for computable Mathias forcing. The n-generics and weak n-generics in this setting form a strict hierarchy as in the case of Cohen forcing. We analyze the complexity of the Mathias forcing relation, and show that if G is any n-generic with n≥3 then it satisfies the jump property G(n−1)=G′⊕∅(n). We prove that every such G has generalized high degree, and so cannot have even Cohen 1-generic degree. On the other hand, we show that G, together with any bi-immune set A≤T∅(n−1), computes a Cohen n-generic set.
We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a Π21 sentence of a certain form is provable using E-HAω along with the axiom of choice and an independence of premise principle, the sequential form of the statement is provable in the classical system RCA. We obtain this and similar results using applications of modified realizability and the \textit{Dialectica} interpretation. These results allow us to use techniques of classical reverse mathematics to demonstrate the unprovability of several mathematical principles in subsystems of constructive analysis.
We show that a version of Ramsey's theorem for trees for arbitrary exponents is equivalent to the subsystem ACA' of reverse mathematics.
Research graph
Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.
BZPEER is loading the nearby papers, people, topics and institutions for this page.