A constructive proof of the Cartan-Dieudonné-Scherk Theorem in the real or complex case

The Cartan-Dieudonné-Scherk Theorem states that for fields of characteristic other than 2, every orthogonality can be written as the product of a certain minimal number of reflections across hyperplanes. The earliest proofs are not constructive, and constructive proofs either do not achieve minimal results or have been restricted to special cases. This paper presents a constructive proof in the real or complex field of the decomposition of a generalized orthogonal matrix into the product of the minimal number of generalized Householder matrices.     

Answer set programming in intuitionistic logic

As a demonstration of the flexibility of constructive mathematics, we propose an interpretation of propositional answer set programming (ASP) in terms of intuitionistic proof theory, in particular in terms of simply typed lambda calculus. While connections between ASP and intuitionistic logic are well-known, they usually take the form of characterizations of stable models with the help of some intuitionistic theories represented by specific classes of Kripke models. As such the known results are model-theoretic rather than proof-theoretic. In contrast, we offer an explanation of ASP using constructive proofs.     

Generalizing realizability and Heyting models for constructive set theory

This article presents a common generalization of the two main methods for obtaining class models of constructive set theory. Heyting models are a generalization of the Boolean models for classical set theory which are a variant of forcing, while realizability is a decidedly constructive method that has first been developed for number theory by Kleene and was later very fruitfully adapted to constructive set theory. In order to achieve the generalization, a new kind of structure (applicative topologies) is introduced, which contains both elements of formal topology and applicative structures. This approach not only deepens the understanding of class models and leads to more efficiency in proofs about these kinds of models, but also makes it possible to prove new results about the two special cases that were not known before and to construct new models.     

The continuum as a formal space

A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined. Received: 11 November 1996     

On the formal points of the formal topology of the binary tree

 Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one. Received: 23 May 2000 / Published online: 12 July 2002     

The Morse–Sard Theorem and Luzin N-Property: A New Synthesis for Smooth and Sobolev Mappings

Considering regular mappings of Euclidean spaces, we study the distortion of the Hausdorff dimension of a given set under restrictions on the rank of the gradient on the set. This problem was solved for the classical cases of k-smooth and Hölder mappings by Dubovitskii, Bates, and Moreira. We solve the problem for Sobolev and fractional Sobolev classes as well. Here we study the Sobolev case under minimal integrability assumptions that guarantee in general only the continuity of a mapping (rather than differentiability everywhere). Some new facts are found out in the classical smooth case. The proofs are mostly based on our previous joint papers with Bourgain and Kristensen (2013, 2015).

     

Criteria for modal controllability of linear systems of neutral type

For linear autonomous differential-difference systems of neutral type with commensurable delays, we suggest solvability criteria for the modal controllability problem with the use of two classes of state feedback controllers, namely, controllers of constant and variable structure. The proofs are constructive and permit one to obtain the corresponding controllers with the use of standard operations on polynomials and polynomial matrices.     

Some examples of application of the metric entropy method

We show how the metric entropy method can be substituted for the dyadic chaining, to prove in a unified setting several classical results. Among them are Stechkin's theorem, Gál--Koksma theorems and quantitative Borel--Cantelli lemmas. We give simpler proofs and improve some of these results. Two classes of examples are given: firstly stationary Gaussian sequences with applications to upper and lower classes and the law of the iterated logarithm for subsequences, and secondly in Diophantine approximation relatively to Gál and Schmidt's theorems.     

Bijective proofs of some classical partition identities

A bijective proof of a general partition theorem is given which has as direct corollaries many classical partition theorems due to Euler, Glaisher, Schur, Andrews, Subbarao, and others. It is shown that the bijective proof specializes to give bijective proofs of these classical results and moreover the bijections which result often coincide with bijections which have occurred in the literature. Also given are some sufficient conditions for when two classes of words omitting certain sequences of words are in bijection.     

Turning cycles into spirals

In [13] Parikh proved the first mathematical result about concrete consistency of contradictory theories. In [6] it is shown that the bounds of concrete consistency given by Parikh are optimal. This was proved by noting that very large numbers can be actually constructed through very short proofs. A more refined analysis of these short proofs reveals the presence of cyclic paths in their logical graphs. Indeed, in [6] it is shown that cycles need to exist for the proofs to be short. Here, we present a new sequent calculus for classical logic which is close to linear logic in spirit, enjoys cut-elimination, is acyclic and its proofs are just elementary larger than proofs in LK. The proofs in the new calculus can be obtained by a small perturbation of proofs in LK and they represent a geometrical alternative for studying structural properties of LK-proofs. They satisfy the constructive disjunction property and most important, simpler geometrical properties of their logical graphs. The geometrical counterpart to a cycle in LK is represented in the new setting by a spiral which is passing through sets of formulas logically grouped together by the nesting of their quantifiers.     

The exterior Dirichlet problem for a quasilinear elliptic boundary value problem suggested by plane shear flow

We study the existence of a classical solution of the exterior Dirichlet problem for a class of quasilinear elliptic boundary value problems that are suggested by plane shear flow. In this connection only bounded solutions which tend to zero at infinity are of interest. A priori bounds on solutions and constructive existence proofs are given. Finally, we prove the existence of a unique bounded solution of the shear flow and we show, under certain hypotheses about the asymptotic behavior of the nonlinearity, that this solution tends to zero at infinity. As an example, we consider the case of the parabolic shear flow.     

Balancedness of Sequencing Games with Multiple Parallel Machines

We provide simple constructive proofs of balancedness of classes of m-PS (m-Parallel Sequencing) games, which arise from sequencing situations with m parallel machines. This includes the setting that is studied by Calleja et al. (2001) and Calleja et al. (2002), who provided a complex constructive proof and a simple non-constructive proof of balancedness of a restricted class of 2-PS games, respectively. Furthermore, we provide a counterexample to illustrate that our balancedness results cannot be extended to a general setting.     

On the geometry of conjugacy classes in classical groups

Summary We study closures of conjugacy classes in the Lie algebras of the orthogonal and symplectic groups and determine which ones are normal varieties. Furthermore we give a complete classification of the minimal singularities which arise in this context, i.e. the singularities which occur in the open classes in the boundary of a given conjugacy class. In contrast to the results for the general linear group ([KP1], [KP2]) there are classes with non normal closure; they are branched in a class of codimension two and give rise to normal minimal singularities. The methods used are (classical) invariant theory and algebraic geometry. Supported in part by the SFB Theoretische Mathematik, University of Bonn, and by the University of Hamburg     

Harris-type results on geometric and subgeometric convergence to equilibrium for stochastic semigroups

We provide simple and constructive proofs of Harris-type theorems on the existence and uniqueness of an equilibrium and the speed of equilibration of discrete-time and continuous-time stochastic semigroups. Our results apply both to cases where the relaxation speed is exponential (also called geometric) and to those with no spectral gap, with non-exponential speeds (also called subgeometric). We give constructive estimates in the subgeometric case and discrete-time statements which seem both to be new. The method of proof also differs from previous works, based on semigroup and interpolation arguments, valid for both geometric and subgeometric cases with essentially the same ideas. In particular, we present very simple new proofs of the geometric case.     

Meaning explanations at higher dimension

Martin-Löf’s intuitionistic type theory is a widely-used framework for constructive mathematics and computer programming. In its most popular form, type theory consists of a collection of inference rules inductively defining formal proofs. These rules are justified by Martin-Löf’s meaning explanations, which extend the Brouwer–Heyting–Kolmogorov interpretation of connectives to a rich collection of types, and therefore provide a constructive realizability interpretation of formal proofs.Around 2005, researchers noticed that the rules of type theory also admit homotopy-theoretic models, and subsequently extended type theory with constructs inspired by these models: higher inductive types and Voevodsky’s univalence axiom. Although the resulting homotopy type theory has proved useful for homotopy-theoretic reasoning, it lacks a constructive interpretation. In this overview, we discuss a cubical generalization of the meaning explanations of type theory that constitutes an inherently constructive account of higher-dimensional structure in types.     

Representation of holomorphic functions on coverings of pseudoconvex domains in Stein manifolds via integral formulas on these domains

The classical integral representation formulas for holomorphic functions defined on pseudoconvex domains in Stein manifolds play an important role in the constructive theory of functions of several complex variables. In this paper, we will show how to construct similar formulas for certain classes of holomorphic functions defined on coverings of such domains.     

A constructive characterization of the split closure of a mixed integer linear program

Two independent proofs of the polyhedrality of the split closure of mixed integer linear program have been previously presented. Unfortunately neither of these proofs is constructive. In this paper, we present a constructive version of this proof. We also show that split cuts dominate a family of inequalities introduced by Köppe and Weismantel.     

Pronormal subgroups and homomorphs in finite groups

A local version of the theory of homomorphs and Schunck classes is given. It is shown that for any finite soluble group the pronormal subgroups are precisely the covering subgroups with respect to “Schunck sets” in this group. As an application simple proofs of some results on pronormal subgroups of finite soluble groups are obtained. Finally a question of Doerk is answered in the negative: any finite soluble group is a subgroup of a minimal non-trivial pronormal subgroup of some finite soluble group.     

关于Dini-Lipschitz型逼近定理的统一处理方法方法

This survey paper studies the approximation of (polynomial) processes for which the operator norms do not form a bounded sequence. In view of familiar direct estimates and quantitative uniform boundedness principles, a unified approach is given to results concerning the equivalence of Dini-Lipschitz-type conditions with (strong) convergence on (smoothness) classes. Emphasis is laid upon the necessity of these conditions, essential ingredients of the proofs are suitable modifications of the familiar gliding hump method. Apart from the classical results concerned with Fourier partial sums, explicit applications are treated for (trigonometric as well as algebralc) Lagrange interpolation, interpolatory quadrature rules based upon Jacobl knots, multipliers or strong convergence, and for Bochner-Riesz means of multivariate Fourier series for parameter values below the critical index.