Fork Algebras in Usual and in Non-well-founded Set Theories

(An Overview)

Ildikó Sain and István Németi^{∗}

March 12, 1996

Abstract

We consider classes of relation algebras expanded with new operations based on the formation of ordered pairs. Examples for such algebras are fork algebras of computer science and pairing algebras of algebraic logic. Among others we prove that the equational theory of the class of Set (or Proper) Fork Algebras (where the fork operation is defined with the help of standard set theoretic pairing) is not finitely axiomatizable, not only in our usual set theory, but also in most of the known unusual set theories, e.g. in the non-well-founded ones surveyed in Aczel’s book, in Quine’s New Foundation, etc. We also attempt to present a kind of “roadmap” by giving a systematic answer to the question asking which choice of proper fork (or pairing) algebras in which choice of set theory can support a reasonable representation theory. It turns out that the Axiom of Strong Extensionality plays a decisive role.

Keywords: relation algebras, quasi-projections, fork algebras, algebraic logic, non-well-founded sets, representability

∗Research supported by Hungarian National Foundation for scientific research grants No’s T16448, T7567, F17452.

Contents

1 Introduction 2

2 Proper Fork Algebras 5

3 Nonstandard Fork Algebras and Weak Representability 14

4 Candidates from the Literature for Proper Fork(-like) Algebras 20

5 The concatenation-version of Proper Fork Algebras 25

6 Positive results 29

1 Introduction

Fork algebras are relation algebras expanded with a new operation based on forming ordered pairs like “a, b ↦ ⟨a, b⟩”. They have been fruitfully applied in computer science in various ways, some references are: Baum et al [9], [8], [10], Berghammer et al [11], Gyuris [16], Haeberer–Veloso et al [17], [39], [40], [41]. Relation algebras expanded with operations (or sometimes just with elements) based on forming ordered pairs have also been studied in algebraic logic under the names “relation algebras with projection elements” or “quasi-projective relation algebras” or “pairing algebras”. Cf. e.g. Tarski [37], Tarski– Givant [38], Németi [24], Andréka–Jónsson–Németi [4], Maddux [20], [19], Mikulás–Sain–Simon [22], Sain–Simon [33].

Analogously to the situation with Boolean algebras, groups, semigroups, polyadic algebras, etc., it is considered desirable to develop a representation theory for fork algebras, too (cf. e.g. [15], [10]). This would consist of

• defining a “concrete” class of, say, “set (or proper) fork algebras” (analogously to Boolean set algebras, transformation semigroups, polyadic set algebras), and

• an axiomatic class FA, defined by finitely many equations (or perhaps quasi-equations), of “abstract fork algebras”; and then

• a “representation theorem” stating that every member of FA is isomorphic to a set fork algebra.

In [28], [33] and [22], it was proved (in usual set theory ZFC) that the equational theory Eq(SFA)^{1} of Set (or Proper) Fork Algebras (see Definition 2.2 below) is not recursively enumerable, moreover, it is Π_{1}^{1}- complete. The Axiom of Foundation was mentioned in the proofs. Therefore, the question comes up that, perhaps, in some of the currently investigated non-well-founded set theories, this class of algebras might show a better behaviour. Here, in section 2, we prove that in most of these non-well-founded set theories this negative result goes through, and that there are further negative results in this line. Namely, in socalled strongly extensional set theories, the quasi-equational as well as the universally quantified theories of SFA are not finitely axiomatizable, and neither I SFA nor S P SFA is axiomatizable by any set of first order formulas.

The present paper also tries to provide a “roadmap” or systematic investigation of the variants for the choice of the notion of proper, or concrete, fork algebra suggested in the literature so far. The existence of a representation theorem depends on three choices: (i) the notion of proper fork algebra, (ii) the notion of abstract fork algebra, (iii) the choice of background (meta) set theory. Therefore our roadmap will be three dimensional in the sense that we will try to give a systematic answer to the general question asking which choices of proper and abstract fork algebras work in which choice of set theory. In particular, in section 3 we discuss what kind of classes can be considered as “concrete” and what is the difference between strong and weak representability. We give several suggestions for the class FA of abstract fork algebras. In sections 4–5 we study the various candidates suggested in the literature as proper fork algebras, and show that the negative results of section 2 concerning the class SFA carry over for these classes, if we keep the metatheory strongly extensional. Finally, in section 6 we summarize the positive results of [26], [25] that can be achieved if we choose some non-well-founded set theory which is not strongly extensional.

Throughout, ZF denotes the usual Zermelo-Frankel set theory, ZFC denotes ZF plus the Axiom of Choice. ZFC^{−} denotes the set theory obtained from ZFC by dropping the Axiom of Foundation (AF). We use the notation ZF^{−} analogously. We do not even assume the Collection Principle as an axiom of ZF^{−}(which is used as an axiom of ZF in [1] but not in Kunen’s, Levy’s or Jech’s books on set theory)^{2} .

1The class here we call SFA was called SEBR in the quoted papers.

The Axiom of Extensionality is not enough to identify non-well-founded sets. Therefore, to handle “set identity”, we need something stronger. This is served by the following potential axiom, called the Axiom of Strong Extensionality (SEX).

(SEX) For any transitive sets^{3} x, y, if either x and y have the same elements or ⟨x, ∈⟩ ≅ ⟨y, ∈⟩^{4} then x = y.

We would like to point out that axiom SEX is exactly the same as axiom FAFA_{2} (part of Finsler’s anti-foundation axiom) in Aczel [1, pp.46–48]. SEX is a theorem both of ZF and of the non-well-founded set theories in Barwise–Etchemendy [7]. To unify the various non-well-founded set theories, Aczel [1, section 4] introduces the flexible axiom AFA^{∼}, where the special equivalence relation ∼ is a parameter of the axiom. For various choices of ∼, we obtain different set theories, e.g., Scott’s non-well-founded set theory, the basic variant AFA of Aczel [1], etc. Aczel [1, Prop.4.26, p.52] shows that SEX is a theorem in all of these set theories.

CONVENTION 1.1 Our theorems below marked as

“(in strongly extensional set theories)”

(after the number of the theorem) are true in any set theory in which ZFC^{−}+SEX is provable. In particular, they are true in both usual set theory ZFC and in the non-well-founded set theories found in Barwise– Etchemendy [7] or in Aczel [1, sections 1–4].

Actually, our results carry over to even more general set theories. Let SEX^{−} denote the weaker axiom we obtain from SEX by restricting x, y to be countably infinite sets. That is, distinct transitive sets may have isomorphic ∈-structures if they are either finite or there is no bijection between them and ω. Now, SEX^{−} is substantially weaker than SEX.

2In passing we note that, by Andréka–Kurucz–Németi [5], Birkhoff’s celebrated characterization of equational hulls depends on the Axiom of Foundation.

3x is transitive iff (∀z ∈ x) z ⊆ x.

4⟨x, ∈⟩ ≅ ⟨y, ∈⟩ iff (∃ injective f : x → y)(∀u, v ∈ x)[u ∈ v ⇔ f(u) ∈ f(v)].

We note that the reason why SEX is usually kept in set theories when “throwing away” AF is that SEX is designed to help us keeping at least parts of our usual mathematical intuition when working in non-well-founded set theories. E.g., ZFC^{−} (without SEX) permits the existence of undefinable hereditarily finite sets. Further, some models of ZFC^{−} have a proper class of automorphisms. Therefore those sets which are interchanged by these automorphisms have exactly the same set theoretic properties, hence cannot be distinguished in the language of mathematics, and still they are distinct. SEX was designed to help these anomalies.

Briefly we mention the system of set theory known as Quine’s New Foundation (NF) and the weaker system NFU of NF with Urelements, cf. e.g. Forster [14]. NF is among the oldest axiomatic set theories without the Axiom of Foundation. The negative results of this paper seem to go through in NF, NFU and even in weakened versions of NF, as far as Axiom of Strong Extensionality (SEX) is added.

The results of this paper were announced in [31] and in [30]. An extended abstract of the present paper is [32].

2 Proper Fork Algebras

On binary relations, say R and S, there are the well known set theoretic operations, e.g. R ∪ S, R ∩ S, …, R ∘ S (relation composition), R^{−1} (converse or inverse), Id (the identity relation). From the above mentioned literature of fork algebras, in Definition 2.2 (ii) below we recall a new binary set theoretic operation ▽, called “fork”, defined on binary relations. So, R▽S is a new binary relation derived from R and S.

Notation 2.1 ⟨x, y⟩ is the usual set theoretic ordered pair of x and y. That is, ⟨x, y⟩ = {{x}, {x, y}}. For any set X, P(X) denotes the powerset (set of all subsets) of X. tr(X) denotes the transitive closure of X, i.e., the smallest transitive set containing X. □

Definition 2.2 (i) By a Set Relation Algebra (an SRA for short) we understand an algebra A = ⟨A, ∪, ∩, −_{U}, ∅, U × U, ∘,^{−1}, Id⟩, where U is a set, A ⊆ P(U × U), ⟨A, ∪, ∩, −_{U}, ∅, U × U⟩ is a Boolean set algebra with greatest element U × U, the constant Id = {⟨a, a⟩ : a ∈ U}, and ∘,^{−1} are the usual set theoretic operations of composition and converse (or inverse) of relations. (R ∘ S = {⟨x, y⟩ : xRz and zRy for some z ∈ U}, R^{−1} = {⟨x, y⟩ : ⟨y, x⟩ ∈ R}, for any R, S ⊆ U × U.) U is called the base set of A.

(ii) Let R and S be binary relations. Then R▽S is a new binary relation defined as follows.

R▽S =^{def} {⟨x, ⟨y, z⟩⟩ : xRy and xSz}.

We call ▽ the fork operation.

(iii) A is called a Set (or Proper) Fork Algebra (an SFA) iff A = ⟨B, ▽⟩, where B is an SRA closed under ▽, and the operation ▽ of A is defined as in (ii) above. □

Other possible ways of defining SFA suggested in the literature will be discussed in sections 3, 4 and 5 below.

Throughout, we use notation like SRA in two different sense. First, an SRA is an algebra defined above. Second, SRA also denotes the class of all SRA’s.

For a class K of algebras, I K, S K, P K and H K denote, respectively, isomorphic copies, subalgebras, isomorphic copies of direct products and homomorphic images of members of K.

Notation 2.3 There are two ways of defining Set Relation Algebras. In one of the cases we require the greatest element 1^{A} of a Set Relation Algebra A to be a square U × U, while in the other case, 1^{A} is required to be an equivalence relation E ⊆ U × U only. We will call the second class (with 1^{A} = E) the class of Generalized Set Relation Algebras (GSRA’s).

The definition of GSFA is obtained from that of SFA in a completely analogous way (that is, requiring only 1^{A} = E).

Theorem 2.3.1 (in ZFC^{−}) I GSRA = S P SRA.

This theorem was proved by Tarski in ZFC, cf. e.g. [18]. It can be checked that the proof does not use the Axiom of Foundation.

Theorem 2.3.2 (in ZFC^{−}) I GSFA = S P SFA.

This can be proved exactly as 2.3.1 is proved in [18], cf. also [23].

Therefore, instead of introducing GSRA and GSFA directly (and then investigating them), we introduced here SRA and SFA, and will investigate S P SRA and S P SFA. By Theorems 2.3.1 and 2.3.2 above, this will have the same effect, that is, Eq(SRA) = Eq(GSRA) and Eq(SFA) = Eq(GSFA).

For various reasons, of the classes defined so far it is GSRA and GSFA that we are interested in, cf. e.g. [18], and Discussion 3.1 below. In particular, the classes RRA of Representable Relation Algebras and RFA of Representable Fork Algebras are defined by

RRA =^{def} I GSRA and RFA =^{def} I GSFA . □

Remark 2.4 In the present paper we are using the usual definitions of the concepts of finiteness, standard model of arithmetic, computability, recursive enumerability, etc. relativized to well-founded sets (which are definable in ZF^{−}). □

PROPOSITION 2.5 (in ZFC^{−}) Assume ZF set theory is consistent. Then (i)–(iii) below hold.

(i) It is not provable that Eq(SFA) would be recursively enumerable, hence no decidable (in particular, no finite) axiomatization can be proved complete (and sound) for Eq(SFA).

(ii) Statement (i) remains true for the quasi-equational theory as well as for the first order theory of SFA.

(iii) It is not provable that I SFA or S P SFA would be axiomatizable (or even pseudo-axiomatizable) by any set of first order formulas.

Proof. This is an obvious consequence of results in [33] or [22]. In these papers it is proved (in ZFC) that Eq(SFA) is not recursively enumerable, and I SFA and S P SFA are not closed under taking ultraproducts. For completeness, we also refer to the proof of Theorem 2.12 in the present paper.

Let us investigate whether Proposition 2.5 above forces us to give up all hope for obtaining positive results using the idea of permitting non-well-founded sets outlined in the introduction. To obtain positive results, perhaps it is not enough to throw away the Axiom of Foundation. Perhaps we have to add new axioms to ZFC^{−} designed for helping us in working with non-well-founded sets. Below we will see that in strongly extensional set theories the classes I SFA and S P SFA are still not axiomatizable; that the equational theory Eq(SFA) of SFA’s is still not finitely axiomatizable; and that there are further negative results in this line.

THEOREM 2.6 (in strongly extensional set theories) The class I SFA of isomorphic copies of Proper Fork Algebras is not axiomatizable by any set of first order sentences. The same is true for the class S P SFA of Representable Fork Algebras.

Proof. We prove that I SFA and S P SFA are not closed under taking ultrapowers.

Let U = Vω be the set of hereditarily finite well-founded sets. Let

A = ⟨P(U × U), ∪, ∩, −_{U}, ∅, U × U, ∘,^{−1}, Id⟩

be the Set Relation Algebra of all subsets of U × U. Then A is closed under (set theoretic) ▽, since U × U ⊆ U. Thus B = ⟨A, ▽⟩ is in SFA.

By an abstract singleton we understand an element x satisfying equations (1 ∘ x) ∩ (x ∘ 1) ≤ Id and 1 ∘ x ∘ 1 = 1. Abstract singletons of an SFA are “real” singletons below Id, i.e., they are of the form {⟨a, a⟩}. Consider the following abstract singletons of B.

x_{0} =^{def} {⟨∅, ∅⟩}
x_{1} =^{def} {⟨⟨∅, ∅⟩, ⟨∅, ∅⟩⟩}
…
x_{n+1} =^{def} {⟨x_{n}, x_{n}⟩}
…

Let s = (Id▽Id), s^{0} = Id and s^{n+1} = s^{n} ∘ s for all n ∈ ω. Then for each n ∈ ω, x_{n} = s^{n} ∘ x_{0} ∘ (s^{n})^{−1} holds. (So far we did not use the Axiom of Choice.)

Now let F be a nonprincipal ultrafilter over ω, and C =^{def} ωB/F. Consider the following elements of C.

y_{0} =^{def} ⟨x_{0}, x_{1}, …, x_{n}, …⟩/F
…
y_{n} =^{def} ⟨\underbrace{∅, …, ∅}_{n-many}, x_{0}, x_{1}, …⟩/F  (n ∈ ω)

Then for any n ∈ ω, y_{n} is an abstract singleton and y_{n} = s^{n} ∘y_{0} ∘(s^{n})^{−1} holds.

Claim 2.6.1 C ∉ S P SFA.

Proof of Claim 2.6.1. Assume C ≅ D for some D ∈ SFA with base set W. Then there are elements z_{n} (n ∈ ω) of D such that for all n ∈ ω,

z_{n} is an abstract singleton  (1)
z_{n} = s^{n} ∘ z_{0} ∘ (s^{n})^{−1}  (2)
z_{m} ≠ z_{n} if m ≠ n.  (3)

But D ∈ SFA, thus there exists an ω-sequence ⟨w_{n} : n ∈ ω⟩ ∈ ωW such that for any n ∈ ω,

z_{n} = {⟨w_{n}, w_{n}⟩}  (by (1))
w_{n} = ⟨w_{n+1}, w_{n+1}⟩  (by (2))
w_{m} ≠ w_{n} if m ≠ n  (by (3)).

Then the epsilon-structures ⟨tr(w_{0}), ∈⟩ and ⟨tr(w_{1}), ∈⟩ are isomorphic. Therefore, by SEX, w_{0} = w_{1} — a contradiction. This disproves our assumption D ∈ SFA. Thus C ∉ I SFA. Now, C ∉ S P SFA is easily derived from this, since C is simple. (Claim 2.6.1)

Thus we proved that an ultrapower of an SFA is not in S P SFA.

The same proof yields the following stronger result.

COROLLARY 2.7 (in strongly extensional set theories) Let K ⊆ S P SFA. Assume there is a simple A ∈ K having two distinct abstract singletons u, v as elements (i.e., 1 ∘ u ∘ 1 = 1 and (1 ∘ u) ∩ (u ∘ 1) ≤ Id, and same for v). Then K is not axiomatizable by any set of first order formulas.

Proof. We prove that if some simple A ∈ K contains at least two distinct abstract singletons u, v then ωA/F ∉ K for some ultrafilter F. Let W_{0} = {u, v}, W_{1} = (W_{0} × W_{0}) − W_{0}, W_{n+1} = (W_{n} × W_{n}) − (W_{n} ∪ W_{n−1} ∪ … W_{0}), for n ∈ ω. Then (∀n ∈ ω)W_{n} ≠ ∅ (e.g. by [38]). Let W = ⋃{W_{n} : n ∈ ω}, and V_{n} = W_{0} ∪ W_{1} ∪ … W_{n}, for n ∈ ω. Let k ∈ ω be such that W_{0} ∩ (W × W) ⊆ V_{k} × V_{k}. Let d ∈ W_{k+1}. Then ⟨d, d⟩ ∉ V_{k+1} since for every x ∈ V_{k+1} either x ∈ W_{0} − (W × W) or (∃a, b ∈ V_{k})x = ⟨a, b⟩, but d ∉ V_{k}. Similarly

(∀n > k)(∀e ∈ W_{n})⟨e, e⟩ ∉ V_{n−1} .  (4)

Using our abstract singletons u, v ∈ A (and the operation ▽) we can generate a singleton {⟨d, d⟩} ∈ A for some d ∈ W_{n} with n > k. Let e_{0} = d and e_{n+1} = ⟨e_{n}, e_{n}⟩. Then |{e_{n} : n ∈ ω}| = ω, by (4). Let x_{n} = {⟨e_{n}, e_{n}⟩} for n ∈ ω. Then s∘x_{n+1}∘(s^{−1}) = x_{n} for all n, where s = (Id▽Id). Further, {x_{n} : n ∈ ω} ⊆ A. Consider the ultrapower ωA/F for a nonprincipal F. Let y_{i} be the element of ωA/F corresponding to ⟨x_{n+i} : n ∈ ω⟩. Now {y_{i} : i ∈ ω} behaves exactly as the y_{i}’s constructed in the proof of Theorem 2.6. From this point on, the above proof goes through.

THEOREM 2.8 Theorem 2.6 and Corollary 2.7 remain true in ZF^{−}+SEX.

Proof. The Axiom of Choice can be eliminated from the above proofs by replacing ultraproducts with using the compactness theorem for countable languages.

Motivated by Tarski–Givant [38], next we recall (e.g. from [24]) a class SPA of algebras whose relation algebra type reduct is a subclass of the class QRA^{5} investigated in [38]. Our SPA’s are those QRA’s whose quasi-projections p, q are the standard set theoretic projection functions. SPA’s were called “strongly quasi-projective relation algebras” and also “standard projection models” in [24, Def.16, pp.74–75]; they were called “RRA’s with standard projections” in Andréka–Jónsson– Németi [4, p.426]; cf. also “conjugated projections over ordered pairs” in [38, above 4.1 (iv) p.96]. In [38, p.96], SPA’s (in different form) are mentioned as a familiar example for QRA’s.

5see Definition 3.3(ii) below

Definition 2.9 A is called a Set Projection Algebra (an SPA) iff A = ⟨B, p, q⟩ where B is an SRA with greatest element U × U, and

p =^{def} {⟨⟨x, y⟩, x⟩ : x, y ∈ U} and q =^{def} {⟨⟨x, y⟩, y⟩ : x, y ∈ U}

are distinguished constants of A. The constants p and q are the standard projections (on set U). □

Let K_{1} and K_{2} be two classes of algebras. Then K_{1} ≡ K_{2} means that K_{1} and K_{2} are term-definitionally equivalent, cf. e.g. McKenzie et al.

[21] or [18, polinomially equivalent, Part I, p.125].

THEOREM 2.10 (in ZF^{−}) SFA ≡ SPA.

Proof. By the definitions of ▽, p, q, we have

R▽S = (R ∘ p^{−1}) ∩ (S ∘ q^{−1}) .

Further, it is easy to see that

p = (Id▽1)^{−1}  and  q = (1▽Id)^{−1} .

COROLLARY 2.11 Theorems 2.6–2.8 above are true for SPA’s in place of SFA’s.

We note that a variant □ of ▽ was introduced and studied in Tarski– Givant [38, 8.4 (xii)] and [4, p.427]. The connection is:

x▽y = (p · q)^{−1} ∘ (x□y) and x□y = (p ∘ x)▽(q ∘ y).

The following theorem, expressing that the equational theory of SFA is very far from being computable, is proved in [33] assuming ZFC. Here we prove that it holds in any strongly extensional set theory. Recall from recursion theory that the computational complexity of a Π_{1}^{1}-hard class is not lower than that of the set of all Π_{1}^{1} formulas valid in the standard model of arithmetic. Thus a Π_{1}^{1}-hard class cannot be described by constructive tools.

THEOREM 2.12 (in strongly extensional set theories) Let K ⊆ H S P SFA or K ⊆ H S P SPA and assume ⟨P(U × U), …⟩ ∈ K for some set U with |U| > 1. Then the equational theory Eq(K) of K is Π_{1}^{1}-hard.^{6}

Proof. The present theorem was proved in [33, Thm.0] assuming ZFC (cf. also [22, Thm.1]). We will show below that the proof in [33] does not essentially use the Axiom of Foundation (AF), instead, it uses the corollary SEX of AF. We will actually show that Eq(K) is not in the arithmetical hierarchy, by showing that the proof in [33] goes through under assuming only ZF^{−}+SEX, and its only step using SEX is Lemma 2.12.1 below.

The standard projections p and q was used in [33] to code the standard model \underline{ω} = ⟨ω, 0, suc, ≤, +, ⋆⟩ of arithmetic in Eq(SPA). Below we recall how the first order theory of \underline{ω} was coded in Eq(SPA) in [33] and in [28]. We fix algebraic variables x_{≤}, x_{+}, x_{⋆} to represent the relations ≤, +, ⋆ of \underline{ω} = ⟨ω, 0, suc, ≤, +, ⋆⟩. suc itself is represented by (p ∩ q)^{−1}. We choose a large enough but finite set P A_{0} of first-order formulas valid in \underline{ω}. Then we fix e_{P A} to be an SPA-equation expressing that “the binary relations suc, x_{≤}, x_{+}, x_{⋆} satisfy the axioms P A_{0}” (whatever this statement might mean). We do not recall here the exact form of e_{P A}, since we do not need it.

Similarly, to any first order formula φ (in the language of \underline{ω}) we associate an SPA-equation e_{φ} which expresses that “φ is satisfied by ⟨… (p ∩ q)^{−1}, x_{≤}, x_{+}, x_{⋆}⟩”. Then (∗) below is proved in [33]. For any first order formula φ,

(∗) \underline{ω} ⊧ φ iff SPA ⊧ (e_{P A} → e_{φ}).

The only part of the proof of (∗) where AF was used is the proof of the following.

6We think that the proof in [33] yields the stronger statement that Eq(K) is Π_{1}^{1}-complete.

(∗∗) If A ∈ SPA and A ⊧ e_{P A}[x_{≤}, x_{+}, x_{⋆}] for some x_{≤}, x_{+}, x_{⋆} ∈ A then the structure ⟨…, (p ∩ q)^{−1}, x_{≤}, x_{+}, x_{⋆}⟩ is isomorphic to \underline{ω}.

The only purpose for which AF was used in [33] was to exclude the possibility that ⟨…, (p∩q)^{−1}, x_{≤}, x_{+}, x_{⋆}⟩ would be a nonstandard model of P A_{0}. But for this, it is enough to see the following lemma.

LEMMA 2.12.1 (in ZF^{−}+SEX) (p ∩ q)^{−1} contains no infinite “descending chain”, i.e., there is no infinite sequence of elements a_{1}, a_{2}, …, a_{n}, … with

(∀n ∈ ω) (p ∩ q)(a_{n}) = a_{n+1}.

Proof of Lemma 2.12.1. Let a_{0} be arbitrary and assume for each n ∈ ω that a_{n+1} = (p ∩ q)(a_{n}). We may assume that the finite set P A_{0} of axioms contains the postulate saying that ≤ is a linear ordering containing the transitive closure of suc. Hence we know that (p ∩ q)^{−1} (and x_{≤}) contains no circles. Thus a_{n} ≠ a_{m} if n ≠ m. Then a_{0} = ⟨a_{1}, a_{1}⟩ = {{a_{1}}}, …, a_{n} = {{a_{n+1}}}. Therefore, for each n ∈ ω, the transitive closure tr(a_{n}) = {a_{k}, {a_{k}} : k ≥ n} is an infinite descending chain of singletons, like this:

… ∈ a_{n} ∈ … ∈ {a_{2}} ∈ a_{1} ∈ {a_{1}} ∈ a_{0}.

Hence e.g. ⟨tr(a_{0}), ∈⟩ ≅ ⟨tr(a_{1}), ∈⟩, which by SEX implies a_{0} = a_{1}, and this is not the case. (Lemma 2.12.1)

Now, the proof in [33] yields (∗∗) from Lemma 2.12.1, and then yields (∗), proving the present theorem without using AF.

The following corollary was first proved as [28, Thm.25.1] in ZFC. Now, by the previous theorem, it holds in any strongly extensional set theory.

COROLLARY 2.13 (in strongly extensional set theories) Eq(SFA) and Eq(SPA) are not recursively enumerable.

COROLLARY 2.14 (in strongly extensional set theories)

(i) Eq(SFA) and Eq(SPA) are not finitely axiomatizable.

(ii) The quasi-equational theories of the classes SFA and SPA are not finitely axiomatizable.

(iii) The sets of universally quantified formulas valid in the classes SFA and SPA are not finitely axiomatizable either.

3 Nonstandard Fork Algebras and Weak Representability

Below (in Discussion 3.1) we summarize some basic considerations about representation theorems in algebra. For more detail on these ideas we refer to e.g. Henkin–Monk–Tarski [18, item 2.7.46 (Part I, pp.459–461)], Tarski–Givant [38, p.62 lines 9–11, section 3.5 (p.56)], Németi [23, beginning with “Remark 2 (Finitization)”], [12], Simon [35], [6, Jónsson’s problem on p.441]. All the arguments and results of this section take place in usual set theory ZFC.

Discussion 3.1 ^{7} A class K_{1} of algebras is called abstract if it is closed under taking isomorphic copies. A class K_{2} is called concrete if for any A, B ∈ K_{2}, whenever A and B have the same universe, then A = B, that is, the universe of A determines the operations of A. In mathematics, (strong) representation theorems are of the following form. An abstract class K_{1} of algebras is considered together with a concrete class K_{2} ⊆ K_{1}. Now, a (strong) representation theorem says that every algebra in the abstract class K_{1} is isomorphic to a member of the concrete class K_{2}.

Examples of (strong) representation theorems are the representation of abstract Boolean algebras (as K_{1}) in terms of concrete Boolean set algebras (as K_{2}), that of abstract groups as concrete permutation groups, point-dense relation algebras as set relation algebras, locally finite cylindric algebras as cylindric set algebras, etc. In each of these cases, the choice of K_{2} (e.g., Boolean set algebras, permutation groups, etc.) was a concrete class (e.g., the universe of a permutation group G completely determines the operations of G).

In some cases, when real representation theorems are not available, weak representation theorems are used as a substitute. In weak representation theorems, instead of requiring K_{2} to be concrete, the operations of K_{2} are represented in terms of a third class K_{3} of structures, which in turn, is defined abstractly again.

7Parts of this discussion were borrowed from Gyuris [16, Remark 4].

In more detail, when K_{2} is concrete, then for each A ∈ K_{2}, the universe A of A completely determines the operations of A, that is, to each operation, say g of A, there is an explicit set theoretic definition of g using no other parameter than A. E.g., in Boolean set algebras “x ∧ y” is the real set theoretic intersection of x and y. In case of weak representation theorems for each operation g of A ∈ K_{2}, there is a definition of g, but this definition depends on not only on A but something else. Namely, a third class K_{3} is introduced axiomatically (i.e., K_{3} is not concrete), and then the operations (like g above) of K_{2} are defined in terms of the abstract class K_{3}. Since K_{3} is chosen to be abstract, defining K_{2} in terms of K_{3} does not ensure concreteness of K_{2}. The insight usually provided by strong representation theorems comes from the fact that they interpret an abstract class by a concrete class. As a contrast, weak representation theorems interpret an abstract class (K_{1}) in another abstract class (K_{2}). Therefore, they do not necessarily bridge the gap between “abstract” and “concrete”. Nevertheless, weak representation theorems can be useful in several context. □

Returning to our present algebras, SFA and SPA are concrete classes. Therefore, representing a class of algebras in terms of SFA’s would be a strong representation theorem. However, Theorems 2.6–2.14 above show that such a strong representation theorem is impossible, at least in strongly extensional set theories (thus also in ZFC). Below we discuss the finitely axiomatizable class NFA of “Nonstandard Fork Algebras” (see Definition 3.2) which was suggested in the literature to achieve weak representability.

Definition 3.2

(i) A is called a Nonstandard Fork Algebra (an NFA)^{8} iff there are a set U and an injective function f : U × U >⟶ U such that A = ⟨B, ▽^{f}⟩, where B is an SRA with greatest element U × U, and for any R, S ∈ B,

8The use of the expression “Nonstandard Fork Algebra” for this kind of algebras was suggested during the Fork Algebra Discussion evening at the Dagstuhl seminar [13].

R▽^{f}S = {⟨x, f(y, z)⟩ : xRy & xSz}

is also in B.

(ii) The structure ⟨U, f⟩ is called the pairing structure of A. □

Definition 3.3 (i) An algebra A = ⟨A, +, ·, −, 0, 1, ∘,^{−1}, Id⟩ is a Relation Algebra (an RA) if it satisfies the equations listed in Tarski– Givant [38, p.235, RaI–X] (cf. also Henkin–Monk–Tarski [18, Part II, ch.5.3]).

(ii) A Relation Algebra A is called a QRA (cf. Tarski–Givant [38]) iff the following (existential) formula is valid in A.

∃p∃q(p^{−1} ∘ p ≤ Id ∧ q^{−1} ∘ q ≤ Id ∧ p^{−1} ∘ q = 1).

Such elements p, q are called quasi-projections. □

There is a certain property of NFA’s that is sometimes called “expressibility of first order logic (FOL) in the equational theory Eq(NFA) of NFA”. This property was essentially proved to hold by Tarski around 1941, see e.g. [38, p.xvi (middle of page)] and also [37, p.586 (middle of page)] (namely, he proved it for QRA, but the RA-reduct of every NFA is obviously a QRA).^{9}

THEOREM 3.4 (Tarski, early 1940’s^{10}) Every QRA is representable, that is, QRA⊆RRA.

9Here we do not want to commit ourselves on the question whether calling this property “expressibility of FOL” is justified. L. Henkin and others expressed certain reservations and problems in this connection, cf. e.g. [28] and Simon [35]. Certainly, Tarski proved this property, but he or Tarski–Givant [38] did not call it “expressibility of FOL”. Instead, they spoke about expressibility of certain strong enough first order theories (cf. e.g. [38], [36]).

10In 1943–44, a theory was built around this result and was presented at Tarski’s Relation Algebra Seminar in 1945, Univ. of California at Berkeley, cf. [38, pp.xvi line 6 bottom up–xvii line 12, and footnote 3 on p.168]. Later, finding different kinds of (simple) proofs for this result became a broadly pursued and fruitful research topic, cf. e.g. Maddux [20], Simon [34].

Proof. It can be found e.g. in Tarski–Givant [38] or in Maddux [20].

Definition 3.5 ([4, section 7], based on [38])

PA =^{def} {⟨A, p, q⟩ : A is a QRA with quasi-projections p, q

and ⟨A, p, q⟩ ⊧ (p ∘ p^{−1}) · (q ∘ q^{−1}) ≤ Id}. □

FACT 3.6 SRA⊆RA and SPA⊆PA.

THEOREM 3.7 (implicit in [4] and in [38]) PA ≡ S P NFA.

Proof. Let A be a subdirectly irreducible PA. Then, by Lemma 8.1 of [4] credited to [38] there, there is some A′ ∈ SRA with greatest element U × U such that A is embeddable into ⟨A′, p^{A}, q^{A}⟩. But then, by the condition on p and q in the definition of PA, p^{A}, q^{A} : U ⟶ U, moreover, letting f =^{def} {⟨a, b, c⟩ ∈ ^{3}U : p^{A}(c) = a & q^{A}(c) = b}, the relation f turns out to be an injective function f : U × U >⟶ U. Thus, ⟨A′, ▽^{f}⟩ is an NFA with pairing structure ⟨U, f⟩. This proves that S P NFA is term-definable in PA. The other direction, saying that PA is term-definable in S P NFA, follows easily using the terms given in the proof of Theorem 2.10 above. A detailed proof is in Gyuris [16].

QRA’s with quasi-projections p, q satisfying (p ∘ p^{−1}) · (q ∘ q^{−1}) ≤ Id are investigated in Tarski–Givant [38]. Theorem 3.7 shows that there is a wealth of material in [38] (and related works) from which research on NFA (and its applications) could benefit. We note that the theory developed and carefully presented in [38] was continued e.g. in Andréka– Jónsson–Németi [4], Maddux [19] and Németi [24].

COROLLARY 3.8 S P NFA is a finitely axiomatizable variety.

Proof. By definition, PA is a variety axiomatized by the (finitely many) RA-axioms and the equations p^{−1} ∘ p ≤ Id, q^{−1} ∘ q ≤ Id, p^{−1} ∘ q = 1, (p ∘ p^{−1}) · (q ∘ q^{−1}) ≤ Id. Therefore, by Theorem 3.7, S P NFA is a finitely axiomatizable variety, too.

The class NFA is not concrete, because the operation ▽^{f} is defined only abstractly via the pairing structure ⟨U, f⟩ which was defined only axiomatically (and not concretely). Therefore, Corollary 3.8 can be considered as a weak representation theorem (in the sense of Discussion 3.1 above) as follows. The class K_{1} of abstract algebras is the finitely axiomatizable class S P NFA. The second class K_{2}, in terms of which the algebras of K_{1} are represented, is NFA which is defined with the help of the third abstract class K_{3} of pairing structures.^{11}

Below we investigate some further candidates for the role of abstract fork algebras.

Definition 3.9 An NFA is non-degenerate if the equation

1 ∘ (−Id) ∘ 1 = 1

is true in it. Those NFA’s that are not non-degenerate are called degenerate.

NFA^{+} denotes the class of non-degenerate NFA’s. □

Remark 3.10 Intuitively, the equation 1 ∘ (−Id) ∘ 1 = 1 excludes those algebras (and only those) in which our “pairing universe” U has only one element, implying f(a, a) = a for all a ∈ U. Only the nondegenerate NFA’s are relevant to applications. If an NFA is degenerate then it has only 2 elements and it contains no more information than the 2-element Boolean algebra. □

COROLLARY 3.11 S P NFA^{+} is a finitely axiomatizable variety.

THEOREM 3.12 The equational theory Eq(NFA^{+}) is hereditarily undecidable. That is, if an equational theory E contains Eq(NFA^{+}), in symbols E ⊇ Eq(NFA^{+}), then E is undecidable, unless E is inconsistent in the sense that E ⊢ 1 = 0.

Proof: A variant of this is already proved in [38] for a variety called ORA strongly related to NFA^{+}. One possible proof for the present theorem is based on the ideas in [38]. Here we give an outline of another proof, which is based on ideas from [33] and a result in [3] or [2].

11A strong representation result (concerning Relation Algebras) directly implied by Corollary 3.8 says that the RA-reducts of the finitely axiomatizable class S P NFA are representable. This amounts to saying that those RA’s which can be expanded with a new operation ▽ satisfying certain axioms are representable. No strong representation theorem concerning Fork Algebras seems to be implied directly from Corollary 3.8.

Assume V is a subvariety of the variety S P NFA^{+}. It is enough to concentrate on the class Sir(V) of subdirectly irreducible members of V.

Sir(V) ⊆ I NFA^{+}. Let A ∈ Sir(V). Then to A, there are U and f : U × U >⟶ U as in Definition 3.2 above. Let

N_{1} =^{def} Rng(Id▽^{f} − Id). Then N_{1} = {f(a, b) : a ≠ b, a, b ∈ U}. Certainly, Id_{1} =^{def} Id ∩ (N_{1} × N_{1}) is term-definable in A. Let

N_{2} =^{def} Rng(Id_{1}▽^{f} − Id_{1}), Id_{2} =^{def} Id ∩ (N_{2} × N_{2}),

…

N_{n+1} =^{def} Rng(Id_{n}▽^{f} − Id_{n}), Id_{n+1} =^{def} Id ∩ (N_{n+1} × N_{n+1}).

… One can check that {Id_{n} : n ∈ ω} are infinitely many distinct elements below Id in A, hence we can apply [3, Thm.1] or [2, Thm.2.1].

By the above, for the choice of the class FA of abstract (axiomatic) Fork Algebras we see three reasonable choices. One would be

FA_{1} =^{def} S P NFA ,

the other would be

FA_{2} =^{def} S P NFA^{+} ,

and the third would result from FA_{2} by adding a few natural equations holding in SFA to the equations defining FA_{2}. Such equations are

Id ∩ (Id▽Id) = 0,  (5)
1 ∘ −(1 ∘ (1▽1)) ∘ 1 = 1.  (6)

Equation (6) above expresses that there are elements of the universe U which are not ordered pairs. Let FA_{3} consist of those members of FA_{2} which satisfy equations (5) and (6) above.

We think that deciding which one of FA_{1}, FA_{2}, … should be FA, might be premature. For any choice of FA ∈ {FA_{1}, FA_{2}, FA_{3}}, the situation is analogous to that of (abstract) Relation Algebras (RA’s) and (concrete) Set Relation Algebras (SRA’s). The analogy is the following:

FA is analogous to RA (both are finitely axiomatizable approximations of the finitely not axiomatizable varieties generated by the concrete classes),

SFA is analogous to SRA, and

NFA is analogous to the complex-algebra representation of RA’s.^{12}

4 Candidates from the Literature for Proper Fork(-like) Algebras

In section 2 we showed that the class SFA of Set Fork Algebras (defined in Definition 2.2) does not support a representation theory in strongly extensional set theories. Here we investigate some subclasses of SFA (and SPA) suggested in the literature as possible candidates for the role of proper fork(-like) algebras. We start with recalling from Maddux [19] the definition of True Pairing Algebras (TPA’s).

Definition 4.1 (i) An SPA A with greatest element U × U is called a True Pairing Algebra (a TPA) iff U is the smallest set such that for some set W, W ⊆ U and U × U ⊆ U − W.^{13}

(ii) An SFA is called an SFA^{+} iff it is term-definitionally equivalent with a TPA. □

We note that in the definition above, A ∈ TPA iff the set W does not contain ordered pairs and U = ⋃_{n∈ω} W_{n}, where W_{0} = W and W_{n+1} = (⋃_{i≤n} W_{i}) × (⋃_{i≤n} W_{i}). Thus, in a TPA there are no infinite (p ∪ q)-chains.

12When discussing the difference between strong and weak representation theorems (our terminology), [18] mentions the Jónsson–Tarski (i.e., complex-algebra)

Representation Theorem for Boolean algebras with operators as an example for a weak representation theorem: [18, Part I, p.460 line 12] writes that this weak representation theorem is “not what could be regarded as a satisfactory representation theorem”.

13In [19], “TPA” was reserved to denote the class of those TPA’s which are of the form ⟨P(U × U), …⟩. However, this restriction does not change the equational or quasi-equational theories of the class in question.

In Definition 4.2 below, we recall from Baum–Haeberer–Veloso [10] the class GFA of free grupoid-representable fork algebras.

Definition 4.2 By a free grupoid-representable fork algebra (a GFA) we understand an NFA A with pairing structure ⟨U, f⟩ such that ⟨U, f⟩ is a free grupoid. □

PROPOSITION 4.3 (in ZF^{−}) I GFA = I SFA^{+}.

We note that SFA^{+} ⊆ SFA, TPA ⊆ SPA, and both classes contain algebras of the form ⟨P(U × U), …⟩. Therefore Theorem 2.12 applies to them, i.e., in strongly extensional set theories these classes have Π_{1}^{1}-hard equational theories. Below we show this even in ZFC^{−}.

THEOREM 4.4 (in ZFC^{−}) Let K ⊆ H S P TPA or K ⊆ H S P SFA^{+}. Assume ⟨P(U × U), …⟩ ∈ K for some U with |U| > 1. Then Eq(K) is Π_{1}^{1}-hard.

Proof. To see the TPA part, the proof method of [33] can be applied (cf. the proof of Theorem 2.12 above) as follows. The only use of the Axiom of Foundation in [33] (or SEX in the proof of Theorem 2.12) was to prove that any sequence obtained by successive applications of the function p ∩ q to an arbitrary element a_{0} ∈ U of the base set of a TPA (where p and q are the standard projections) is finite (cf. Lemma 2.12.1 above). But this finiteness is built into the definition of TPA, hence it need not be proved. Thus neither the Axiom of Foundation nor the Axiom of Strong Extensionality are needed. Now, the SFA^{+} part follows from Definition 4.1(ii).

By Theorem 4.4, the negative results in e.g. [33], [22], [28] remain true for the original algebras in [10] and Maddux [19], even if we completely drop the Axiom of Foundation from our set theory ZFC and do not “replace the gap” by any kind of anti-foundation axiom.

COROLLARY 4.5 (in ZFC^{−}) Eq(TPA), Eq(SFA^{+}) and Eq(GFA) are not recursively enumerable.

COROLLARY 4.6 (in ZFC^{−})

(i) Eq(TPA), Eq(SFA^{+}) and Eq(GFA) are not finitely axiomatizable.

(ii) The quasi-equational theories of TPA, SFA^{+} and GFA are not finitely axiomatizable.

(iii) The sets of universally quantified formulas valid in the classes TPA, SFA^{+} and GFA are not finitely axiomatizable.

We note that, by Corollary 2.7, in strongly extensional set theories I SFA^{+}, I TPA, S P SFA^{+} and S P TPA are not axiomatizable by any set of first order sentences. Below we will see that these negative results go through even in ZF^{−}.

THEOREM 4.7 (in ZF^{−}) The classes I SFA^{+}, I TPA, S P SFA^{+} and S P TPA are not axiomatizable by any set of first order sentences.

Proof. Let B be the SFA defined in the proof of Theorem 2.6. Then B ∈ SFA^{+} also holds. Let F be a nonprincipal ultrafilter over ω and let

C =^{def} ωB/F.

Claim 4.7.1 (in ZFC^{−}) C ∉ S P SFA^{+}.

Proof of Claim 4.7.1. The ω-sequence ⟨w_{n} : n ∈ ω⟩, given in the proof of Claim 2.6.1, is an infinite descending (p∩q)-chain which cannot occur in a TPA or in an SFA^{+} by definition. (Claim 4.7.1)

The Axiom of Choice can be eliminated again by replacing ultraproducts with using the compactness theorem for countable languages.

In [10], GFA’s were suggested for the rôle of proper (or set) fork algebras. The negative results above seem to imply that this direction is not likely to work in any set theory. The above negative results about free grupoid-representable fork algebras GFA’s and SFA^{+}’s suggest the question that, perhaps, we could generalize the notion of a free grupoid so much that the above negative results would go away. We will look into this below (but cf. also Definition 4.10).

Definition 4.8 (i) By a pairing structure we understand the pairing structure of some NFA (cf. Definition 3.2 (ii)).

(ii) Let U = ⟨U, f⟩ be a pairing structure. For x ∈ U, we let f^{0}(x) = x, and f^{n+1}(x) = f(f^{n}(x), f^{n}(x)) for each n ∈ ω. Now, U is called loop-free iff U ⊧ x ≠ f^{n}(x), for all n > 0.

(iii) By a loop-freely represented fork algebra (an LFA) we understand an NFA whose pairing structure is loop-free. □

We note that I LFA ⊇ GFA ∪ SFA^{+} is a very large class of fork algebras. The only restriction made in the definition of LFA is a very natural property of pairing (or of ▽), namely, that a ≠ ⟨a, a⟩ and similarly a ≠ ⟨⟨a, a⟩, ⟨a, a⟩⟩, etc. Clearly, this condition or equivalently, x ≠ f^{n}(x) is true in every (reasonable generalization of a) free grupoid.

THEOREM 4.9 (in ZFC^{−}) Let K ⊆ H S P LFA be such that ⟨P(U × U), …⟩ ∈ K, for some U with |U| > 1. Then Eq(K) is Π_{1}^{1}- hard.

Proof. It is similar to that of Theorem 4.4.

The above is a quite general result. It says that, as long as we keep our proper (or set) fork algebras to be loop-free, they will not support a representation theorem. What inconvenience can be caused by loops? If the non-standard pairing function f : U × U → U built into our algebras might contain loops then e.g. ⟨a, b⟩ = a or ⟨⟨a, b⟩, ⟨c, d⟩⟩ = a or ⟨… ⟨a, b⟩, …⟩ = a may happen. But this clearly contradicts the programmer’s intuition concerning ordered pairs or forking.

Consider the following infinite set of equations:

Id▽Id ≤ −Id,

(Id▽Id)▽Id ≤ −Id,

…

Id▽ … ▽Id ≤ −Id

…

All these equations are intuitively true properties of fork. But none of these equations are true in e.g. FA_{1} (cf. section 3). Moreover, if we add any finite number of these to the FA_{1}-axioms, the rest will remain unprovable from the enriched theory. (There are many other infinite sets of equations behaving the above way, e.g. we could have started with (Id▽−Id) ≤ −Id.) By Theorem 4.9 above, in the language of fork algebras there is no finite set of axioms which would avoid the above outlined “looping”. The question comes up naturally whether there is an alternative to fork algebras which can avoid looping. Such an alternative is provided by the weakly higher order cylindric algebras of ternary relations in [26],[25]. These algebras provide a formalism strictly stronger than that of fork algebras where looping can be excluded by a single axiom.

Besides grupoids, there is a further way of “representing” pairing (i.e. fork), namely, by using trees (cf. e.g. [10], [39]). Finite trees will behave just as badly as SFA^{+} or free groupoids do, cf. Theorems 4.5– 4.4 above. Let us see if we can save our algebras by moving from finite trees to arbitrary (possibly infinite) trees.

Definition 4.10 (i) A pairing structure ⟨U, f⟩ is tree-like iff there is a transitive and irreflexive relation <⊆ U × U on U such that

(∀x, y ∈ U) (x < f(x, y) & y < f(x, y)).

We note that a pairing structure is tree-like iff the pair-forming behavior of f is not “circular” (like x = f(x, x) or x = f(f(x, y), y), etc.). Thus, a tree-like pairing structure is always loop-free.

(ii) By a Tree Fork Algebra (a TFA) we understand an NFA such that its pairing structure is tree-like. □

Since TFA ⊆ LFA, the following results are corollaries of Theorem 4.9.

COROLLARY 4.11 (in ZFC^{−}) Eq(TFA) is not finitely axiomatizable.

COROLLARY 4.12 (in ZFC^{−}) Let K ⊆ H S P TFA be such that there exists A ∈ K with A = P(U × U) for some U with |U| > 1. Then Eq(K) is not finitely axiomatizable.

5 The concatenation-version of Proper Fork Algebras

In this section we investigate a further candidate in the literature for playing the role of proper fork algebras, cf. Veloso–Haeberer [39].

Notation 5.1 For any set X, X^{∗} is the set of all finite sequences of elements of X. nil denotes the empty sequence. For any y, z ∈ X^{∗}, y^{∩}z denotes the concatenation of sequences y and z.

Definition 5.2 A = ⟨B, ▽^{c}⟩ is an SFA’91 iff B is an SRA with greatest element X^{∗} × X^{∗} for some set X, and

R▽^{c}S = {⟨x, y^{∩}z⟩ : xRy and xSz}. □

THEOREM 5.3 (in ZF^{−}) I SFA’91 and S P SFA’91 are not axiomatizable by any set of first order formulas. (They are not closed under taking ultraproducts, hence they are not even pseudo-axiomatizable.)

Proof. This proof is completely analogous with that of Theorem 4.7, therefore we omit it.

THEOREM 5.4 (in ZF^{−}) Eq(TPA) is interpretable in Eq(SFA’91) by a recursive translation function.

Proof. We define the derived constant E as follows.

E =^{def} Id ∩ (Id▽^{c}Id).

We note that E = {⟨nil, nil⟩} in SFA’91’s. Let p, q and y be variable symbols. Then the following properties can be expressed by equations in the language of SFA’91.

(a) y is rectangular, i.e., y = W × W for some set W;

(b) p and q are W → W partial functions;

(c) for all α, β ∈ W there exists a unique γ ∈ W with p(γ) = α and q(γ) = β; (d) p and q have the same domains, not containing the empty se-

quence nil;

(e) for all sequences α, β ∈ W, if p(α) = β or q(α) = β then there are sequences γ, δ ≠ nil such that α = γ^{∩}β^{∩}β^{∩}δ.

Indeed, let φ(p, q, y) be the conjunction of the following equations.

(1 ∘ y) ∩ (y ∘ 1) = y, p ∪ q ≤ y,

(p^{−1} ∘ p) ∪ (q^{−1} ∘ q) ≤ Id, (p ∘ p^{−1}) ∩ (q ∘ q^{−1}) ≤ Id,

p^{−1} ∘ q = y, (p ∘ y) ∩ Id = (q ∘ y) ∩ Id,

p ∪ q ≤ (1 − E)▽^{c}(Id▽^{c}Id)▽^{c}(1 − E).

For any A ∈ SRA and set W, we let

A_{W} =^{def} ⟨A ∩ (W × W), ∪, ∩, −_{W ×W} , ∅, W × W, ∘,^{−1}, Id ∩ (W × W)⟩.

Further, for any equation e in the language of SRA and variable y not occurring in e, we let e_{y} denote the equation obtained from e by replacing each subterm of form −τ with −τ ∩ y, and each occurrence of constant 1 and constant Id with y and Id ∩ y, respectively.

Then it is easy to see that for any SRA-equation e, having free variables from x_{1}, …, x_{n}, for any A ∈ SRA and a_{1}, …, a_{n}, W ×W ∈ A,

A_{W} ⊧ e[a_{1}, …, a_{n}] ⟺ A ⊧ e_{y}[a_{1}, …, a_{n}, W × W]. (7)

Now let e(x_{1}, …, x_{n}) be an arbitrary equation in the language of TPA. Let e^{pq} be the same equation but with p, q regarded as variable symbols. Then e^{pq} is in the language of SFA’91, having free variables p, q, x_{1}, …, x_{n}. Let y be a new variable and let ψ(e) be the following quasi-equation.

φ(p, q, y) ∧ x_{1} ≤ y ∧ … ∧ x_{n} ≤ y → e_{y}^{pq}(p, q, x_{1}, …, x_{n}, y).

Since SFA’91 is a discriminator class, any quasi-equation is equivalent with an equation. Thus, let the translation t(e) of e be an equation such that SFA’91 ⊧ ψ(e) ↔ t(e) holds.

Claim 5.4.1 For any equation e in the language of TPA,

TPA ⊧ e  ⟹  SFA’91 ⊧ t(e).

Proof of Claim 5.4.1. Assume A ∈ SFA’91 and p, q, a_{1}, …, a_{n}, b ∈ A are such that A |̸= t(e)[p, q, a_{1}, …, a_{n}, b]. Then, by properties (a)–(b), b = W × W for some set W, and p, q are W → W partial functions. Let κ be the cardinality of the set {w ∈ W : w ∉ Dom(p)}, let Z be the smallest set with κ ⊆ Z and Z × Z ⊆ Z. By (d)–(e), for each w ∈ Dom(p), the sequences p(w) and q(w) are strictly shorter than w. Therefore, by (c), there is a bijection f : W → Z such that

P =^{def} {⟨f(w), f(p(w))⟩ : w ∈ Dom(p)} and

Q =^{def} {⟨f(w), f(q(w))⟩ : w ∈ Dom(p)}

are the standard projections on set Z. Let A^{0} denote the SRA-type reduct of A. Then, the function f above can be extended to a baseisomorphism f̃ : A_{W}^{0} → B for some B ∈ SRA with base Z such that f̃(p) = P and f̃(q) = Q hold. Therefore ⟨B, P, Q⟩ ∈ TPA. Now

A |̸= t(e)[p, q, a_{1}, …, a_{n}, W × W]

⇓

A |̸= e_{y}^{pq}[p, q, a_{1}, …, a_{n}, W × W]

⇓

A^{0} |̸= e_{y}^{pq}[p, q, a_{1}, …, a_{n}, W × W]

⇓ by (7)

A_{W}^{0} |̸= e^{pq}[p, q, a_{1}, …, a_{n}]

⇓ f̃ is an isomorphism B |̸= e^{pq}[P, Q, f̃(a_{1}), …, f̃(a_{n})]

⇓ ⟨B, P, Q⟩ |̸= e[f̃(a_{1}), …, f̃(a_{n})]

⇓ ⟨B, P, Q⟩ ∈ TPA TPA |̸= e. (Claim 5.4.1)

Claim 5.4.2 For any equation e in the language of TPA,

SFA’91 ⊧ t(e)  ⟹  TPA ⊧ e.

Proof of Claim 5.4.2. Assume A ∈ TPA with base U, a_{1}, …, a_{n} ∈ A and A |̸= e[a_{1}, …, a_{n}]. Let U_{0} be the set for which U is the smallest set with U_{0} ⊆ U and U × U ⊆ U − U_{0}. We may assume that U_{0} is such that

({⊢, ⊣} ∪ (U_{0} ∪ {⊢, ⊣})^{∗}) ∩ U_{0} = ∅.  (8)

Now let V =^{def} U_{0} ∪ {⊢, ⊣}, and let

B =^{def} ⟨P(V^{∗} × V^{∗}), …, ▽^{c}⟩ ∈ SFA’91.

We define a function f : U → V^{∗} as follows.

f(u) =^{def} ⟨u⟩ for all u ∈ U_{0}  (9)
f(⟨a, b⟩) =^{def} ⟨⊢⟩^{∩}f(a)^{∩}f(a)^{∩}f(b)^{∩}f(b)^{∩}⟨⊣⟩  (10)

(here e.g. ⟨⊢⟩ is the 1-long sequence consisting of ⊢). Let W be the range of f. Then it is easy to see that, by (8) above, f is a bijection from U to W. Therefore it extends to a base-isomorphism f̃: A^{0} → B_{W}^{0} (where A^{0} and B^{0} are the SRA-type reducts of A and B). Now let p and q be the standard projections on U. Then

A |̸= e[a_{1}, …, a_{n}]

⇓

A^{0} |̸= e^{pq}[p, q, a_{1}, …, a_{n}]

⇓ f̃ is an isomorphism B_{W}^{0} |̸= e^{pq}[f̃(p), f̃(q), f̃(a_{1}), …, f̃(a_{n})]

⇓ by (7)

B^{0} |̸= e_{y}^{pq}[f̃(p), f̃(q), f̃(a_{1}), …, f̃(a_{n}), W × W]

⇓

B |̸= e_{y}^{pq}[f̃(p), f̃(q), f̃(a_{1}), …, f̃(a_{n}), W × W]  (11)

On the other hand, it is easy to show that f̃(p) and f̃(q) have properties (b)–(e) above (w.r.t. W) in algebra B. Therefore

B ⊧ φ[f̃(p), f̃(q), W × W]

holds. Thus, by (11), B |̸= t(e), proving SFA’91 |̸= t(e). (Claim 5.4.2)

Now Claims 5.4.1–5.4.2 together prove Theorem 5.4.

THEOREM 5.5 (in ZFC^{−}) The equational theory Eq(SFA’91) of SFA’91 is Π_{1}^{1}-hard.

Proof. This follows from Theorems 4.4 and 5.4 above.

COROLLARY 5.6 (in ZFC^{−})

(i) Eq(SFA’91) is not finitely axiomatizable.

(ii) The quasi-equational theory of SFA’91 is not finitely axiomatizable.

(iii) The universal theory of SFA’91 is not finitely axiomatizable.

6 Positive results

If we do not insist on our non-well-founded set theory being strongly extensional then some positive results can be achieved. Let U be a set and let E be a binary relation on U, i.e., E is a set with E ⊆ U ×U. The structure ⟨U, E⟩ is called extensional if it satisfies the usual extensionality axiom:

(∀x, y ∈ U)[(∀z ∈ U)(⟨z, x⟩ ∈ E ⇔ ⟨z, y⟩ ∈ E) ⇒ x = y].

Boffa’s weak anti-foundation axiom (BAFA_{0}) is the following:

(BAFA_{0}) Every extensional structure is isomorphic to the ‘set theoretical ∈-structure’ of some transitive set. That is,

(∀ set U)(∀ set E ⊆ U × U)

(⟨U, E⟩ is extensional ⇒ (∃ transitive W) ⟨U, E⟩ ≅ ⟨W, ∈_{W} ⟩),

where ∈_{W} = {⟨x, y⟩ ∈ W × W : x ∈ y}.

THEOREM 6.1 (Aczel [1]) ZFC^{−}+BAFA_{0} is consistent if ZFC^{−} is consistent.

Proof. Our formulation of BAFA_{0} is denoted by BA1 in Aczel [1]. Boffa’s Anti-foundation Axiom BAFA is formulated on p.59, and Exercise 5.14 on p.65 states that BAFA implies BA1. On p.61 it is stated that ‘BAFA holds in the universe iff the universe is superuniversal’ (see p.13 for the definition of a system, and p.59 for superuniversality). Theorem 5.9 on p.61 states that every superuniversal system is full (see p.34 for definition). Rieger’s theorem on p.119 states that any full system is a class model of ZFC^{−}. Finally, Theorem 5.18 on p.66 states that, assuming that there is a definable well-ordering of the universe (i.e. V is isomorphic to On, the class of all ordinals), there exists a superuniversal system. Since the assumption V ≅ On holds in the constructible universe L, and V = L is consistent with ZFC^{−}, the consistency of ZFC^{−}+BAFA_{0} with ZFC^{−} is proved.

THEOREM 6.2 In any set theory in which ZFC^{−}+BAFA_{0} is provable we have that S P SFA and S P SPA are finitely axiomatizable varieties.

Proof. It is in [26], cf. also [25].

COROLLARY 6.3 The finite axiomatizability of S P SFA and S P SPA is independent from ZFC^{−}.

We note that BAFA_{0} can be interpreted as an axiom stating existence of certain kinds of sets. Hence one can interpret our results as saying that strong representability of fork algebras depends on what kind of ontology we choose to use. If our ontology is rich enough then we will have positive representability results by the above theorems. If we prefer Occham’s razor in the form of axiom SEX then we will have no such results by sections 2, 4 and 5. The crucial question seems to be whether we permit the existence of sets which are different from each other but are not distinguishable in the language of pure set theory. (An example of permitting such existence is provided by set theories with “urelements”.)

There is a striking difference between the classes of algebras SFA, SPA on the one side and the classes of algebras TPA, SFA^{+}, GFA, SFA’91 on the other side, as the following theorem shows.

THEOREM 6.4 (in ZFC^{−}+BAFA_{0}) Let K ∈ {TPA, SFA^{+}, GFA, SFA’91}. Then Eq(K) is Π_{1}^{1}-hard (thus it is not finitely axiomatizable).

Proof. It is an obvious corollary of Theorems 4.4 and 5.5.

If we do not insist on binary relations and on the language of fork algebras then there are positive results even in ZFC. Instead of only binary relations, consider all possible finitary relations over some set U. Let us consider the possible algebras of these.

Notation 6.5 Ref (U) is the set of all finitary relations over U, i.e.

Ref (U) =^{def} {R : for some finite n, R is an n-ary relation over U}. □

THEOREM 6.6 (in ZFC) ( [28], [27]) It is possible to define set theoretic operations f_{1}, …, f_{9} on finitary relations such that (i)–(iii) below hold.

(i) The variety REL generated by the class

{⟨Ref (U), f_{1}, …, f_{9}⟩ : U is a set}

is finitely axiomatizable.

(ii) First order logic is expressible in the equational language of REL.

(iii) The operations f_{1}, …, f_{9} of REL are logical in the sense of Tarski– Givant [38].

Remark 6.7 There is a version of the above theorem where the set algebras already form a variety, so we do not have to generate a variety in this version of (i). This latter version as well as Theorem 6.6 above are in [27] and in [28]. Cf. also [29] for recent developments in this direction. □

ACKNOWLEDGEMENT: We would like to thank Ewa Orlowska for calling our attention to the “Fork Algebra paper” [39] during the 1991 Warsaw Banach Semester. Thanks are due to Hajnal Andréka, Steven Givant, Viktor Gyuris, Ágnes Kurucz and András Simon for careful reading and helpful suggestions. Special thanks are due to Ágnes Kurucz for extensive help in preparing the final version of this paper. We would like to thank those members of the Algebraic Logic seminar and the Non-well-founded Sets seminar who double-checked the proofs of these results (remaining mistakes are our fault, not theirs).

References

[1] P. Aczel. Non-well-founded Sets. CSLI Lecture Notes No.14, 1988.

[2] H. Andréka, S. Givant, and I. Németi. Decision problems for equational theories of relation algebras. Memoirs of the American Mathematical Society, to appear.

[3] H. Andréka, S. Givant, and I. Németi. Decision problems for equational theories of relation algebras. Bull. of the Section of Logic, Univ. of Łódz, 23(2):47–52, 1994.

[4] H. Andréka, B. Jónsson, and I. Németi. Free algebras in discriminator varieties. Algebra Universalis, 28:401–447, 1991.

[5] H. Andréka, Á. Kurucz, and I. Németi. Connections between axioms of set theory and basic theorems of universal algebra. Journal of Symbolic Logic, 59, 3:912–922, 1994.

[6] H. Andréka, J. D. Monk, and I. Németi (editors). Algebraic Logic (Proc. Conf. Budapest 1988). Colloq. Math. Soc. J. Bolyai Vol 54, North-Holland, Amsterdam, 1991.

[7] J. Barwise and J. Etchemendy. The Liar. Oxford University Press, 1989.

[8] G. A. Baum, M. F. Frías, A. M. Haeberer, and P. E. M. López. From specifications to programs: a fork algebraic approach to bridge the gap. In Document 731-HKO-4, 47th Meeting of the IFIP Working Group 2.1 “Algorithmic Languages and Calculi”; Hong Kong, January 1995.

[9] G. A. Baum, M. F. Frías, A. M. Haeberer, and P. E. M. López. From specifications to programs: a fork algebraic approach to bridge the gap. Technical Report, Pontifícia Universidade Católico do Rio de Janeiro, 1994.

[10] G. A. Baum, A. M. Haeberer, and P. A. S. Veloso. On the representability of the ▽-abstract relational algebra. IGPL Newsletter, 1(3):3–4, 1992.

[11] R. Berghammer, A. M. Haeberer, A. M. Schmidt, and P. A. S. Veloso. Comparing two different approaches to products in abstract relation algebras. In T. Rus M. Nivat, C. Rattray and G. Scollo, editors, Algebraic Methodology and Software Technology (AMAST’93) (Proceedings of the Third International Conference on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21-25 June 1993), Springer-Verlag, London, 1993.

[12] B. Biró. Non-finite-axiomatizability results in algebraic logic. Journal of Symbolic Logic, 75(2):832–843, 1992.

[13] C. Brink and G. Schmidt (organizers). Relational methods in computer science. In Dagstuhl Seminar 9403, Jan. 17–21, 1994.

[14] T. E. Forster. Set theory with a universal set. Volume 20 of Oxford Logic Guides, Oxford Science Publications, 1992.

[15] M. Frías, G. A. Baum, A. M. Haeberer, and P. Veloso. A Representation Theorem for Fork Algebras. Technical Report, Universidad de Buenos Aires, Dept. de Compuyación, 1993.

[16] V. Gyuris. A short proof for representability of fork algebras. Journal of the IGPL, 5(3):791–796, 1995.

[17] A. M. Haeberer and P. A. S. Veloso. Partial relations for program derivation: adequacy, inevitability and expressiveness. In Bernhard Möller, editor, Constructing programs from specifications, pages 319–371, 1991. Proc. of the IFIP TC2 Working Conference on Constructing Programs from Specifications, N.H., IFIP WG 2.1.

[18] L. Henkin, J. D. Monk, and A. Tarski. Cylindric Algebras Parts I and II. North-Holland, Amsterdam, 1971 and 1985.

[19] R. D. Maddux. Finitary algebraic logic Part II. Mathematical Logic Quarterly, 39:566–569, 1993.

[20] R. D. Maddux. Sufficient conditions for representability of relation algebras. Algebra Universalis, 8:162–172, 1978.

[21] R. N. McKenzie, G. F. McNulty, and W. F. Taylor. Algebras, Lattices, Varieties, Vol I. The Wadsworth and Brooks/Cole Mathematics Series, Monterey, California, 1987.

[22] Sz. Mikulás, I. Sain, and A. Simon. Complexity of equational theory of relational algebras with projection elements. Bull. of the Section of Logic, Univ. of Łódz, 21(3):103–111, 1992. Full paper is [33].

[23] I. Németi. Algebraizations of quantifier logics: an overview (version 11.2). Technical report, Math. Inst. Budapest, 1991. A short version without proofs appeared in Studia Logica, 50(3/4):485–569, 1991.

[24] I. Németi. Free Algebras and Decidability in Algebraic Logic. Dissertation for D.Sc. with Hung. Academy of Sciences, Budapest, 1986. In Hungarian.

[25] I. Németi. Ontology can turn negative results to positive. Technical Report, Math. Inst. Budapest, 1995. Extended abstract is to appear in Bull. of the Section of Logic, Univ. of Łódz.

[26] I. Németi. Strong representation theorem for fork algebras, a set theoretical foundation. Journal of the IGPL, to appear.

[27] I. Sain. On the problem of finitizing first order logic and its algebraic counterpart (a survey of results and methods). In L. Csirmaz, D.M. Gabbay, and M. de Rijke, editors, Logic Colloquium ’92, pages 243–292, CSLI Publications, 1995.

[28] I. Sain. On the Search for a Finitizable Algebraization of First Order Logic (Shortened Version A). Technical Report, Math. Inst. Budapest, 1988.

[29] I. Sain and V. Gyuris. Finite schematizable algebraic logic. Journal of the IGPL, to appear.

[30] I. Sain and I. Németi. Fork algebras in usual as well as in non-well-founded set theories. SIGALA (Special Interest Group of Algebraic Logic and its Applications) Newsletter, 2(1), April 1994.

[31] I. Sain and I. Németi. Fork algebras in usual as well as in non-well-founded set theories (abstract). In Relational Methods in Computer Science, Dagstuhl Seminar 9403, pages 17–19, 1994.

[32] I. Sain and I. Németi. Fork algebras in usual as well as in nonwell-founded set theories (extended abstract), parts I and II. Bull. of the Section of Logic, Univ. of Łódz, 24(3,4):158–168, 182–192, 1995.

[33] I. Sain and A. Simon. The Complexity of Equational Theory of Relational Algebras with Projection Elements. Technical Report, Math. Inst. Budapest, 1991.

[34] A. Simon. A purely algebraic proof of representability of quasiprojective relation algebras (QRA’s). Technical Report, Math. Inst. Budapest, 1995.

[35] A. Simon. What the finitization problem is not. In Algebraic Methods in Logic and in Computer Science (Proceedings of the ’91 Banach Semester, Banach Center), pages 95–116, Polish Academic Publishers, Banach Center Publications, Volume 28, Warsaw, 1993.

[36] A. Tarski. Collected Papers, Volumes 1–4. Birkhäuser (Basel– Boston–Stuttgart), 1986. Editors: S.R. Givant and R.N. McKenzie.

[37] A. Tarski. Some metalogical results concerning the calculus of relations. In [36] Volume 4, pages 603–604. Originally appeared in the Journal of Symbolic Logic, 18:188–189, 1953.

[38] A. Tarski and S. Givant. A Formalization of Set Theory Without Variables. Volume 41 of AMS Colloquium Publications, Providence, Rhode Island, 1987.

[39] P. A. S. Veloso and A. M. Haeberer. A finitary relational algebra for classical first-order logic. Bull. of the Section of Logic, Univ. of Łódz, 20(2):52–62, June 1991.

[40] P. A. S. Veloso and A. M. Haeberer. A new algebra of first-order logic. In Methodology and Philosophy of Science, 1991. 9th International Congress on Logic, Upsala, Sweden.

[41] P. A. S. Veloso, A. M. Haeberer, and G. A. Baum. Formal Program Construction within an Extended Calculus of Binary Relations. Technical Report 19, MCC, 1992. Submitted to a special issue on Automatic Programming in the Journal of Symbolic Computation.

Mathematical Institute of the Hungarian Academy of Sciences Budapest, P.O. Box 127 H–1364, Hungary e-mail: sain@math-inst.hu

nemeti@math-inst.hu