Legal structures may form barriers to, or enablers of, adoption of precision agriculture management with small autonomous agricultural robots. This article develops a conceptual regulatory framework for small autonomous agricultural robots, from a practical, self-contained engineering guide perspective, sufficient to get working research and commercial agricultural roboticists quickly and easily up and running within the law. The article examines the liability framework, or rather lack of it, for agricultural robotics in EU, and their transpositions to UK law, as a case (...) study illustrating general international legal concepts and issues. It examines how the law may provide mitigating effects on the liability regime, and how contracts can be developed between agents within it to enable smooth operation. It covers other legal aspects of operation such as the use of shared communications resources and privacy in the reuse of robot-collected data. Where there are some grey areas in current law, it argues that new proposals could be developed to reform these to promote further innovation and investment in agricultural robots. (shrink)

Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. We show that Euclidean geometry can be developed using only intuitionistic logic. This involves finding “uniform” constructions where normally a case distinction is used. For example, in finding a perpendicular to line L through point p, one usually uses two different constructions, “erecting” a perpendicular when p is on L, and “dropping” a perpendicular when p is not on L, but in (...) constructive geometry, it must be done without a case distinction. Classically, the models of Euclidean geometry are planes over Euclidean fields. We prove a similar theorem for constructive Euclidean geometry, by showing how to define addition and multiplication without a case distinction about the sign of the arguments. With intuitionistic logic, there are two possible definitions of Euclidean fields, which turn out to correspond to different versions of the parallel postulate.We consider three versions of Euclid’s parallel postulate. The two most important are Euclid’s own formulation in his Postulate 5, which says that under certain conditions two lines meet, and Playfair’s axiom, which says there cannot be two distinct parallels to line L through the same point p. These differ in that Euclid 5 makes an existence assertion, while Playfair’s axiom does not. The third variant, which we call the strong parallel postulate, isolates the existence assertion from the geometry: it amounts to Playfair’s axiom plus the principle that two distinct lines that are not parallel do intersect. The first main result of this paper is that Euclid 5 suffices to define coordinates, addition, multiplication, and square roots geometrically.We completely settle the questions about implications between the three versions of the parallel postulate. The strong parallel postulate easily implies Euclid 5, and Euclid 5 also implies the strong parallel postulate, as a corollary of coordinatization and definability of arithmetic. We show that Playfair does not imply Euclid 5, and we also give some other independence results. Our independence proofs are given without discussing the exact choice of the other axioms of geometry; all we need is that one can interpret the geometric axioms in Euclidean field theory. The independence proofs use Kripke models of Euclidean field theories based on carefully constructed rings of real-valued functions. “Field elements” in these models are real-valued functions. (shrink)

Under the assumption that all "rules" are recursive (ECT) the statement $\operatorname{Cont}(N^N,N)$ that all functions from N N to N are continuous becomes equivalent to a statement KLS in the language of arithmetic about "effective operations". Our main result is that KLS is underivable in intuitionistic Zermelo-Fraenkel set theory + ECT. Similar results apply for functions from R to R and from 2 N to N. Such results were known for weaker theories, e.g. HA and HAS. We extend not only (...) the theorem but the method, fp-realizability, to intuitionistic ZF. (shrink)

Western Australia has recently assumed an unaccustomed centrality in the minds of Australian policymakers. The recent resource boom briefly propelled WA to the forefront of national economic affairs. While this proved a relatively short-lived prominence, the emergence of WA at the centre of a putative ‘Indo-Pacific’ region promises to give it a more enduring strategic significance. This paper details how geopolitical and geoeconomic forces have shaped WA’s developmental history, and why they are likely to do so in the future as (...) well. (shrink)

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

We use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.

Brouwer's positions about existence (reality) and truth are examined in the light of ninety years of scientific progress. Relevant results in proof theory, recursion theory, set theory, relativity, and quantum mechanics are used to cast light on the following philosophical questions: What is real, and how do we know it? What does it mean to say a thing exists? Can things exist that we can't know about? Can things exist that we don't know how to find? What does it mean (...) to say something is true? How can we know whether something is true? Can things be true that we can't ever know to be true? (shrink)

One of the more striking, surprising, and optimism-inducing features of the contemporary international system has been the decline of interstate war. The key question for students of international relations and comparative politics is how this happy state of affairs came about. In short, was this a universal phenomenon or did some regions play a more important and pioneering role in bringing about peaceful change? As part of the roundtable “International Institutions and Peaceful Change,” this essay suggests that Western Europe generally (...) and the European Union in particular played pivotal roles in transforming the international system and the behavior of policymakers. This helped to create the material and ideational conditions in which other parts of the world could replicate this experience, making war less likely and peaceful change more feasible. This argument is developed by comparing the experiences of the EU and the Association of Southeast Asian Nations and their respective institutional offshoots. The essay uses this comparative historical analysis to assess both regions’ capacity to cope with new security challenges, particularly the declining confidence in institutionalized cooperation. (shrink)