Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...) remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF. (shrink)

South Africa’s groundbreaking constitution explicitly confers a right of access to sufficient water. But the country is officially ‘water-stressed’ and around 10 % of the population still has no access to on-site or off-site piped or tap water. It is evident that a disconnect exists between this right and the reality for many; however the reasons for the continuation of such discrepancies are not always clear. While barriers to sufficient water are myriad, one significant factor contributing to insufficient and unpredictable (...) access to water is the high percentage of broken water pumps. Previous studies have reported that between 20 and 50 % of all hand operated water pumps installed on the African continent are broken, or out of use. Monitoring and maintenance of pumps, which in South Africa is the responsibility of local municipalities is often ineffective, in part due to the distances between municipal centres and rural communities and the consequent costs of site visits, as well as breakdowns within the local bureaucratic system. The emergence of new telemetry tools that can remotely monitor water applications constitutes a novel and cost-efficient alternative to undertaking regular sites visits. Sustainable, appropriate, low-cost telemetry systems are emerging that could be used to monitor the operational performance of water pumps, or a wide range of other field parameters, and to communicate this information swiftly and cheaply to water service providers, using SMS messages. Data on the performance of water pumps could also be made available to the public online. This is an example of how ICT can be used for water resources management and environmental regulation, as well as in the governance of socio-economic rights: helping to optimize water allocation by improving communication and strengthening accountability. (shrink)

We develop a number of variants of Lifschitz realizability for $\mathbf {CZF}$ by building topological models internally in certain realizability models. We use this to show some interesting metamathematical results about constructive set theory with variants of the lesser limited principle of omniscience including consistency with unique Church’s thesis, consistency with some Brouwerian principles and variants of the numerical existence property.

We define a class of higher inductive types that can be constructed in the category of sets under the assumptions of Zermelo‐Fraenkel set theory without the axiom of choice or the existence of uncountable regular cardinals. This class includes the example of unordered trees of any arity.