Another characterization of congruence distributive varieties

We provide a Maltsev characterization of congruence distributive varieties by showing that a variety 𝓥 is congruence distributive if and only if the congruence identity … (k factors) holds in 𝓥, for some natural number k.

Klein-Beltrami model. Part III

SummaryTimothy Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2],[3],[4],[5].With the Mizar system [1] we use some ideas taken from Tim Makarios’s MSc thesis [10] to formalize some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. In this article we prove that our constructed model (we prefer “Beltrami-Klein” name over “Klein-Beltrami”, which can be seen in the naming convention for Mizar functors, and even MML identifiers) satisfies the congruence symmetry, the congruence equivalence relation, and the congruence identity axioms formulated by Tarski (and formalized in Mizar as described briefly in [8]).

Multi-brand loyalty in consumer markets: a qualitatively-driven mixed methods approach

Purpose Although multi-brand loyalty (MBL) in consumer markets has been identified in previous brand loyalty research, empirical studies have not yet explored the facets of its different types. This paper aims to have a deeper understanding of MBL by investigating its different types and facets. Design/methodology/approach This study uses a sequential, qualitatively driven mixed-method design consisting of in-depth interviews and supplementary survey research. Findings The findings of this study suggest that mood congruence, identity enhancement, unavailability risk reduction and market competition are the most important facets that explains the two types of MBL (complementary-based and product substitutes). Furthermore, the findings show that the family factor can motivate consumers to be multi-brand loyal by adding brands to an initially family-endorsed brand. Research limitations/implications This study advances the conceptual foundations of MBL and extends previous research on brand loyalty. Some of the findings may be limited to the economic and cultural context of relatively affluent countries with an abundance of market offers. Practical implications Marketing managers gain insights into how to manage brand loyalty and how to transition from MBL to single-brand loyalty. Originality/value The study generates novel insights into the facets of different types of MBL.

Tarski Geometry Axioms – Part II

Summary In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation), of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1), congruence equivalence relation (A2), congruence identity (A3), segment construction (A4), SAS (A5), betweenness identity (A6), Pasch (A7). Also a simple model, which satisfies these axioms, was previously constructed, and described in [6]. In this paper, we deal with four remaining axioms, namely: the lower dimension axiom (A8), the upper dimension axiom (A9), the Euclid axiom (A10), the continuity axiom (A11). They were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles cong is introduced via congruence of sides (SSS). In order to show that the structure which satisfies all eleven Tarski’s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure Euclid 2 satisfies all these attributes. Although the tradition of the mechanization of Tarski’s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned – we had some doubts about the proof of the Euclid’s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].

Chief Factor Sizes in Finitely Generated Varieties

Let A be a k-element algebra whose chief factor size is c. We show that if B is in the variety generated by A, then any abelian chief factor of B that is not strongly abelian has size at most ck−1. This solves Problem 5 of The Structure of Finite Algebras, by D. Hobby and R. McKenzie. We refine this bound to c in the situation where the variety generated by A omits type 1. As a generalization, we bound the size of multitraces of types 1, 2, and 3 by extending coordinatization theory. Finally, we exhibit some examples of bad behavior, even in varieties satisfying a congruence identity.