Search

There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics. [ABSTRACT FROM AUTHOR]

We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice over a preordered set. This manuscript rests in the Oskar-Becker-Nachlass at the Philosophisches Archiv of Universität Konstanz, file OB 5-3b-5. It has probably been written between March and May 1944. We also compare this proof to Gentzen's and Novikov's, and provide a translation of the manuscript. [ABSTRACT FROM AUTHOR]

Let R be a local domain, v a valuation of its quotient field centred in R at its maximal ideal. We investigate the relationship between R h , the henselisation of R as local ring, and v ˜ , the henselisation of the valuation v , by focussing on the recent result by de Felipe and Teissier referred to in the title. We give a new proof that simplifies the original one by using purely algebraic arguments. This proof is moreover constructive in the sense of Bishop and previous work of the authors, and allows us to obtain as a by-product a (slight) generalisation of the theorem by de Felipe and Teissier. [ABSTRACT FROM AUTHOR]

We provide constructive versions of Hilbert's syzygy theorem for Z and Z/NZ following Schreyer's method. Moreover, we extend these results to arbitrary coherent strict Bézout rings with a divisibility test for the case of finitely generated modules whose module of leading terms is finitely generated. [ABSTRACT FROM AUTHOR]

For an m×n matrix A with nonnegative real entries, Atkinson, Moran and Watterson proved the inequality s(A)3⩽mns(AAtA), where At is the transpose of A, and s(·) is the sum of the entries. We extend this result to finite products of the form AAtAAt⋯A or AAtAAt⋯At and give some applications to the theory of iterated kernels. [Copyright &y& Elsevier]