Austin laws
The singleton or empty magma satisfies all equational laws. It is natural to ask whether an equational law admits nontrivial finite or infinite models. If no model exists, then the law is equivalent to E2 \(({x = y})\). An Austin law is a law which admits infinite models, but no nontrivial finite models: the law is equivalent to E2 for finite magmas. Austin (Austin 1965) established the first such law, namely the order \(9\) law
A shorter Austin law of order \(6\) was established in (Kisielewicz 1990):
TheoremKisielewicz's first Austin law#
E374794 \(({x = (((y \diamond y) \diamond y) \diamond x) \diamond ((y \diamond y) \diamond z)})\) is an Austin law.
Proof
First we show that every finite model of E374794 is trivial. Write \(y^2 := y \diamond y\) and \(y^3 := y^2 \diamond y\). For any \(y,z\), introduce the functions \({f_y: x \mapsto y^3 \diamond x}\) and \({g_{yz}: x \mapsto x \diamond (y^2 \diamond z)}\). E374794 says that \(g_{yz}(f_y(x))=x\), hence by finiteness \(g_{yz}=f_y^{-1}\), showing that \(g_{yz}\) does not depend on the value of \(z\). Since
it follows that \(f_y(y^2 \diamond z)=f_y(y^3)\) which by injectivity of \(f_y\) implies that \(z\mapsto y^2 \diamond z\) is a constant function (with \(y\) fixed). Substituting \(y^2\) for \(y\) shows that the same is true for \(z\mapsto (y^2 \diamond y^2) \diamond z\), and since
we conclude that \(f_y\) is also a constant function. But this function is already known to be injective, thus there do not exist distinct elements in its domain, showing that the model must be trivial.
To construct an infinite model, consider the magma of positive integers \(\mathbb{Z}^+\) with the operation \(x \diamond y\) defined by
Then \(y \diamond y = 2^y\) and \((y \diamond y) \diamond y = 1\) for all \(y\). If \(x\neq 1\) we have that
and since \((y \diamond y) \diamond z\) is a power of two for all \(y, z\) it follows that
The case \(x=1\) requires a further argument: observe that \(w = (y \diamond y) \diamond z\) evaluates to one unless \(z = 2^y\), in which case it evaluates to \(2^{2^y}\) (which is greater than or equal to four). In particular, \(w\) never takes the value two. Thus
concluding our proof that this magma is a model of E374794
Lean
Formalized as InfModel.Finite.Equation374794_implies_Equation2, InfModel.Equation374794_not_implies_Equation2.
Sources
Uses 2
An even shorter law (order \(5\)) was obtained by the same author in a follow-up paper (Kisielewicz 1997):
TheoremKisielewicz's second Austin law#
E28770 \(({x = (((y \diamond y) \diamond y) \diamond x) \diamond (y \diamond z)})\) is an Austin law.
Proof
Using the \(y^2\) and \(y^3\) notation as before, the law reads
In particular, for any \(y\), the map \(T_y \colon x \mapsto y^3 \diamond x\) is injective, hence bijective in a finite model \(G\). In particular we can find a function \(f : G \to G\) such that \(T_y f(y) = y^3\) for all \(y\) Applying (1) with \(x = f(y)\), we conclude
and thus \(y \diamond z\) is independent of \(z\) by injectivity of \(T_y\). Thus, the right-hand side of (1) does not depend on \(x\), and so the model is trivial. This shows there are no non-trivial finite models.
To establish an infinite model, use \(\mathbb{N}\) with \(x \diamond y\) defined by requiring
and
for \(x \neq 3^y\), and
for \(z \neq 3^y 5^x\). Finally set
for \(z \neq 3^y, 2^{3^y}\). All other assignments of \(\diamond\) may be made almost arbitrarily, such as setting them to \(1\). It is then a routine matter to establish (1).
Lean
Formalized as InfModel.Equation28770_not_implies_Equation2.
Sources
Uses 2
In that paper a computer search was also used to show that no law of order four or less is an Austin law.
An open question is whether E5093 \(({x = y \diamond (y \diamond (y \diamond (x \diamond (z \diamond y))))})\) is an Austin law. We have the following partial result from (Kisielewicz 1997):
TheoremEquation 5093 has no non-trivial finite models#
E5093 has no non-trivial finite models.
Proof
From E5093 we see that the map \(w \mapsto y \diamond w\) is onto, hence injective in a finite model. Using this injectivity four times in E5093, we see that \(z \diamond y\) does not depend on \(z\), hence the expression \(x \diamond (z \diamond y)\) does not depend on \(x\). By E5093 again, this means that \(x\) does not depend on \(x\), which is absurd in a non-trivial model.
Lean
Formalized as InfModel.Finite.Equation5093_implies_Equation2.
Sources
Uses 2
The following result was established in (Austin 1966):
TheoremAustin's finite model theorem#
Any law with at most two variables has a non-trivial finite model.
Proof
If neither side of the law is a single variable then the zero law \(x \diamond y = 0\) will work, so one can assume the law takes the form \(x = f(x,y)\). Consider a finite field \(F\) with the operation \(x \diamond y := ax+by\) for some coefficients \(a,b \in F\). Then the law becomes a pair of equations \(P(a,b)=0\), \(Q(a,b)=1\) in the coefficients for some polynomials \(P,Q\) with integer coefficients, which one can verify to not divide each other (they have the same degree, and do not have the same set of non-zero monomials). From Bezout's theorem, this equation has a solution in some field, and hence by the Lefschetz principle it has a solution in a finite field.
Lean
Formalized as InfModel.Finite.two_variable_laws.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.