1,721,007 research outputs found
Algebras of Complemented Subsets
No full textComplemented subsets were introduced by Bishop, in order to avoid complementation in terms of negation. In his two approaches to measure theory Bishop used two sets of operations on complemented subsets. Here we study these two algebras and we introduce the notion of Bishop algebra as an abstraction of their common structure. We translate constructively the classical bijection between subsets and boolean-valued functions by establishing a bijection between the proper classes of complemented subsets and of strongly extensional, boolean-valued, partial functions. Avoiding negatively defined concepts, most of our results are within minimal logic
Cut elimination for entailment relations
No full textEntailment relations, introduced by Scott in the early 1970s, provide an abstract gen- eralisation of Gentzen’s multi-conclusion logical inference. Originally applied to the study of multi-valued logics, this notion has then found plenty of applications, ranging from computer science to abstract algebra. In particular, an entailment relation can be regarded as a constructive presentation of a distributive lattice and in this guise it has proven to be a useful tool for the constructive reformulation of several classical theorems in commutative algebra. In this paper, motivated by these concrete applica- tions, we state and prove a cut-elimination result for inductively generated entailment relations. We analyse some of its consequences and describe the existing connections with analogous results in the literature
Radical theory of Scott-open filters
Full text linkFollowing the Kronecker–Duval or D5 philosophy of dynamic evaluation in computer algebra, the dynamical proof method was brought into constructive algebra in order to obtain computational interpretations of the individual, concrete instances of the Kuratowski–Zorn Lemma modern algebra abounds with. We now push this approach into complete lattices, and thus capture the computational content also of generic, abstract forms of the axiom of choice such as the Teichmüller–Tukey lemma. To this end we first strengthen the (key lemma for) the Hofmann–Mislove theorem about Scott-open filters (SOF): to be a member of a SOF is equivalent, with the axiom of choice, to membership of all complete extensions. This then allows for a constructive treatment: membership of the given SOF means that from the potential element one can grow a finite labelled binary tree of an inductively defined type such that every branch of the tree eventually dips into the SOF. The ideal objects characteristic for invocations of the Kuratowski–Zorn Lemma are thus approximated and actually replaced by paths in those trees, by whic h we shed light on the interaction of transfinite methods and their dynamical interpretation. The first test case includes abstract dependence, especially bases of vector spaces. Key to the above lies in taking Erné's saturation map as a radical operator for Scott-open sets. Through a generalised inductive definition this radical can be pinned down in terms of universal properties; and reaches into classical pointfree topology, as exemplified by a succinct proof of Isbell's spatiality theorem
Complemented subsets and Boolean-valued, partial functions
No full textWe study the two algebras of complemented subsets that were introduced in the constructive development of the Daniell approach to measure and integration within Bishop-style constructive mathematics. We present their main properties both for the so-called here categorical complemented subsets and for the extensional complemented subsets. We translate constructively the classical bijection between subsets and Boolean-valued, total functions by establishing a bijection between complemented subsets (categorical or extensional) and Boolean-valued, partial functions (categorical or extensional). The role of Myhill's axiom of non-choice in the equivalence between categorical and extensional subsets is discussed. We introduce swap algebras of type (I) and (II) as an abstract version of Bishop’s algebras of complemented subsets of type (I) and (II), respectively, and swap rings as an abstract version of the structure of Boolean-valued partial functions on a set. Our examples of swap algebras and swap rings together with the included here results indicate that their theory is a certain generalisation of the theory of Boolean algebras and Boolean rings, a fact which we find interesting both from a constructive and a classical point of view
Boolean rigs
No full textSemirings of partial Boolean-valued functions arise in Bishop's approach to constructive measure theory. In this paper, we treat such semirings axiomatically. Lifting the corresponding result for Boolean rings, we prove a representation theorem a la Stone that aligns with the intended semantics. Moreover, among the semirings at hand, we determine the order of those that are free over finitely many generators
Dynamic evaluation of integrity and the computational content of Krull's lemma
Full text linkA multiplicative subset of a commutative ring contains the zero element precisely if the set in question meets every prime ideal. While this form of Krull’s Lemma takes recourse to transfinite reasoning, it has recently allowed for a crucial reduction to the integral case in Kemper and the third author’s novel characterization of the valuative dimension. We present a dynamical solution by which transfinite reasoning can be avoided, and illustrate this constructive method with concrete examples. We further give a combinatorial explanation by relating the Zariski lattice to a certain inductively generated class of finite binary trees. In particular, we make explicit the computational content of Krull’s Lemma
Some forms of excluded middle for linear orders
No full textThe intersection of a linearly ordered set of total subrelations of a total relation with range 2 need not be total, constructively
Syntax for Semantics: Krull’s Maximal Ideal Theorem
No full textPaul Lorenzen -- Mathematician and Logicia
The Jacobson radical for an inconsistency predicate
Full text linkAs a form of the Axiom of Choice about relatively simple structures (posets), Hausdorff's Maximal Chain Principle appears to be little amenable to computational interpretation. This received view, however, requires revision: maximal chains are more reminiscent of maximal ideals than it seems at first glance. The latter live in richer algebraic structures (rings), and thus are readier to be put under computational scrutiny. Exploiting this, and of course the analogy between maximal chains and maximal ideals, the concept of Jacobson radical carries over from a ring to an arbitrary set with an abstract inconsistency predicate: that is, a distinguished monotone family of finite subsets. All this makes possible not only to generalise Hausdorff's principle, but also to express it as a syntactical conservation theorem. The latter, which encompasses the desired computational core of Hausdorff's principle, is obtained by a generalised inductive definition. The over-all setting is constructive set theory
The Jacobson Radical of a Propositional Theory
Full text linkAlongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum's Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko's Theorem. The Jacobson radical in fact turns out to coincide with the classical deductive closure. As a by-product we obtain a possible interpretation in logic of the axioms-as-rules conservation criterion for a multi-conclusion Scott-style entailment relation over a single-conclusion one
- …
