I examine various claims to the effect that Cantor's Continuum Hypothesis and other problems of higher set theory are ill-posed questions. The analysis takes into account the viability of the underlying philosophical views and recent mathematical developments.

An interview with Charles McCarty by Piotr Urbańczyk concerning mathematical explanation.

In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. Cheney's (...) proof is non-effective in the sense that it is based on classical logic and on the non-computational principle WKL . The result of our analysis provides the first effective uniform modulus of uniqueness . Moreover, the extracted modulus has the optimal ε-dependency as follows from Kroó 331). The paper also describes how the uniform modulus of uniqueness can be used to compute the best L1-approximations of a fixed fC[0,1] with arbitrary precision. The second author uses this result to give a complexity upper bound on the computation of the best L1-approximation in Oliva 66–77). (shrink)

We examine the Dual Ramsey Theorem and two related combinatorial principles VW(k,l) and OVW(k,l) from the perspectives of reverse mathematics and effective mathematics. We give a statement of the Dual Ramsey Theorem for open colorings in second order arithmetic and formalize work of Carlson and Simpson [1] to show that this statement implies ACA 0 over RCA 0 . We show that neither VW(2,2) nor OVW(2,2) is provable in WKL 0 . These results give partial answers to questions posed by (...) Friedman and Simpson [3]. (shrink)

First order reasoning about hyperintegers can prove things about sets of integers. In the author’s paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12 100–125, it was shown that each of the “big five” theories in reverse mathematics, including the base theory , has a natural nonstandard counterpart. But the counterpart of has a defect: it does not imply the Standard Part Principle that a set exists if and only if it is coded by a hyperinteger. In this (...) paper we find another nonstandard counterpart, *RCA0′, that does imply the Standard Part Principle. (shrink)

We show that a version of Ramsey’s theorem for trees for arbitrary exponents is equivalent to the subsystem ${{\sf ACA}^\prime_{0}}$ of reverse mathematics.

In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...) a model of IΣ1. This condition is used to give a model-theoretic proof of Parsons’ theorem, that is, IΣ1 is Π2-conservative over PRA. We shall also give a purely syntactical proof of Parsons’ theorem. Finally, we show that IΣ1 proves the consistency of PRA on a definable IΣ1-cut. This implies that proofs in IΣ1 can have non-elementary speed up over proofs in PRA. (shrink)

In this paper we will investigate different axiomatic theories of truth that are minimal in some sense. One criterion for minimality will be conservativity over Peano Arithmetic. We will then give a more fine-grained characterization by investigating some interpretability relations. We will show that disquotational theories of truth, as well as compositional theories of truth with restricted induction are relatively interpretable in Peano Arithmetic. Furthermore, we will give an example of a theory of truth that is a conservative extension of (...) Peano Arithmetic but not interpretable in it. We will then use stricter versions of interpretations to compare weak theories of truth to subsystems of second-order arithmetic. (shrink)

In his remarkable paper Formalism 64, Robinson defends his eponymous position concerning the foundations of mathematics, as follows:Any mention of infinite totalities is literally meaningless.We should act as if infinite totalities really existed. Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that ‘some infinite totalities are more meaningful than others’, the textbook example being that of infinitesimals. For instance, Bishop and Connes have made such claims regarding infinitesimals, (...) and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate ‘meaning’ and ‘computational content’, though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects in Nonstandard Analysis yields the absence of meaning. We will debunk the Bishop–Connes critique by establishing the contrary, namely that the presence of ideal objects in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation between a large class of theorems of Nonstandard Analysis and theorems rich in computational content, similar to the ‘reversals’ from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation. (shrink)

We present an extension of Heyting arithmetic in finite types called Uniform Heyting Arithmetic that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant (...) of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program. (shrink)

In this paper we introduce theories of universes in analysis. We discuss a non-uniform, a uniform and a minimal variant. An analysis of the proof-theoretic bounds of these systems is given, using only methods of predicative proof-theory. It turns out that all introduced theories are of proof-theoretic strength between Γ0 and ϕ1ɛ00.

We explore the interaction between Lebesgue measure and dominating functions. We show, via both a priority construction and a forcing construction, that there is a function of incomplete degree that dominates almost all degrees. This answers a question of Dobrinen and Simpson, who showed that such functions are related to the proof-theoretic strength of the regularity of Lebesgue measure for Gδ sets. Our constructions essentially settle the reverse mathematical classification of this principle.

In the paper we investigate typed axiomatizations of the truth predicate in which the axioms of truth come with a built-in, minimal and self-sufficient machinery to talk about syntactic aspects of an arbitrary base theory. Expanding previous works of the author and building on recent works of Albert Visser and Richard Heck, we give a precise characterization of these systems by investigating the strict relationships occurring between them, arithmetized model constructions in weak arithmetical systems and suitable set existence axioms. The (...) framework considered will give rise to some methodological remarks on the construction of truth theories and provide us with a privileged point of view to analyze the notion of truth arising from compositional principles in a typed setting. (shrink)

Reductivist programs in logicand philosophy, especially inthe philosophy of mathematics,are reviewed. The paper argues fora ``methodological realism'' towardsnumbers and sets, but still givesreductionism an important place,albeit in methodology/epistemologyrather than in ontology proper.

It is known that infinitely many Medvedev degrees exist inside the Muchnik degree of any nontrivial Π10 subset of Cantor space. We shed light on the fine structures inside these Muchnik degrees related to learnability and piecewise computability. As for nonempty Π10 subsets of Cantor space, we show the existence of a finite-Δ20-piecewise degree containing infinitely many finite-2-piecewise degrees, and a finite-2-piecewise degree containing infinitely many finite-Δ20-piecewise degrees 2 denotes the difference of two Πn0 sets), whereas the greatest degrees in (...) these three “finite-Γ-piecewise” degree structures coincide. Moreover, as for nonempty Π10 subsets of Cantor space, we also show that every nonzero finite-2-piecewise degree includes infinitely many Medvedev degrees, every nonzero countable-Δ20-piecewise degree includes infinitely many finite-piecewise degrees, every nonzero finite-2-countable-Δ20-piecewise degree includes infinitely many countable-Δ20-piecewise degrees, and every nonzero Muchnik degree includes infinitely many finite-2-countable-Δ20-piecewise degrees. Indeed, we show that any nonzero Medvedev degree and nonzero countable-Δ20-piecewise degree of a nonempty Π10 subset of Cantor space have the strong anticupping properties. Finally, we obtain an elementary difference between the Medvedev degree structure and the finite-Γ-piecewise degree structure of all subsets of Baire space by showing that none of the finite-Γ-piecewise structures is Brouwerian, where Γ is any of the Wadge classes mentioned above. (shrink)

We show that a theory of autonomous iterated Ramseyness based on second order arithmetic (SOA) is proof-theoretically equivalent to ${\Pi^1_2}$ -comprehension. The property of Ramsey is defined as follows. Let X be a set of real numbers, i.e. a set of infinite sets of natural numbers. We call a set H of natural numbers homogeneous for X if either all infinite subsets of H are in X or all infinite subsets of H are not in X. X has the property (...) of Ramsey if there exists a set which is homogeneous for X. The property of Ramsey is considered in reverse mathematics to compare the strength of subsystems of SOA. To characterize the system of ${\Pi^1_2}$ -comprehension in terms of Ramseyness we introduce a system of autonomous iterated Ramseyness, called R-calculus. We augment the language of SOA with additional set terms (called R-terms) ${R\vec{x}X\phi(\vec{x},X)}$ for each first order formula ${\phi(\vec{x},X)}$ (where φ may contain further R-terms). The R-calculus is a system which comprises comprehension for all first order formulas (which may contain R-terms or other set parameters) and defining axioms for the R-terms which claim that for each ${\vec{x}}$ , we can remove finitely many elements from the set ${R\vec{x}X\phi(\vec{x},X)}$ such that the remaining set is homogeneous for ${\{{X}{\phi(\vec{x},X)\}}}$ . We show that the R-calculus proves the same ${\Pi^1_1}$ -sentences as the system of ${\Pi^1_2}$ -comprehension. (shrink)

HellmanGeoffrey* * and ShapiroStewart.** ** Varieties of Continua—From Regions to Points and Back. Oxford University Press, 2018. ISBN: 978-0-19-871274-9. Pp. x + 208.

El objetivo de este artículo es analizar qué quiere decir capturar una teoría (se utilizará la aritmética como ejemplo paradigmático) por medio de un sistema axiomático formal. Se considerarán para ello dos enfoques, que pueden denominarse “semántico” y “sintáctico”, tanto en términos de sus ventajas como de sus limitaciones. El enfoque semántico (presupuesto por Barrio y Da Ré en este volumen y expuesto en la primera sección), entiende la expresabilidad como una restricción de la clase de los modelos; se muestra (...) que esta concepción lleva a tres clases distintas de limitaciones expresivas. En la segunda sección se examinan -y finalmente rechazan- algunos posibles caminos de solución a estos problemas. En la última sección se ofrecen objeciones a las alternativas restantes y en base a ellas se elabora el enfoque sintáctico que liga la noción de captura a la de prueba de las oraciones relevantes. También se argumenta que desde este marco pueden evitarse algunas de las limitaciones del enfoque semántico. (shrink)