We give an overview of the role of equicontinuity of sequences of real-valued functions on [0,1] and related notions in classical mathematics, intuitionistic mathematics, Bishop’s constructive mathematics, and Russian recursive mathematics. We then study the logical strength of theorems concerning these notions within the programme of Constructive Reverse Mathematics. It appears that many of these theorems, like a version of Ascoli’s Lemma, are equivalent to fan-theoretic principles.

One of the earliest applications of transfinite numbers is in the construction of derived sequences by Cantor [2]. In [6], the existence of derived sequences for countable closed sets is proved in ATR0. This existence theorem is an intermediate step in a proof that a statement concerning topological comparability is equivalent to ATR0. In actuality, the full strength of ATR0 is used in proving the existence theorem. To show this, we will derive a statement known to be equivalent (...) to ATR0, using only RCA0 and the assertion that every countable closed set has a derived sequence. We will use three of the subsystems of second order arithmetic defined by H. Friedman , which can be roughly characterized by the strength of their set comprehension axioms. RCA0 includes comprehension for Δmath image definable sets, ACA0 includes comprehension for arithmetical sets, and ATR0 appends to ACA0 a comprehension scheme for sets defined by transfinite recursion on arithmetical formulas. MSC: 03F35, 54B99. (shrink)

The accurate annotation of an unknown protein sequence depends on extant data of template sequences. This could be empirical or sets of reference sequences, and provides an exhaustive pool of probable functions. Individual methods of predicting dominant function possess shortcomings such as varying degrees of inter-sequence redundancy, arbitrary domain inclusion thresholds, heterogeneous parameterization protocols, and ill-conditioned input channels. Here, I present a rigorous theoretical derivation of various steps of a generic algorithm that integrates and utilizes several statistical methods (...) to predict the dominant function in unknown protein sequences. The accompanying mathematical proofs, interval definitions, analysis, and numerical computations presented are meant to offer insights not only into the specificity and accuracy of predictions, but also provide details of the operatic mechanisms involved in the integration and its ensuing rigor. The algorithm uses numerically modified raw hidden markov model scores of well defined sets of training sequences and clusters them on the basis of known function. The results are then fed into an artificial neural network, the predictions of which can be refined using the available data. This pipeline is trained recursively and can be used to discern the dominant principal function, and thereby, annotate an unknown protein sequence. Whilst, the approach is complex, the specificity of the final predictions can benefit laboratory workers design their experiments with greater confidence. -/- . (shrink)

This paper sketches a way of supplementing classical mathematics with a motivation for a Brouwerian theory of free choice sequences. The idea is that time is unending, i.e. that one can never come to an end of it, but also indeterminate, so that in a branching time model only one branch represents the ‘actual’ one. The branching can be random or subject to various restrictions imposed by the creating subject. The fact that the underlying mathematics is classical (...) makes such perhaps delicate issues as the fan theorem no longer problematic. On this model, only intuitionistic logic applies to the Brouwerian free choice sequences, and there it applies not because of any skepticism about classical mathematics, but because there is no ‘end of time’ from the standpoint of which everything about the sequences can be decided. (shrink)

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 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. (shrink)

This study looks at the relation between mathematical discovery and semiosis, focusing on the famous Fibonacci sequence. The serendipitous discovery of this sequence as the answer to a puzzle designed by Italian mathematician Leonardo Fibonacci to illustrate the efficiency of the decimal number system is one of those episodes in human history which show how serendipity, semiosis, and discovery are intertwined. As such, the sequence has significant implications for the study of creative semiosis, since it suggests that symbols are hardly (...) arbitrary products of human reason, but rather unconscious probes of reality. (shrink)

This study looks at the relation between mathematical discovery and semiosis, focusing on the famous Fibonacci sequence. The serendipitous discovery of this sequence as the answer to a puzzle designed by Italian mathematician Leonardo Fibonacci to illustrate the efficiency of the decimal number system is one of those episodes in human history which show how serendipity, semiosis, and discovery are intertwined. As such, the sequence has significant implications for the study of creative semiosis, since it suggests that symbols are hardly (...) arbitrary products of human reason, but rather unconscious probes of reality. (shrink)

Mathematical logic is a branch of mathematics that takes axiom systems and mathematical proofs as its objects of study. This book shows how it can also provide a foundation for the development of information science and technology. The first five chapters systematically present the core topics of classical mathematical logic, including the syntax and models of first-order languages, formal inference systems, computability and representability, and Gödel’s theorems. The last five chapters present extensions and developments of classical mathematical logic, particularly (...) the concepts of version sequences of formal theories and their limits, the system of revision calculus, proschemes (formal descriptions of proof methods and strategies) and their properties, and the theory of inductive inference. All of these themes contribute to a formal theory of axiomatization and its application to the process of developing information technology and scientific theories. The book also describes the paradigm of three kinds of language environments for theories and it presents the basic properties required of a meta-language environment. Finally, the book brings these themes together by describing a workflow for scientific research in the information era in which formal methods, interactive software and human invention are all used to their advantage. The second edition of the book includes major revisions on the proof of the completeness theorem of the Gentzen system and new contents on the logic of scientific discovery, R-calculus without cut, and the operational semantics of program debugging. This book represents a valuable reference for graduate and undergraduate students and researchers in mathematics, information science and technology, and other relevant areas of natural sciences. Its first five chapters serve as an undergraduate text in mathematical logic and the last five chapters are addressed to graduate students in relevant disciplines. (shrink)

An amendment to this paper has been published and can be accessed via the original article.

Specker sequences are constructive, increasing, bounded sequences of rationals that do not converge to any constructive real. A sequence is said to be a strong Specker sequence if it is Specker and eventually bounded away from every constructive real. Within Bishop's constructive mathematics we investigate non-decreasing, bounded sequences of rationals that eventually avoid sets that are unions of sequences of intervals with rational endpoints. This yields surprisingly straightforward proofs of certain basic results fromconstructive mathematics. (...) Within Russian constructivism, we show how to use this general method to generate Specker sequences. Furthermore, we show that any nonvoid subset of the constructive reals that has no isolated points contains a strictly increasing sequence that is eventually bounded away from every constructive real. If every neighborhood of every point in the subset contains a rational number different from that point, the subset contains a strong Specker sequence. (shrink)

Can the straight line be analysed mathematically such that it does not fall apart into a set of discrete points, as is usually done but through which its fundamental continuity is lost? And are there objects of pure mathematics that can change through time? Mathematician and philosopher L.E.J. Brouwer argued that the two questions are closely related and that the answer to both is "yes''. To this end he introduced a new kind of object into mathematics, the choice (...) sequence. But other mathematicians and philosophers have been voicing objections to choice sequences from the start. This book aims to provide a sound philosophical basis for Brouwer's choice sequences by subjecting them to a phenomenological critique in the style of the later Husserl. (shrink)

Five recursively axiomatizable theories extending Kleene's intuitionistic theory FIM of numbers and numbertheoretic sequences are introduced and shown to be consistent, by a modified relative realizability interpretation which verifies that every sequence classically defined by a Π11 formula is unavoidable and that no sequence can fail to be classically Δ11. The analytical form of Markov's Principle fails under the interpretation. The notion of strongly inadmissible rule of inference is introduced, with examples.

This contribution aims to explore the historical predecessors of the Five Percenter model of self-realization, as popularized by Hip Hop artists such as Supreme Team, Rakim Allah, Brand Nubian, Wu-Tang Clan, or Sunz of Man. As compared to frequent considerations of the phenomenon as a creative mythological background for a socio-political struggle, Five Percenter teachings shall be discussed as contemporary interpretations of historical models of self-realization in various philosophical, religious, and esoteric systems. By putting the coded system of the tenfold (...) Supreme Mathematics as one of its core teachings in context with the Pythagorean Tetractys, an arrangement of ten points in four lines, the commonalities between the sequence and concepts attributed to the respective numbers will be demonstrated. (shrink)

This article discusses Charles Parsons’ conception of mathematical intuition. Intuition, for Parsons, involves seeing-as: in seeing the sequences I I I and I I I as the same type, one intuits the type. The type is abstract, but intuiting the type is supposed to be epistemically analogous to ordinary perception of physical objects. And some non-trivial mathematical knowledge is supposed to be intuitable in this way, again in a way analogous to ordinary perceptual knowledge. In particular, the successor axioms (...) are supposed to be knowable intuitively.This conception has the resources to respond to some familiar objections to mathematical intuition. But the analogy to ordinary perception is weaker than it looks, and the warrant provided for non-trivial mathematical beliefs by intuition of this sort is weak too weak, perhaps, to yield any mathematical knowledge. (shrink)

This article discusses Charles Parsons’ conception of mathematical intuition. Intuition, for Parsons, involves seeing-as: in seeing the sequences I I I and I I I as the same type, one intuits the type. The type is abstract, but intuiting the type is supposed to be epistemically analogous to ordinary perception of physical objects. And some non-trivial mathematical knowledge is supposed to be intuitable in this way, again in a way analogous to ordinary perceptual knowledge. In particular, the successor axioms (...) are supposed to be knowable intuitively.This conception has the resources to respond to some familiar objections to mathematical intuition. But the analogy to ordinary perception is weaker than it looks, and the warrant provided for non-trivial mathematical beliefs by intuition of this sort is weak too weak, perhaps, to yield any mathematical knowledge. (shrink)

This paper studies the metric structure of the space Hr of absolutely summable sequences of real numbers with at most r nonzero terms. Hr is complete, and is located and nowhere dense in the space of all absolutely summable sequences. Totally bounded and compact subspaces of Hr are characterized, and large classes of located, totally bounded, compact, and locally compact subspaces are constructed. The methods used are constructive in the strict sense. MSC: 03F65, 54E50.

We propose a new method for constructing Turing ideals satisfying principles of reverse mathematics below the Chain–Antichain (CAC) Principle. Using this method, we are able to prove several new separations in the presence of Weak König’s Lemma (WKL), including showing that CAC+WKL does not imply the thin set theorem for pairs, and that the principle “the product of well-quasi-orders is a well-quasi-order” is strictly between CAC and the Ascending/Descending Sequences principle, even in the presence of WKL.

We investigate maximal free sequences in the Boolean algebra \ {/}\text {fin}\), as defined by Monk :593–610, 2011). We provide some information on the general structure of these objects and we are particularly interested in the minimal cardinality of a free sequence, a cardinal characteristic of the continuum denoted \. Answering a question of Monk, we demonstrate the consistency of \. In fact, this consistency is demonstrated in the model of Shelah for \ :433–443, 1992). Our paper provides a (...) streamlined and mostly self contained presentation of this construction. (shrink)

We investigate maximal free sequences in the Boolean algebra \ {/}\text {fin}\), as defined by Monk :593–610, 2011). We provide some information on the general structure of these objects and we are particularly interested in the minimal cardinality of a free sequence, a cardinal characteristic of the continuum denoted \. Answering a question of Monk, we demonstrate the consistency of \. In fact, this consistency is demonstrated in the model of Shelah for \ :433–443, 1992). Our paper provides a (...) streamlined and mostly self contained presentation of this construction. (shrink)

We investigate maximal free sequences in the Boolean algebra \ {/}\text {fin}\), as defined by Monk :593–610, 2011). We provide some information on the general structure of these objects and we are particularly interested in the minimal cardinality of a free sequence, a cardinal characteristic of the continuum denoted \. Answering a question of Monk, we demonstrate the consistency of \. In fact, this consistency is demonstrated in the model of Shelah for \ :433–443, 1992). Our paper provides a (...) streamlined and mostly self contained presentation of this construction. (shrink)

Revision sequences are a kind of transfinite sequences which were introduced by Herzberger and Gupta in 1982 as the main mathematical tool for developing their respective revision theories of truth. We generalise revision sequences to the notion of cofinally invariant sequences, showing that several known facts about Herzberger’s and Gupta’s theories also hold for this more abstract kind of sequences and providing new and more informative proofs of the old results.

We present a new proof of the existence of Morley sequences in simple theories. We avoid using the Erdős–Rado theorem and instead use only Ramsey’s theorem and compactness. The proof shows that the basic theory of forking in simple theories can be developed using only principles from “ordinary mathematics,” answering a question of Grossberg, Iovino, and Lessmann, as well as a question of Baldwin.

We prove James's sequential characterization of reflexivity in set-theory ZF + DC, where DC is the axiom of Dependent Choices. In turn, James's criterion implies that every infinite set is Dedekind-infinite, whence it is not provable in ZF. Our proof in ZF + DC of James' criterion leads us to various notions of reflexivity which are equivalent in ZFC but are not equivalent in ZF. We also show that the weak compactness of the closed unit ball of a reflexive space (...) does not imply the Boolean Prime Ideal theorem : this solves a question raised in [6]. (shrink)

This paper outlines a logical representation of certain aspects of the process of mathematical proving that are important from the point of view of Artificial Intelligence. Our starting point is the concept of proof-event or proving, introduced by Goguen, instead of the traditional concept of mathematical proof. The reason behind this choice is that in contrast to the traditional static concept of mathematical proof, proof-events are understood as processes, which enables their use in Artificial Intelligence in such contexts in which (...) problem-solving procedures and strategies are studied. We represent proof-events as problem-centred spatio-temporal processes by means of the language of the calculus of events, which adequately captures certain temporal aspects of proof-events (i.e. that they have history and form sequences of proof-events evolving in time). Further, we suggest a “loose” semantics for the proof events by means of Kolmogorov’s calculus of problems. Finally, we expose the intented interpretations for our logical model from the fields of automated theorem-proving and Web-based collective proving. (shrink)

It is shown that, relative to Bishop-style constructive mathematics, the boundedness principle BD-N is equivalent both to a general result about the convergence of double sequences and to a particular one about Cauchyness in a semi-metric space.

Investigation into the sequence structure of the genetic code by means of an informatic approach is a real success story. The features of human language are also the object of investigation within the realm of formal language theories. They focus on the common rules of a universal grammar that lies behind all languages and determine generation of syntactic structures. This universal grammar is a depiction of material reality, i.e., the hidden logical order of things and its relations determined by natural (...) laws. Therefore mathematics is viewed not only as an appropriate tool to investigate human language and genetic code structures through computer sciencebased formal language theory but is itself a depiction of material reality. This confusion between language as a scientific tool to describe observations/experiences within cognitive constructed models and formal language as a direct depiction of material reality occurs not only in current approaches but was the central focus of the philosophy of science debate in the twentieth century, with rather unexpected results. This article recalls these results and their implications for more recent mathematical approaches that also attempt to explain the evolution of human language. (shrink)

We show that the universally axiomatized, induction-free theory equation image is a sequential theory in the sense of Pudlák's 5, in contrast to the closely related Robinson's arithmetic.

A biologically unavoidable sequence is an infinite gender sequence which occurs in every gendered, infinite genealogical network satisfying certain tame conditions. We show that every eventually periodic sequence is biologically unavoidable (this generalizes König's Lemma), and we exhibit some biologically avoidable sequences. Finally we give an application of unavoidable sequences to cellular automata.

Sequences play a great role in mathematical communication. In mathematical notation, we use sequence ellipsis (. . . ) to denote "obvious" sequences like 1, 2, . . . , 7, and in conceptualizations sequence constructors like (i 2+1) i∈N. Furthermore, sequences have a prominent role as argument sequences of flexary functions. While the former cases can adequately be represented and reasoned about as domain objects in Open- Math and MathML, argument sequences are at the (...) language level, and can only be represented, but not reasoned with, since the necessary (sequence-schematic) axioms cannot be represented in the language. (shrink)

The classical theory of definitions bans so-called circular definitions, namely, definitions of a unary predicate P, based on stipulations of the form $$Px =_{\mathsf {Df}} \phi,$$where ϕ is a formula of a fixed first-order language and the definiendumP occurs into the definiensϕ. In their seminal book The Revision Theory of Truth, Gupta and Belnap claim that “General theories of definitions are possible within which circular definitions [...] make logical and semantic sense” [p. IX]. In order to sustain their claim, they (...) develop in this book one general theory of definitions based on revision sequences, namely, ordinal-length iterations of the operator which is induced by the definition of the predicate. Gupta-Belnap’s approach to circular definitions has been criticised, among others, by D. Martin and V. McGee. Their criticisms point to the logical complexity of revision sequences, to their relations with ordinary mathematical practice, and to their merits relative to alternative approaches. I will present an alternative general theory of definitions, based on a combination of supervaluation and ω-length revision, which aims to address some criticisms raised against revision sequences, while preserving the philosophical and mathematical core of revision. (shrink)

The generative and governing "idea" of radical modernity is spawned by the technique of mathematical construction deployed and interpreted by the major early-modern thinkers and their legatees. ;Chapter I is a survey of this legacy as it appears in Vico, Kant, Fichte, Marx and Nietzsche and in the post-Nietzschean inheritance of contemporary philosophy, hyperbolic in the case of Derrida et al., elliptical, in the case of Carnap and Goodman. ;In Chapter II I try to show how the pre-modern mathematical tradition, (...) represented by Euclid, aimed at keeping the enticements of technical facility in check by means of didactic phronesis and how the post-Kantian interpretation of "existence" in Euclid as constructibility betrays his usage and self-understanding. I suggest that his focus in the postulates and elsewhere is on the undistorted iterability of graphic evocations of the items already intelligible thanks to the definitions or to the pre-understanding shared by the teacher and student. ;In Chapter III, devoted to Descartes the principal claims of modern constructivism are brought to sight. After examining Descartes' fabulous autobiography and its emphasis on self-origination, I turn to the style, contents and under-pinnings of the Geometry in an effort to extract from that text what he once referred to as "the metaphysics of geometry." The latter yields the conditions of successful problem-solving, i.e., dimensional homogeneity and kinematic continuity. These conditions, in turn, find their justification in Descartes' theses in the Rules concerning order, measure and the uniformity of "mental" activity. In the final section I apply the lessons learned from the Geometry and the Rules to one critical issue in the later Meditations, the transition from essence to existence. Descartes' "solution" generates a sequence of perplexities with Hobbes, Leibniz, Kant and other radical moderns continue to wrestle. (shrink)