The equivalence of Side-Angle-Side with Side-Side-Side and the general triangle inequality in the absolute plane

We show that if we start with an absolute plane, remove Side-Angle-Side as an axiom, and replace it with Side-Side-Side together with a weakened version of the triangle inequality as new axioms, then the new resulting axiom system is also an absolute plane. In particular, we show that Side-Angle-Side still holds in the new axiom system. In addition, we give a new proof of the two-circle theorem which does not depend on Side-Angle-Side, but instead uses Side-Side-Side and the weakened version of the triangle inequality.     

A proposal for a variation on the axioms of classical geometry

A set of axioms for classical absolute geometry is proposed that is accessible to students new to axioms. The metric axioms adopted are the ruler axiom, triangle inequality and the bisector axiom. Angle measure is derived from distance, and all properties needed to establish a consistent system are derived. In particular, the SAS congruence theorem is proved. The proofs are broken into many small steps suitable for the target audience. Some explorations with geometry drawing programmes are shown.     

Separating families of locale maps and localic embeddings

We establish the notion of a separating family of locale maps, which is the localic analogue of the topological concept of separating points from closed sets by continuous maps. We then present a localic version of the topological embedding (or diagonal) theorem. Applications to arbitrary locales, zero-dimensional locales, and completely regular locales are given. Using the axiom of choice, we are able to control the number of factors of the target localic products so that it does not exceed the weight of the embeddable locale. Apart from the proofs of results involving the weights of locales, the remaining proofs are valid in topos logic.     

An axiom system for the weak monadic second order theory of two successors

A compelte axiom system for the weak monadic second order theory of two successor functions, W2S, is presented. The axiom system consists, roughly, of the generalized Peano axioms and of an inductive definition of the finite sets. For the proof, methods of J. R. Buchi and J. Doner are used to obtain a new decision procedure for W2S, whose proofs are easily formalized. Different finiteness axioms are discussed. This paper was written while the author was visiting at Purdue University, and appeared first as Report CSD TR-56, Purdue University, 1971.     

An axiomatic foundation of Cayley-Klein geometries

We present a common axiomatic characterization of Cayley-Klein geometries over fields of characteristic \({\neq 2}\). To this end the axiom system of Bachmann (Aufbau der Geometrie aus dem Spiegelungsbegriff, 2nd edn. Springer, Heidelberg1973) for plane absolute geometry, which allows a common axiomatization of Euclidean, hyperbolic and elliptic geometry, is generalized. The notion of plane absolute geometry is broadened in several aspects. The most important one is that the principle of duality holds: the dual of a Cayley-Klein geometry is also a Cayley-Klein geometry. The various Cayley-Klein geometries are singled out by additional axioms like the Euclidean or hyperbolic parallel axiom or their dual statements.     

Arithmetical conservation results

In this paper we present a proof of Goodman’s Theorem, a classical result in the metamathematics of constructivism, which states that the addition of the axiom of choice to Heyting arithmetic in finite types does not increase the collection of provable arithmetical sentences. Our proof relies on several ideas from earlier proofs by other authors, but adds some new ones as well. In particular, we show how a recent paper by Jaap van Oosten can be used to simplify a key step in the proof. We have also included an interesting corollary for classical systems pointed out to us by Ulrich Kohlenbach.     

Ternary Operations as Primitive Notions for Constructive Plane Geometry V

In this paper we provide a quantifier-free, constructive axiomatization of metric-Euclidean and of rectangular planes (generalizations of Euclidean planes). The languages in which the axiom systems are expressed contain three individual constants and two ternary operations. We also provide an axiom system in algorithmic logic for finite Euclidean planes, and for several minimal metric-Euclidean planes. The axiom systems proposed will be used in a sequel to this paper to provide ‘the simplest possible’ axiom systems for several fragments of plane Euclidean geometry. Mathematics Subject Classification: 51M05, 51M15, 03F65.     

A general axiomatic system for image resolution quantification

In this paper, we generalize our previously published axiom system for quantification of image resolution and prove that any resolution measure consistent with the new axiom system must be a homogeneous symmetric function of order 1/2 of the eigenvalues of the covariance matrix of the PSF. We demonstrate that the previous axiom system is not consistent with the affine transformation axiom. We propose a weak combination axiom to replace the previous strong combination axiom and use it to solve this conflict. It is remarkable that the original finding in one-dimension by Wang and Li can be easily rediscovered with aid of the weak combination axiom, instead of using the previous strong combination axiom. If the previous axiom system is modified with the weak combination axiom and augmented with the affine transformation axiom, the resolution measure is shown to be proportional to the squared root of the geometric mean of the eigenvalues of the covariance matrix of the PSF. Relevant discussions and possible extensions are also provided.     

Completeness theorems for continuous functions and product topologies

In this paper we formulate a first order theory of continuous functions on product topologies via generalized quantifiers. We present an axiom system for continuous functions on product topologies and prove a completeness theorem for them with respect to topological models. We also show that if a theory has a topological model which satisfies the Hausdorff separation axiom, then it has a 0-dimensional, normal topological model. We conclude by obtaining an axiomatization for topological algebraic structures, e.g. topological groups, proving a completeness theorem for the analogue with countable conjunctions and disjunctions, and presenting counterexamples to interpolation and definability.     

An axiomatic analysis of the Droz-Farny Line Theorem

We analyze an elementary theorem of Euclidean geometry, the Droz-Farny Line Theorem, from the point of view of the foundations of geometry. We start with an elementary synthetic proof which is based on simple properties of the group of motions. The proof reveals that the Droz-Farny Line Theorem is a special case of the Theorem of Goormatigh which is, in turn, a special case of the Counterpairing Theorem of Hessenberg. An axiomatic analysis in the sense of Hilbert [14] and Bachmann [2] leads to a study of different versions of the theorems (e.g., of a dual version or of an absolute version, which is valid in absolute geometry) and to a new axiom system for the associated very general plane absolute geometry (the geometry of pencils and lines). In the last section the role of the theorems in the foundations of geometry is discussed.     

Aufbau der hyperbolischen Geometrie aus dem Geradenorthogonalitätsbegriff

We present an axiom system for plane hyperbolic geometry in a language with lines as the only individual variables and the binary relation of line-perpendicularity as the only primitive notion. It was made possible by results obtained by K. List and H.L. Skala. A similar axiomatization is possible for n-dimensional hyperbolic geometry with n≥4. We also point out that plane hyperbolic geometry admits a AE-axiomatization in terms of line-perpendicularity alone, an axiomatization we could not find.     

信息熵公理及其在决策分析中的应用

针对信息量是消息发生前的不确定性给出一个直观测量信息量公式.为了克服Shannon熵的局限性和分析信息度量本质,借鉴距离空间理论中度量公理定义的思路,通过非负性、对称性、次可加和极大性给出信息熵的公理化新定义.将Shannon熵、直观信息熵和β-熵等不同形式的信息度量统一在同一公理化结构下.应用直观信息熵公式仅采用四则运算进行决策树分析,避免了利用Shannon熵公式的对数运算.     

Population replications and ethical poverty measurement

In this paper, a class of relative and a class of absolute ethical measures of poverty depending on the head-court ratio and the aggregate income gap of the poor are characterized. Among other requirements, an axiom for poverty comparisons of distributions of different dimensions is used. Furthermore, it is shown that the above-mentioned axiom for population change cannot be used to characterize a specific class of absolute ethical poverty indices depending on the absolute number of poor instead of the head-count ratio.     

Perspective Graves triads and triads of perspective inscribed triangles

Any Pappus configuration can be regarded (in six ways) as a triad of triangles, each inscribed in the previous one; such a triad of triangles is called aGraves triad. Graves triads in which each pair of triangles is in perspective may be calledperspective Graves triads; such triads occur in connection with various results in both projective and metrical geometry. In this paper we give a synthetic proof of the existence of perspective Graves triads; the proof is of interest because it holds in allharmonic planes and requires neither the axiom of Pappus nor the full axiom of Desargues. The paper also includes synthetic proofs of other related results.(Results involving perspective Graves triads can be found in [l, p.149] and [2]. This paper is the result of recent correspondence with Guinand concerning [2] and [3].)     

Convexity in Topological Affine Planes

We extend to topological affine planes the standard theorems of convexity, among them the separation theorem, the anti-exchange theorem, Radon's, Helly's, Caratheodory's, and Kirchberger's theorems, and the Minkowski theorem on extreme points. In a few cases the proofs are obtained by adapting proofs of the original results in the Euclidean plane; in others it is necessary to devise new proofs that are valid in the more general setting considered here.     

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.     

A case study in formalizing projective geometry in Coq: Desargues theorem

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to long technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point–line, point–plane, line–plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove that it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three-dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to fairly easily formalize Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.     

Players indifferent to cooperate and characterizations of the Shapley value

In this paper we provide new axiomatizations of the Shapley value for TU-games using axioms that are based on relational aspects in the interactions among players. Some of these relational aspects, in particular the economic or social interest of each player in cooperating with each other, can be found embedded in the characteristic function. We define a particular relation among the players that it is based on mutual indifference. The first new axiom expresses that the payoffs of two players who are not indifferent to each other are affected in the same way if they become enemies and do not cooperate with each other anymore. The second new axiom expresses that the payoff of a player is not affected if players to whom it is indifferent leave the game. We show that the Shapley value is characterized by these two axioms together with the well-known efficiency axiom. Further, we show that another axiomatization of the Shapley value is obtained if we replace the second axiom and efficiency by the axiom which applies the efficiency condition to every class of indifferent players. Finally, we extend the previous results to the case of weighted Shapley values.     

Weakly ordered plane geometry

A plane geometry is introduced, which although ordered such that both every line is densely linearly ordered without first or last element and such that every line partitions the points of the plane not incident with it into two convex half-planes, does not need to satisfy the Pasch axiom. An alternate axiomatization of ordered planes is obtained by adding several axioms, including the inner form of the Pasch axiom. The missing link between the inner form of Pasch’s axiom and the full Pasch axiom is herewith determined.     

Constructive Axiomatizations of Plane Absolute,Euclidean and Hyperbolic Geometry

In this paper we provide quantifier‐free, constructive axiomatizations for 2‐dimensional absolute, Euclidean, and hyperbolic geometry. The main novelty consists in the first‐order languages in which the axiom systems are formulated.