Search

Persistent homology is one of the most active branches of computational algebraic topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this article, we report on the formal development of certified programs to compute persistent Betti numbers , an instrumental tool of persistent homology, using the C oq proof assistant together with the SSR eflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.

We present a proof of Goodman's Theorem, which is a variation of the proof of Renaldel de Lavalette.

For most purposes, one can replace the use of Rolle's theore m and the mean value theorem, which are not constructively valid, by the law of bounded change (3). The proof of two basic results in numerical analysis, the e rror term for Lagrange interpolation and Simpson's rule, however see m to require the full strength of the classical Rolle's Theorem. The goal of this n ote is to justify these two results constructively, using ideas going back to Amp` (1) and Genocchi (6). 2000 Mathematics Subject Classification03F60; 65D30 (primary)

We associate with any game G another game, which is a variant of it, and which we call bck(G). Winning strategies for bck(G) have a lower recursive degree than winning strategies for G: if a player has a winning strategy of recursive degree 1 over G, then it has a recursive winning strategy over bck(G), and vice versa. Through bck(G) we can express in algorithmic form, as a recursive winning strategy, many (but not all) common proofs of non-constructive Mathematics, namely exactly the theorems of the sub-classical logic Limit Computable Mathematics (Hayashi (2006) [6], Hayashi and Nakata (2001) [7]). (C) 2010 Elsevier B.V. All rights reserved.

The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 (1–3) (2003) 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev (Ed.), Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents a topological space, not as a set of points, but as a logical theory which describes the lattice of open sets. The application to Hilbert’s program is then the following. Hilbert’s ideal objects are represented by points of such a formal space. There are general methods to “eliminate” the use of points, close to the notion of forcing and to the “elimination of choice sequences” in intuitionist mathematics, which correspond to Hilbert’s required elimination of ideal objects. This paper illustrates further this general program on the notion of valuations. They were introduced by Dedekind and Weber [R. Dedekind, H. Weber, Theorie des algebraischen Funktionen einer Veranderlichen, J. de Crelle t. XCII (1882) 181–290] to give a rigorous presentation of Riemann surfaces. It can be argued that it is one of the first example in mathematics of point-free representation of spaces [N. Bourbaki, Elements de Mathematique. Algebre commutative, Hermann, Paris, 1965, Chapitre 7]. It is thus of historical and conceptual interest to be able to represent this notion in formal topology.

Is it possible to give an abstract characterisation of constructive real numbers? A condition should be that all axioms are valid for Dedekind reals in any topos, or for constructive reals in Bishop mathematics. We present here a possible first-order axiomatisation of real numbers, which becomes complete if one adds the law of excluded middle. As an application of the forcing relation defined in [3, 2], we give a proof that the formula which specifies the maximum function is not provable in this theory. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

We present a new and constructive proof of the Peter-Weyl theorem on the representations of compact groups. We use the Gelfand representation theorem for commu- tative C*-algebras to give a proof which may be seen as a direct generalization of Burnside's algorithm (3). This algorithm computes the characters of a finite group. We use this proof as a basis for a constructive proof in the style of Bishop. In fact, the present theory of com- pact groups may be seen as a natural continuation in the line of Bishop's work on locally compact, but Abelian, groups (2).

A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajn’s theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.

This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive way by an initiality condition. We then use our work to define in a purely inductive way the measure of Borel subsets.

The completeness proof for first-order logic by Rasiowa and Sikorski [13] is a simplification of Henkin's proof [7] in that it avoids the addition of infinitely many new individual constants. Instead they show that each consistent set of formulae can be extended to a maximally consistent set, satisfying the following existence property: if it contains (∃x)ϕit also contains some substitutionϕ(y/x) of a variableyforx. In Feferman's review [5] of [13], an improvement, due to Tarski, is given by which the proof gets a simple algebraic form.Sambin [16] used the same method in the setting of formal topology [15], thereby obtaining a constructive completeness proof. This proof is elementary and can be seen as a constructive and predicative version of the one in Feferman's review. It is a typical, and simple, example where the use of formal topology gives constructive sense to the existence of a generic object, satisfying some forcing conditions; in this case an ultrafilter satisfying the existence property.In order to get a formal topology on the set of first-order formulae, Sambin used the Dedekind-MacNeille completion to define a covering relation ⊲DM. This method, by which an arbitrary poset can be extended to a complete poset, was introduced by MacNeille [9] and is a generalization of the construction of real numbers from rationals by Dedekind cuts. It is also possible to define an inductive cover, ⊲I, on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].

The effort in providing constructive and predicative meaning to non-constructive modes of reasoning has almost without exception been applied to theories with full classical logic [4]. In this paper we show how to combine unrestricted countable choice, induction on infinite well-founded trees and restricted classical logic in constructively given models. These models are sheaf models over a $\sigma$ -complete Boolean algebra, whose topologies are generated by finite or countable covering relations. By a judicious choice of the Boolean algebra we can directly extract effective content from $\Pi_2^0$ -statements true in the model. All the arguments of the present paper can be formalised in Martin-Lof's constructive type theory with generalised inductive definitions.

We introduce the notion of Boolean measure algebra. It can be described shortly using some standard notations and terminology. If B is any Boolean algebra, let BN denote the algebra of sequences (xn), xn ∈ B. Let us write pk ∈ BN the sequence such that pk(i) = 1 if i ⩽ K and Pk(i) = 0 if k x ∗ ∈ B N the constant sequence x ∗ = (x,x,x,…) . We define a Boolean measure algebra to be a Boolean algebra B with an operation μ:BN → B such that μ(pk) = 0 and μ(x ∗ ) = x . Any Boolean measure algebra can be used to model non-principal ultrafilters in a suitable sense. Also, we can build effectively the initial Boolean measure algebra. This construction is related to the closed open Ramsey Theorem (J. Symbolic Logic 38 (1973) 193–198.)

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem.

A standard result in topological dynamics is the existence of minimal subsystem. It is a direct consequence of Zorn's lemma: given a compact topological space X with a map f: X→X, the set of compact non empty subspaces K of X such that f(K) ⊆ K ordered by inclusion is inductive, and hence has minimal elements. It is natural to ask for a point-free (or formal) formulation of this statement. In a previous work [3], we gave such a formulation for a quite special instance of this statement, which is used in proving a purely combinatorial theorem (van de Waerden's theorem on arithmetical progression).In this paper, we extend our analysis to the case where X is a boolean space, that is compact totally disconnected. In such a case, we give a point-free formulation of the existence of a minimal subspace for any continuous map f: X→X. We show that such minimal subspaces can be described as points of a suitable formal topology, and the “existence” of such points become the problem of the consistency of the theory describing a generic point of this space. We show the consistency of this theory by building effectively and algebraically a topological model. As an application, we get a new, purely algebraic proof, of the minimal property of [3]. We show then in detail how this property can be used to give a proof of (a special case of) van der Waerden's theorem on arithmetical progression, that is “similar in structure” to the topological proof [6, 8], but which uses a simple algebraic remark (Proposition 1) instead of Zorn's lemma. A last section tries to place this work in a wider context, as a reformulation of Hilbert's method of introduction/elimination of ideal elements.

If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: “Thus propositions of actualist mathematics seem to have a certain utility, but no sense. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense to actualist propositions.” From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a “finitist sense” to classical propositions.In this paper, we reformulate Gentzen's and Novikoff's “finitist sense” of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the “finitist sense” of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that “internal chatters” between two programs end eventually.We first present Novikoff's notion of regular formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.

A point-free formulation of the K¨ onig Lemma for trees with uniformly at most one infinite path allows for a constructive proof without unique choice. 2000 Mathematics Subject Classification: 03E25, 03F65 (primary); 05C05, 05C38, 05C63 (secondary)

We present a way to organize a constructive development of the theory of Banach algebras, inspired by works of Cohen, de Bruijn and Bishop. We illustrate this by giving elementary proofs of Wiener's result on the inverse of Fourier series and Wiener's Tauberian Theorem, in a sequel to this paper we show how this can be used in a localic, or point-free, description of the spectrum of a Banach algebra.

Tychonoff's theorem states that a product of compact spaces is compact. In [3], P. Johnstone presents a proof of Tychonoff's theorem in a “localic” framework. The surprise is that the point-free formulation of Tychonoff's theorem is provable without the axiom of choice, whereas in the usual formulation it is equivalent to the axiom of choice (see Kelley [5]).The proof given in [3], however, is classical and seems to use the replacement axiom of Zermelo-Fraenkel. The aim of this paper is to present what we believe to be a more direct proof, which is intuitionistic and can be proved using as primitive only the notion of inductive definition, as it is for instance presented in Martin-Löf [6]. One main point of the paper is to show that the theory of locales can be developed rather naturally in the framework of inductive definitions. We think that our arguments can be presented in the constructive set theory of Aczel [2].The paper is organized as follows. In §1 we show the argument in the case of a product of two spaces. This proof has a direct generalisation to the case of a product over a set with a decidable equality.§1. Product of two spaces. We first recall a possible definition of a point-free space (see Johnstone [3] or Vickers [10]). It is a poset (X, ≤), together with a meet operation ab, written multiplicatively, and, for each a ∈ X, a set Cov(a) of subsets of {x ∈ X ∣ x ≤ a}. We ask that if M ∈ Cov(a) and b ≤ a, then {bs ∈ s ∈ M} ∈ Cov(b). This property of Cov will be called the axiom of covering. The elements of Cov(u) are called basic covers of u ∈ X.

We construct a homeomorphism between the compact regular locale of integrals on a Riesz space and the locale of (valuations) on its spectrum. In fact, we construct two geometric theories and show that they are biinterpretable. The constructions are elementary and tightly connected to the Riesz space structure., Comment: Submitted for publication 15/05/08

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology.Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined.