Reverse Mathematics and Recursive Graph Theory

We examine a number of results of infinite combinatorics using the techniques of reverse mathematics. Our results are inspired by similar results in recursive combinatorics. Theorems included concern colorings of graphs and bounded graphs, Euler paths, and Hamilton paths.     

On local non‐compactness in recursive mathematics

A metric space is said to be locally non‐compact if every neighborhood contains a sequence that is eventually bounded away from every element of the space, hence contains no accumulation point. We show within recursive mathematics that a nonvoid complete metric space is locally non‐compact iff it is without isolated points. The result has an interesting consequence in computable analysis: If a complete metric space has a computable witness that it is without isolated points, then every neighborhood contains a computable sequence that is eventually computably bounded away from every computable element of the space. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

N.G. de Bruijn’s contribution to the formalization of mathematics

N.G. (Dick) de Bruijn was the first to develop a formal language suitable for the complete expression of a mathematical subject matter. His formalization does not only regard the usual mathematical expressions, but also all sorts of meta-notions such as definitions, substitutions, theorems and even complete proofs. He envisaged (and demonstrated) that a full formalization enables one to check proofs automatically by means of a computer program. He started developing his ideas about a suitable formal language for mathematics in the end of the 1960s, when computers were still in their infancy. De Bruijn was ahead of his time and much of his work only became known to a wider audience much later. In the present paper we highlight de Bruijn’s contributions to the formalization of mathematics, directed towards verification by a computer, by placing these in their time and by relating them to parallel and later developments. We aim to explain some of the more technical aspects of de Bruijn’s work to a wider audience of interested mathematicians and computer scientists.     

Reverse Mathematics and Ordinal Multiplication

This paper uses the framework of reverse mathematics to analyze the proof theoretic content of several statements concerning multiplication of countable well-orderings. In particular, a division algorithm for ordinal arithmetic is shown to be equivalent to the subsystem ATR ₀.     

Pushouts of Categories,Derived Limits,and Colimits

We provide a counterexample to a theorem of Ford, namely a pushout square of categories with all involved functors injective, such that there is no associated exact “Mayer–Vietoris” sequence of derived limits. Further, we construct a Mayer–Vietoris sequence for derived (co)limits under some additional hypotheses, extending the well-known case of a pushout square of group monomorphisms.     

Two proving strategies of highly successful mathematics majors

We examined the proof-writing behaviors of six highly successful mathematics majors on novel proving tasks in calculus. We found two approaches that these students used to write proofs, which we termed the targeted strategy and the shotgun strategy. When using a targeted strategy students would develop a strong understanding of the statement they were proving, choose a plan based on this understanding, develop a graphical argument for why the statement is true, and formalize this graphical argument into a proof. When using a shotgun strategy, students would begin trying different proof plans immediately after reading the statement and would abandon a plan at the first sign of difficulty. The identification of these two strategies adds to the literature on proving by informing how elements of existing problem-solving models interrelate.     

Variation on a theme of Schütte

Let ? be a primitive recursive well‐ordering on the natural numbers and assume that its order‐type is greater than or equal to the proof‐theoretic ordinal of the theory T. We show that the proof‐theoretic strength of T is not increased if we add the negation of the statement which formalizes transfinite induction along ?. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Decidability and Specker sequences in intuitionistic mathematics

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema (which we call ED ) about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED . We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Pincherle's theorem in reverse mathematics and computability theory

We study the logical and computational properties of basic theorems of uncountable mathematics, in particular Pincherle's theorem, published in 1882. This theorem states that a locally bounded function is bounded on certain domains, i.e. one of the first ‘local-to-global’ principles. It is well-known that such principles in analysis are intimately connected to (open-cover) compactness, but we nonetheless exhibit fundamental differences between compactness and Pincherle's theorem. For instance, the main question of Reverse Mathematics, namely which set existence axioms are necessary to prove Pincherle's theorem, does not have an unique or unambiguous answer, in contrast to compactness. We establish similar differences for the computational properties of compactness and Pincherle's theorem. We establish the same differences for other local-to-global principles, even going back to Weierstrass. We also greatly sharpen the known computational power of compactness, for the most shared with Pincherle's theorem however. Finally, countable choice plays an important role in the previous, we therefore study this axiom together with the intimately related Lindelöf lemma.     

Obstruction Theory for Objects in Abelian and Derived Categories

ABSTRACT

In this article, we develop the obstruction theory for lifting complexes, up to quasi-isomorphism, to derived categories of flat nilpotent deformations of abelian categories. As a particular case we also obtain the corresponding obstruction theory for lifting of objects in terms of Yoneda Ext-groups. In an appendix we prove the existence of miniversal derived deformations of complexes.     

How some research mathematicians and statisticians use proof in undergraduate mathematics

The paper examines the roles and purposes of proof mentioned by university research faculty when reflecting on their own teaching and teaching at their institutions. Interview responses from 14 research mathematicians and statisticians who also teach are reported. The results suggest there is a great deal of variation in the role and purpose of proof in and among mathematics courses and that factors such as the course title, audience, and instructor influence this variation. The results also suggest that, for this diverse group, learning how to prove theorems is the most prominent role of proof in upper division undergraduate mathematics courses and that this training is considered preparation for graduate mathematics studies. Absent were responses discussing proof's role in preparing K-12 mathematics teachers. Implications for a proof and proving landscape for school mathematics are discussed.     

Transfinite sequences of continuous and Baire class 1 functions

The set of continuous or Baire class 1 functions defined on a metric space is endowed with the natural pointwise partial order. We investigate how the possible lengths of well-ordered monotone sequences (with respect to this order) depend on the space .

     

Validating proofs and counterexamples across content domains: Practices of importance for mathematics majors

Validating proofs and counterexamples across content domains is considered vital practices for undergraduate students to advance their mathematical reasoning and knowledge. To date, not enough is known about the ways mathematics majors determine the validity of arguments in the domains of algebra, analysis, geometry, and number theory—the domains that are central to many mathematics courses. This study reported how 16 mathematics majors, including eight specializing in secondary mathematics education, who had completed more proof-based courses than transition-to-proof classes evaluated various arguments. The results suggest that the students use one of the following strategies in proof and counterexample validation: (1) examination of the argument's structure and (2) line-by-line checking with informal deductive reasoning, example-based reasoning, experience-based reasoning, and informal deductive and example-based reasoning. Most students tended to examine all steps of the argument with informal deductive reasoning across various tasks, suggesting that this approach might be problem dependent. Even though all participating students had taken more proof-related mathematics courses, it is surprising that many of them did not recognize global-structure or line-by-line content-based flaws presented in the argument.     

The canonical Ramsey theorem and computability theory

Using the tools of computability theory and reverse mathematics, we study the complexity of two partition theorems, the Canonical Ramsey Theorem of Erdös and Rado, and the Regressive Function Theorem of Kanamori and McAloon. Our main aim is to analyze the complexity of the solutions to computable instances of these problems in terms of the Turing degrees and the arithmetical hierarchy. We succeed in giving a sharp characterization for the Canonical Ramsey Theorem for exponent 2 and for the Regressive Function Theorem for all exponents. These results rely heavily on a new, purely inductive, proof of the Canonical Ramsey Theorem. This study also unearths some interesting relationships between these two partition theorems, Ramsey's Theorem, and König's Lemma.

     

Reverse mathematics of separably closed sets

This paper contains a corrected proof that the statement “every non-empty closed subset of a compact complete separable metric space is separably closed” implies the arithmetical comprehension axiom of reverse mathematics.     

On Derived Equivalences for Selfinjective Algebras

We show that if A is a representation-finite selfinjective Artin algebra, then every P ^? ? K ^b(𝒫 _A ) with Hom _K(Mod?A)(P ^?,P ^?[i]) = 0 for i ≠ 0 and add(P ^?) = add(νP ^?) is a direct summand of a tilting complex, and that if A, B are derived equivalent representation-finite selfinjective Artin algebras, then there exists a sequence of selfinjective Artin algebras A = B ₀, B ₁,…, B _m  = B such that, for any 0 ≤ i < m, B _i+1 is the endomorphism algebra of a tilting complex for B _i of length ≤ 1.     

Minima of initial segments of infinite sequences of reals

Suppose that 〈x_k〉_k∈? is a countable sequence of real numbers. Working in the usual subsystems for reverse mathematics, RCA₀ suffices to prove the existence of a sequence of reals 〈u_k〉_k∈? such that for each k, u_k is the minimum of {x₀, x₁, …, x_k}. However, if we wish to prove the existence of a sequence of integer indices of minima of initial segments of 〈x_k〉_k∈?, the stronger subsystem WKL₀ is required. Following the presentation of these reverse mathematics results, we will derive computability theoretic corollaries and use them to illustrate a distinction between computable analysis and constructive analysis. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Generalized Auslander-Reiten Conjecture and Derived Equivalences

In this note, we prove that the generalized Auslander-Reiten conjecture is preserved under derived equivalences between Artin algebras.