Profiniteness in finitely generated varieties is undecidable
Anvar M. Nurakunov Michał M. Stronkowski
math.LO math.GN 22A30, 03D35, 03C05, 06E15, 08B25




 





plain
theoremTheorem[section]
proposition[theorem]Proposition
lemma[theorem]Lemma
corollary[theorem]Corollary
fact[theorem]Fact
conjecture[theorem]Conjecture
*claimClaim
definition
definition[theorem]Definition
example[theorem]Example
remark[theorem]Remark
question[theorem]Question
problem[theorem]Problem

tmTheorem
thmTheorem
cor[thm]Corollary
lm[thm]Lemma
rem[thm]Remark
cproof



























 


Institute of Mathematics, National Academy of Sciences of the Kyrgyz Republic,
pr. Chu 265a, Bishkek, 720071 Kyrgyzstan
a.nurakunov@gmail.com



Faculty of Mathematics and Information Sciences,
Warsaw University of Technology, ul. Koszykowa 75, 00-662
Warsaw, Poland
m.stronkowski@mini.pw.edu.pl




[2010]22A30, 03D35, 03C05, 06E15, 08B25

































 



















The first author is supported by Alexander von Humboldt Foundation (Fellowship 2017) and Ministry of Education and Science of Kazakhstan.
The second author is supported by the Polish National Science Centre grant no. DEC-2011/01/D/ST1/06136.  








Profinite algebras are exactly those that are isomorphic to inverse limits  of finite algebras. Such algebras are naturally equipped with Boolean topologies. A variety  is standard if every Boolean topological algebra with the algebraic reduct in  is profinite.   

We show that there is no algorithm which takes as input a finite algebra  of a finite type and decide whether the variety  () generated by  is standard.
We also show the undecidability of some related properties. In particular, we solve a problem posed by Clark, Davey, Freese and Jackson.

We accomplish this by combining two results. The first one is Moore's result saying that there is no algorithm which takes as input a finite algebra  of a finite type and decides whether () has definable principal subcongruences.  The second is our result saying that possessing definable principal subcongruences yields possessing finitely determined syntactic congruences for varieties. The latter property is known to yield standardness.


Profiniteness in finitely generated varieties is undecidable 
    Michał M. Stronkowski
    December 30, 2023
=============================================================






§ INTRODUCTION




 §.§ What we prove


Let  be a variety (an equationally defined class of algebras, see Section <ref> for definitions). We consider the class of _Bt of Boolean topological algebras with the algebraic reducts in , and the class V_Bc of profinite algebras (consider also as Boolean topological algebras) with the algebraic reducts in . The class _Bc is called the Boolean core of . We call  standard provided that _Bt=V_Bc, i.e., when all Boolean topological algebras with the algebraic reducts in  are profinite. Let us formulate our main result.


There is no algorithm which decides if a given finite algebra of a finite type generates a standard variety.



The most widely applicable condition forcing standardness for varieties is possessing finitely determined syntactic congruences (FDSC) <cit.>. This prompted the authors of <cit.> to formulate the following question.

[<cit.>]
Is there an algorithm to decide if a given finite algebra of finite type generates a variety with finitely determined syntactic congruences?
   
We present the answer to this question.


There is no algorithm which decides if a given finite algebra of a finite type generates the variety with finitely determined syntactic congruences.



The standardness of   may be restated as the property that profinite algebras from  (equipped with a natural topology) may be distinguished among all Boolean topological algebras of the same type as  just by checking the satisfaction of identities defining . In particular, we can do it without referring to topology. We may then ask when this distinction can be done within a particular logic and without referring to topology. The case of first-order logic was addressed in <cit.>. With respect to this issue, we obtain the following fact.


There is no algorithm which decides if a given finite algebra of a finite type generates the variety with the Boolean core definable (relative to the class of all Boolean topological algebras of the same type as ) by a set of sentences in a first-order logic.


 



 §.§ How we prove it



A general strategy for Problem <ref> was already proposed in <cit.>. It is based on McKenzie's construction <cit.>. It effectively assigns to each Turing machine 𝐓 the algebra A(𝐓) such that 𝐓 halts iff there is a finite bound on the cardinality of subdirectly irreducible algebras in the variety V( A(𝐓)) generated by A(𝐓). In fact, if  does not halt, then, up to term equivalence, the particular subdirectly irreducible algebra 𝐐_ω (described in Section <ref>) is in V( A(𝐓)). The algebra 𝐐_ω admits a compatible Boolean topology. Thus 𝐐_ω with this topology belongs to V( A())_Bt and does not belong to V( A())_Bc. Hence it witnesses that V( A(𝐓)) is not standard. In particular, V( A()) does not have FDSC <cit.>. 

What remains to be proved is that V( A()) has FDSC if  halts. However, recently Moore verified that it is not true <cit.>. 
In the same paper he also showed that V( A()) does not have  definable principal subcongruences (DPSC) (see Section <ref> for the definition). This property was invented in order to give the most elegant proof  of Baker's  finite basis theorem <cit.> saying that every finitely generated congruence-distributive variety of a finite type is finitely axiomatizable <cit.>. (The idea of Baker and Wang was subsequently used also in the context of quasivariety <cit.> and of deductive systems <cit.>.)

In  <cit.> Moore managed to modify the algebra A() by adding one basic operation. The resulting algebra A'() allows him to obtain the following fact: V( A'()) has DPSC iff  halts. Consequently, he proved that the problem whether the variety generated by a given finite algebra of finite type has DPSC is undecidable.  In <cit.> he suggested that the construction of A'() would be used in Problem <ref>. Indeed, again, up to term equivalence, the algebra 𝐐_ω belongs to V( A'()).  The author also wrote that a detailed analysis of polynomials in V( A'()) might be needed in order to show that V( A'()) has FDSC when  halts.


It led us to consider an idea that having DPSC may yield having FDSC in general. If it is true, then actually no additional analysis of the variety V( A'()) is needed. Let us look at both properties from a common perspective of defining principal congruences. The principal congruence θ(a,b) generated by a pair (a,b) in an algebra  is a transitive closure of the relation R which is the carrier of the subalgebra 𝐑 of ^2 generated by {(a,b),(b,a)}∪{(c,c)| c∈ A}. This fact may be expressed in the following way: a pair (c,d) is in θ(a,b)  iff there is a congruence formula (see Section <ref> for formal definitions) witnessing it. These are two dimensional objects. They have length which expresses how many compositions of the relation R we have to use. They also have depth which expresses, roughly speaking, how complex terms we have to use when generating 𝐑. A variety  has  definable principal congruences (DPC) if there is a finite bound on length and  depth in a whole . There are many ways to weaken this property. It appears that  has FDSC exactly when there is a finite bound only on depth (we assume that the type of  is finite) and length is arbitrary. And  has DPSC when we have length and depth bounded by a finite number just for some principal congruences. 

At first glance, it seems that the properties of having FDSC and DPSC are incomparable. The group 𝐒_3 of all permutation on a three element set generates the variety with FDSC (every variety of groups has FDSC) and without DPSC <cit.>. Also, every finite non-distributive lattice generates the variety without DPC <cit.> but, by the main result in <cit.> (see also our Corollary <ref>), with FDSC. But an example of a variety with DPSC and without FDSC is unknown. 



The main technical contribution of this paper is the introduction of a common weakening of the properties of  having FDSC and having DPSC. When a variety has this property, we say that it has term finite principal subcongruences (TFPSC).  We show that having TFPSC is equivalent to having FDSC for varieties (Theorem <ref>). 

    @=15pt@M=9pt    DPC  @=>[dl]  @=>[dr]    
     FDSC  @=>[dr]        DPSC  @=>[dl] 
        TFPSC      -37ptcolapses to@=15pt@M=9pt DPC  @=>[d]   
     DPSC  @=>[d] 
        FDSC ⇔ TFPSC



Thus it is indeed the case that having DPSC yields having FDSC. This fact, Moore's result and the analysis of 𝐐_ω lead to a negative answer for the question in Problem <ref>. Thus Theorems <ref> and <ref> hold. A bit of additional work on algebra 𝐐_ω, based on a technique from <cit.>, leads to the conclusion that the Boolean core of V( A'()) is not axiomatizable in first-order logic when  does not halt. This gives Theorem <ref>. 




   













 









 §.§ Why we prove it; A bit of history




Let  be a finite structure (a set with operations and relations of finite arities) equipped with a discrete topology. The class IS_CP^+() of all isomorphic images of closed subalgebras of non-zero direct powers of  is called the topological prevariety generated by . Such classes appear in duality theory as dual categories <cit.>. For example, in Stone duality for Boolean algebras as  we take a two element set (no operations and relations) and then IS_CP^+() is the class of Boolean topological spaces (aka Stone spaces) <cit.>. In Pristley duality for bounded distributive lattices as  we take a two element linearly ordered set  and then IS_CP^+() is the class of Pristley spaces 

<cit.>.
In Pontryagin duality restricted to abelian groups of exponent at most m we may take the group ℤ_m of integers modulo m. Then IS_CP^+(ℤ_m) is the class of Boolean topological abelian groups of exponent at most m <cit.>.

It is a convenient situation when we have a good description of members of IS_CP^+(). A general scheme, based on the idea from <cit.>, for axiomatizations of topological varieties was given in <cit.>. However, it involves infinite, possibly difficult to work with, expressions. They refer to topological properties of the structures under considerations. Consequently, such axiomatizations are not considered as good. The property of standardness, introduced in  <cit.> was intended as a formalization of the idea of good behavior for topological prevarieties with respect to the axiomatization. 

A  theory for standardness was developed in <cit.>, and the following general sufficient condition was presented. (Standardeness was defined there as the property for topological prevarieties, not for quasivarieties.) 


Let 𝒬 be the quasivariety (a universal Horn class with a trivial algebra) generated by a finite algebra. If  𝒬 is a variety with FDSC, then 𝒬 is standard

Stone duality and restricted Pontryagin duality fall into the scope of this theorem. But Pristley duality, even if we extend this theorem to relational case, does not <cit.>. We will use a slight extension of the FDSC-HSP theorem, see Theorem <ref>.


In <cit.> a main problem in this area was formulated.

[<cit.>]
Is there an algorithm to decide if a given finite algebra of finite type generates a standard universal Horn class?
   


 
Problem <ref> seems to be very difficult. It is open even when we restrict it to finite lattices <cit.>. Thus the authors of <cit.> also formulated a simpler Problem <ref>, together with some hints how to approach it.


In <cit.> two extensions were made. Firstly, not only finitely generated, but also topological prevarieties generated by sets of finite structures are considered. Secondly, a weakening of standardness to first-order axiomatizations, as still good description, was proposed. General techniques for disproving standardness and first-order axiomatization were presented. In particular, it appears that Pristley duality is as bad as it can be: the topological prevariety of Pristley spaces in not first-order axiomatizable <cit.>. An analogous problem to Problem <ref> for first-order aximatizability is formulated <cit.>. It is also suggested that standardness may yield finite aximatizability for finitely generated universal Horn classes. There are known standard finitely generated varieties which are not finitely axiomatizable (for instance of semigroups). However, such universal Horn classes are unknown <cit.>. Note  that the converse implication does not hold. The class of ordered sets is not standard <cit.>. Moreover, a non-standard finitely axiomatizable universal Horn class generated by a four-element algebra in presented in <cit.>.






We would like to point out the following quotation of Johnstone  <cit.> 

The question thus arises: given an algebraic category A, when
can we say that every Stone topological A-algebra is profinite? It seems
hard to give a simple condition on A which is both necessary and sufficient;


The meaning of the adjective simple is unclear. But one could argue that simplicity should yield decidability for varieties presented in a finitary way. Thus Theorem <ref> confirms Johnstone's supposition in case of presenting a variety by a finite generating algebra. Yet, there is another finitary way of presenting varieties: by a finite set of defining identities. For this case Jackson proved an analogous theorem.


There is no algorithm which decides if a given finite set of identities defines a standard variety or a variety with FDSC.







§ TOOLBOX


Here we provide the required definitions and facts. If necessary, the reader may consult <cit.> for notions in universal algebra and <cit.> for notions on topological prevariety (note that adopt the terminology from <cit.>.




 §.§ Algebras, topological algebras and Boolean cores

Let us fix an arbitrary finite algebraic type σ, i.e., a finite set of symbols of basic operations with ascribed arities. Except Section <ref>, all (topological) algebras will be of type σ. 

A universal Horn class of algebras is a class definable by (first-order) universal Horn sentences, i.e., universal sentences without occurrences of conjunction and with at most one positive literal. Equivalently, a class of algebras is a universal Horn class iff it is closed under the formation of isomorphic images, subalgebras and direct products over a nonempty indexing sets  <cit.>. Our results refers to classes closed under homomorphic images, in particular to varieties. A variety is a class of algebras definable by identities, i.e., sentences which are universally quantified equations. Equivalently, a class of algebras is a variety iff it is closed with respect to the formation of homomorphic images, subalgebras and direct products over arbitrary indexing sets  <cit.>.




A topological algebra  is a pair (,𝒯) where  is an algebra of type σ and 𝒯 is a topology such that every basic operation ω^n→ is a continuous map with respect to topological spaces (A,𝒯) and its power (A,𝒯)^n (we also say that 𝒯 is compatible with basic operations of ). 

In this paper all considered topological spaces are Boolean. This means that they are Hausdorff, compact and totally disconnected. Topological algebras with such topologies are called Boolean topological algebras. Most commonly encountered Boolean topological algebras are profinite (groups, rings, semigroups, distributive lattices, Heyting algebras, closure algebras, all of them have FDSC <cit.>). It means that they are isomorphic to inverse limits of finite algebras. However, not all Boolean topological algebras are profinite. For instance, one may take an infinite subdirectly irreducible algebra (i.e., having a least congruence which is not the identity relation) admitting a Boolean topology. An example of such unary algebra is given in <cit.> and of modular lattice  in <cit.>, see also <cit.>. One such example, presented in Section <ref>, will be crucial for us. 




Following <cit.>, we call a class of Boolean topological algebras which is closed under the formation of isomorphic images, topologically closed subalgebras and direct products over a nonempty indexing set a topological prevariety.  (The fact that we disallow empty indexing set is not relevant here. Indeed, the difference is only with adding or excluding a trivial algebra. It has its origin in duality theory, where this definition is natural.)

For every class 𝒦 of Boolean topological algebras there exists a smallest topological previariety containing 𝒦. It consists of topological algebras which are isomorphic to closed subalgebras of non-zero products of members of 𝒦. 

With a given universal Horn class  $̋ (in particular, with a variety) we associate two topological prevarieties: The first one, denoted by_̋Btconsists of all Boolean topological algebras with the algebraic reducts in$̋. The second one, denoted by _̋Bc and called the Boolean core of $̋, is the topological prevariety generated by finite members of$̋, each of them considered as a Boolean topological algebra with the discrete topology. In general, we have the inclusion _̋Bc⊆_̋Bt. We say that $̋ is standard if_̋Bt=_̋Bc. 

It appears that the members of_̋Bcare exactly those Boolean topological algebras which are isomorphic to inverse limits of finite algebras from$̋ <cit.>. Moreover,
profinite algebras are exactly those algebras which are isomorphic to inverse limits of its finite homomorphic images.

Thus, since varieties are closed under the formation of (finite) homomorphic images, we have the following fact.



Let  be a variety. Then _Bc consists of all profinite algebras which have the algebraic reducts in . Consequently,  is standard if and only if every Boolean topological algebra with the algebraic reduct in  is profinite. 



We say that a topological prevariety 𝒢 is first-order  axiomatizable if there exists a set S of first-order sentences such that 
𝒢 consists of all Boolean topological algebras of type σ with algebraic reducts satisfy all sentences from S. We are interested in the existence of first-order axiomatization of Boolean cores. Clearly, if $̋ is a standard universal Horn class, then_̋Bcis first-order axiomatizable by any set of first-order sentences defining$̋. However, there are non-standard universal classes with the first-order axiomatizable Boolean core. Such an universal Horn class generated by a finite lattice is presented in <cit.>).
We will need the following fact. Recall that an algebra is locally finite if every its finitely generated subalgebra is finite. In this paper by a one-point compactification we mean a  topological space (A,𝒯) with a distinguish element 0, where  

    𝒯={B∈𝒫(A)| 0∈ B and  A-B  is finite}∪𝒫(A-{0}).

Here 𝒫(X) denotes the powerset of X. The point 0 is called then the condensation point of (A,𝒯). Note that (A,𝒯) is simply the Alexandrov compactification of the discrete spaces on the set A-{0}. 

 

Let =(,𝒯) be a Boolean topological algebra such that


  *  is locally finite,

  *  has a constant 0,

  * (A,𝒯) is a one-point compactification with the condensation point 0,

  * ∈_Bt-_Bc,

  * for every algebra  of the same type as , if  is a model of the universal theory of  and  (B,𝒯') is the one-point compactification with the condensation point 0, then the topology 𝒯' is compatible on  (i.e, (,𝒯') is a Boolean topological algebra). 

Then _Bc is not first-order axiomatizable.






 §.§ Determining  principal congruences



Let us fix a denumerable set X={x,p_0,p_1,p_2,…} of variables. We consider x as a distinguished  variable. Let us also fix one  set 
 of terms over X satisfying the following conditions


  * x∈ T_x,

  * if ω is a basic operation of positive arity n,  then 
 ω(p_0,…,p_i-1,x,p_i+1,…, p_n-1)∈ T_x,

  * if s(x,p̅), t(x,q̅)∈ T_x, then s(t(x,q̅),p̅)∈ T_x.
 


From the perspective of this paper it is not relevant which set T_x satisfying the listed conditions is chosen (actually, we could simply take T_x to be the set of all terms over X)
. What is important is the following Mal'cev's lemma. For an algebra  and a pair a,b of its elements let θ(a,b) denote the principal congruence of  generated by (a,b).


By a congruence formula π(u,v,x,y) we mean a first-order formula of the form

    CF∃p̅( u≈ t_0(z'_0,p̅)(⋀_i=0^n-1 t_i(z_i',p̅)≈ t_i+1(z'_i+1,p̅))  t_n(z'_n,p̅)≈ v  ),

where t_i(x,p̅)∈ T_x and {z_i,z_i'}={x,y} for all 0≤ i≤ n.  Let us denote the set  {t_0,…,t_n} of terms appearing in (CF) by (π). The set of all congruence formulae will be denoted by Π. (Now we formalize the notions from the introduction: The length of π in (CF) equals n, and the depth is the maximal depth of x in the terms t_0,…,t_n.)





 
 
For an algebra  and elements a,b,c,d∈ A we have (c,d)∈θ(a,b) if and only if there is a  congruence formula π(u,v,x,y) such that π(c,d,a,b).
 

The above lemma suggests that we may impose various restrictions on determining principal congruences. For instance, a class 𝒞 of algebras has definable principal congruences (DPC in short) if there is a finite set P⊆Π such that θ(a,b)={(c,d)∈ A^2|∃π∈ P  π(c,d,a,b)} for all a,b∈ A, ∈𝒞. (This topic is covered in a more general context of relative congruences in <cit.>.) In this paper a weaker restriction will be crucial:
For F⊆ T_x let 

    Π^F={π∈Π|(π)⊆ F}.
 
For an algebra  and its elements a,b define

    θ^F(a,b)={(c,d)∈ A^2|∃π∈Π^F (c,d,a,b)}.

We say that a subset F of T_x determines principal congruences in a class 𝒞 if for every ∈𝒞 and a,b∈ A we have θ(a,b)=θ^F(a,b).
We say that 𝒞 has term finite principal congruences (TFPC in short) if there is a finite subset of T_x which determines principal congruences in 𝒞.




For F⊆ T_x and an algebra  let F^ be the set of all translation on  induced by terms in F. Formally,
 
    F^={f∈ A^A|∃ t(x,p̅)∈ F,e̅∈ A^n  ∀ a∈ A  f(a)=t(a,e̅)}.

For an equivalence relation θ on the carrier of an algebra  let 

    θ_F={(a,b)∈ A^2|∀ f∈ F^  (f(a),f(b))∈θ}.

Note that θ_F is an equivalence relation on A. If x∈ F, then it is contained in θ. More generally, θ_G⊆θ_F whenever F⊆ G.  Moreover, θ_T_x is the largest congruence on  contained in θ  <cit.>). It is called the syntactic congruence of θ and is denoted by (θ).

We say that F⊆ T_x determines syntactic congruences in a class 𝒞 of algebras provided that (θ)=θ_F for every equivalence relation θ on the carrier of an algebra in 𝒞. We say that 𝒞 has finitely determined syntactic congruences  if there is a finite subset of T_x determining syntactic congruences in 𝒞. 

It appears that the properties of having FDSC and TFPC are equivalent.

Let 𝒞 be a class of algebras and F⊆ T_x. Then F determines syntactic congruences in 𝒞 if and only if F determines principal congruences in 𝒞.


From the proof of Lemma <ref> we may extract the following fact.



Let  be an algebra, a,b∈ A, and θ be an eqivalence relation on A. If (a,b)∈θ_F, then θ^F(a,b)⊆θ.



What makes the property of having FDSC relevant in the context of topological algebras is the fact that this property yields  profiniteness. The following observation was first proved for many special cases, see the historical comments preceding <cit.>. (The reader may also see <cit.> for a related characterization of profiniteness.)



Let  be a Boolean topological algebra. If there is a finite set of terms that determines syntactic congruences on , then  is profinite.


Proposition <ref> and Fact <ref> give the following theorem.


Let  be a variety. If  has FDSC, then  is standard. 





§ DETERMINING  PRINCIPAL SUBCONGRUENCES




We say that a pair F,G of subsets of T_x determines principal subcongruences in a class 𝒞 of algebras if for every ∈𝒞 and for every pair a,b of distinct elements of A there is a pair c,d of distinct elements of A such that  

    (c,d)∈θ^F(a,b)   and   θ(c,d)=θ^G(c,d).

A class 𝒞 has term finite principal subcongruences (TFPSC in short) if there is a pair  of finite subsets of T_x which determines principal subcongruenses in 𝒞.

Let θ,η be equivalence relations on a set A. If η⊆θ then the quotient equivalence relation θ/η on the set A/η is given by

    (a/η,b/η)∈θ/η  iff   (a,b)∈θ.



 
Let F⊆ T_x, θ be an equivalence relation on the carrier of an algebra  and a,b∈ A. Then (a,b)∈θ_F if and only if (a/-1pt(θ),b/-1pt(θ))∈(θ/-1pt(θ))_F. Consequently, (θ/-1pt(θ)) is the identity relation on A/-1pt(θ).






By definition of θ_F, we have


    (a,b)∈θ_F      iff   (f(a),f(b))∈θ  for all   f∈ F^
         iff   (f(a)/-1pt(θ),f(b)/-1pt(θ))∈θ/-1pt(θ)  for all   f∈ F^ 
         iff   (g(a/-1pt(θ)),g(b/-1pt(θ)))∈θ/-1pt(θ)  for all   g∈ F^/-1pt(θ)
         iff   (a/-1pt(θ),b/-1pt(θ))∈(θ/-1pt(θ))_F.

The third equivalence follows from the fact that (θ) is a congruence on . 
By setting F=T_x, we obtain the second assertion.



For F,G⊆ T_x we define

    F∘ G ={ s(t(x,q̅),p̅)| s(x,p̅)∈ F and  t(x,q̅)∈ G}.

Then for every algebra  and every equivalence relation θ on A we have

    COMPθ_F∘ G=(θ_F)_G.



Let 𝒞 be a class of algebras and  assume that 𝒞 is closed under homomorphic images.
Let  F,G⊆ T_x. If the pair F,G determines principal subcongruences in 𝒞, then G∘ F determines syntactic congruences in 𝒞. 



Let  be an algebra in 𝒞 and θ be an equivalence relation on A. We want to show that (θ)=θ_G∘ F. Let =/-1pt(θ) and η=θ/-1pt(θ). By Lemma <ref>, (η) is the identity relation on B. Thus we should show that η_G∘ F is the identity relation on B.
Assume that it is not the case, i.e., there is a pair a,b of distinct elements of B such that (a,b)∈η_G∘ F. 

By assumption, =/-1pt(θ)∈𝒞.
Thus the pair F,G determines principal subcongruences in . This yields that there exists a pair c,d of distinct elements such that

    (c,d)∈θ^F(a,b)   and   θ(c,d)=θ^G(c,d).

By (<ref>), η_G∘ F=(η_G)_F. Hence, by Lemma <ref>, 

    (c,d)∈θ^F(a,b)⊆η_G.

Applying Lemma <ref> once more, but 
for c,d and G, we infer that

    θ(c,d)=θ^G(c,d)⊆η.

It follows that (c,d)∈η_T_x. Since η_T_x=(η) and (η) is the identity relation on B, c=d. This is a contradiction with the choice of c,d. 



Let 𝒞 be a class of algebras and  assume that 𝒞 is closed under homomorphic images.
Then 𝒞 has FDSC if and only if 𝒞 has TFPSC.



The forward implication follows from Lemma <ref> and the obvious fact that having TFPC yields TFPSC. The backward implication follows from Proposition <ref>.



We present two corollaries.

We say that a class 𝒞 has definable principal subcongruences (DPSC for short) if there are finite subsets  P,R of T_x such that for every algebra ∈𝒞 and for every pair a,b of distinct elements of A there are a pair c,d of distinct elements of A and a congruence formula π∈ P such that

    π(c,d,a,b)   and   θ(c,d)={(e,f)∈ A^2|∃ρ∈ R  ρ(e,f,c,d)}.
 
In <cit.> it is pointed that having DPC yiels having TFPC, and hence also having FDSC. But 
clearly, also having DPSC yields TFPSC. Thus Theorem <ref> gives the following stronger fact.

 
Let 𝒞 be a class of algebras and  assume that 𝒞 is closed under homomorphic images. If 𝒞 has DPSC, then 𝒞 has FDPC.


The following corollary was proved in <cit.>, and then reproved in <cit.>. The novelty here is the fact that we do not need to use  Jónsson's terms in order to prove it.
Indeed, one of the main results in <cit.> is the proof (without Jónsson's terms) that finitely generated congruence distributive varieties have DPSC. 
 

Let 𝒱 be a congruence distributive finitely generated variety. Then  has FDSC.



It follows by Corollary <ref> and <cit.>.






§ UNDECIDABILITY





By modifying McKenzie construction <cit.>, Moore <cit.> provided an effective construction that takes a Turing machine  and returns the algebra A'() with some properties depending on whether  halts or not. The construction  is quite complicated. However, we extract some information relevant for our paper in the next theorem. 

We say that two algebras are term equivalent if they have the same carrier and the same set of term operations. This means that every basic operation of one of this algebras is a term operation of the second algebra. 

Let Q_ω=(Q_ω,⊓,·,0) be the algebra with the carrier

    Q_ω={a_0,b_0,a_1,b_1,…}∪{0},

where 0 is a constant and ⊓,· are binary operations given by 

    a⊓ b =
    
    a     if  a=b
    
    0     if a≠b
          
    a· b =
    
    b_i     if  a=a_i,b =b_i+1 and i∈ℕ
     
    0     otherwise.

Note that Q_ω is subdirectly irreducible and locally finite.



Let  be a Turing machine and A'(T) be the algebra constructed as in <cit.> for . Then


  * if  halts on empty input, then V( A'()) has DPSC;

  * if  does not halt on empty input, then there is an algebra Q in  V( A'()) which is term equivalent to Q_ω.
 


The following fact holds.



Assume that there is an algebra Q in  which is term equivalent to Q_ω. Then _Bc is not  first-order axiomatizable.


 
We equip the set Q_ω with the Boolean topology 𝒯 such that (Q_ω,𝒯) is the a one-point compactification with the condensation point 0. It is the case that 𝒯 is compatible with basic operations of Q_ω, and hence with basic operations of Q. This means that Q=( Q,𝒯) is a Boolean topological algebra.  
We use Proposition <ref> for Q. The condition (1)-(3) from this theorem thus hold. The argument for the condition (4), which says that Q witnesses non-standardness for , was given in <cit.>: Since Q is infinite subdirectly irreducible, Q cannot be profinite. 

Let us check the condition (5). Let Q' be an algebra of the same type as Q and assume that Q' satisfies every universal sentence which holds in Q. Let 𝒯' be the Boolean topology such that (Q',𝒯') is the one-point compactification with the condensation point 0.
In Q' we have (term) operations ·, ⊓ and 0. We have to verify their continuity. Indeed, all basic operations in Q' may be obtained by composition of these three ones. Thus their continuity will follow.

The operation 0, as a constant, is obviously continuous. Let C∈𝒯' and a,b∈ Q' be such that a∘ b ∈ C, where ∘=· or ∘ =⊓. We have to find two sets A,B in 𝒯' such that (a,b)∈ A× B and A∘ B⊆ C.

In order to do it let us first observe that Q, and hence also Q', satisfy the sentence

    (∀ x,y)   x∘ y ≉0  →  ( x≉0   y≉0).
 
Thus, in the case when 0∉C we may put A={a} and B={b}. 

Let us assume that 0∈ C. Then the set Q'-C is finite and does not contain 0. Note that Q and Q' satisfy the sentence

    (∀ x,y,x',y')  (x∘ y≈ x'∘ y'   x∘ y ≉0)  →  (x≈ x'   y≈ y'   x≉0   y≉0).
 
Hence the cardinalities of the sets

    L =    {a∈ Q'|∃ d∈ Q'   a∘ d∈ Q'-C},
    
    R =    {b∈ Q'|∃ c∈ Q'   c∘ b∈ Q'-C}

are not greater than the cardinality of Q'-C. Thus they are finite. Moreover,  0,a∉L and 0,b∉R. Hence we may put A=Q'-L and B=Q'-R.






Let  be a Turing machine and '(T) be the algebra constructed as in <cit.> for . Then


  * if  halts on empty input, then V( A' ()) has FDSC;

  * if  does not halt on empty input, then  V( A'())_Bc is not  first-order axiomatizable.
 




It follows from Corollary <ref>, Theorem <ref> and Proposition <ref>.





By Theorem <ref>, having FDSC yields standardness for varieties and, clearly, standardness yields first-order axiomatizability of the Boolean core. Thus the theorem follows from the undeciability of halting problem and Theorem <ref>.
 


plain





§ PROBLEMS


There are important problems concerning the results of this paper. Both of them may be stated as follows: Are our main theorems really different?


Provide an example of a standard finitely generated variety of a finite type which does not have FDSC.


There is a candidate for it in <cit.>.



Provide an example of a non-standard finitely generated variety of a finite type with the first-order definable Boolean core.



plain




