Representability of Pairing Relation Algebras Depends on your Ontology

Ágnes KURUCZ and István NÉMETI ^{∗} Math. Inst. of Hung. Acad. Sci. Budapest, P.O.B. 127., H–1364 Hungary e-mail: kuag@math-inst.hu, nemeti@math-inst.hu

April 25, 1997

Abstract

We consider classes of relation algebras expanded with new operations based on the formation of ordered pairs. Examples for such algebras are pairing (or projection) algebras of algebraic logic and fork algebras of computer science. It is proved in Sain–Németi [36] that there is no ‘strong’ representation theorem for all abstract pairing algebras in most set theories including ZF C as well as most non-well-founded set theories. Such a ‘strong’ representation theorem would state that every abstract pairing algebra is isomorphic to a set relation algebra having projection elements which are defined with the help of the real (set theoretic) pairing function. Here we show that, by choosing an appropriate (non-well-founded) set theory as our metatheory, pairing algebras and fork algebras admit such ‘strong’ representation theorems.

1 Introduction

This paper is about representation (or axiomatization) problems of algebraic logic. In particular, we discuss the representation problem of classes of relation algebras expanded with extra operations based on the formation of ordered pairs. Our results are also related to completeness problems of finite variable fragments of first order logic. In the present paper we prove that in a particular non-well-founded set theory, a natural variant of these expanded relation algebras admits a so called ‘strong representation theorem’. We will also see that for such a theorem we need this particular variant of our algebras as well as this particular choice of set theory. Namely: (i) the other variants which came up in the literature do not admit a strong representation theorem even in this set theory, and (ii) all known variants (including ours) of these algebras behave badly in many other set theories (non-well-founded as well as well-founded ones). This way this paper can also be considered as a contribution to the field of so called ‘reverse mathematics’ or ‘inverse set theory’, cf. e.g. Simpson [39], Andréka et al [4]. In this field one tries to find out what is the exact fragment of background set theory really needed to prove some theorems of certain mathematical disciplines, in our case theorems of algebraic logic.

The motivation for studying relation algebras expanded with extra operations based on forming ordered pairs comes from the following two areas (or ‘traditions’).

(1) In Tarskian algebraic logic, these kinds of algebras are called ‘relation algebras with projection elements’ or ‘pairing relation algebras’. They have been studied beginning with the early 1940’s, when Tarski observed that certain theories of first-order logic with countably many variables are ‘algebraizable’ with the help of relation algebras having ‘projection elements’ (Tarski [40], Tarski–Givant [41], Maddux [20]). The ‘projection elements’ were taken as distinguished constants of the similarity type in Németi [27], Andréka–Jónsson–Németi [3], Maddux [21], [22], Mikulás–Sain–Simon [26], Sain–Simon [37].

∗Research supported by Hungarian National Foundation for Scientific Research grants No T7567, No T16448 and No F17452. Á.Kurucz is also supported by a grant from Logic Graduate School, Eötvös Loránd University Budapest. We are grateful to the referee for a very careful reading and her/his helpful remarks.

(2) Recently in computer science, these kinds of expanded relation algebras were found useful in various ways (e.g. in the theory of programming). Therefore they have been studied in the computer science literature extensively, cf. Veloso–Haeberer [42], [43], [16], Baum–Haeberer– Veloso [7], Berghammer et al [8], Frias et al [9], Baum et al [6], Frias–Gordillo [10]. The name ‘fork algebra’ was suggested in computer science for a relatively comprehensive class, where relation algebras are expanded with a binary operation (based on pairing) called ‘fork’.

Analogously to the situation with Boolean algebras, groups, semigroups, polyadic algebras etc., one can contemplate the idea of developing a representation theory for the above kinds of expanded relation algebras, too. Desirability of a representation theory also comes from logic (cf. section 5 for a discussion). By the above analogy, such a representation theory would consist of

• defining a concrete class of algebras, i.e. where the universe of an algebra completely determines the operations of the algebra (analogously to Boolean set algebras, transformation semigroups, polyadic set algebras, etc.); and

• an axiomatic (abstract) class of algebras, defined by finitely many first-order formulas (preferably equations) valid in the concrete class; and then

• a strong representation theorem^{1} stating that every member of the abstract class is isomorphic to a member of the concrete class.

Both traditions (1) and (2) above mention as standard examples those expanded set relation algebras in which the extra operations (based on pairing) are based on the standard set theoretic definition of ordered pairs ⟨a, b⟩ =^{def} {{a}, {a, b}}. These algebras are concrete in the above sense: given such an algebra A, to each operation g of A (in particular, to the extra operation [fork or the projections] based on pairing) there is an explicit set theoretic definition of g using no other parameter than A (see sections 2 and 3 for definitions). Therefore it would be nice to find an axiomatic (abstract) class of, say, fork algebras such that their representation theory could be based on these standard algebras. This was indeed experimented with in the earlier papers of the computer science tradition, cf. e.g. Haeberer et al [7], [16], [42], [15]. Several variants of ‘standard’ algebras were introduced and studied in the literature, e.g. in Németi [27], Andréka–Jónsson– Németi [3], Veloso–Haeberer [43], Baum–Haeberer–Veloso [7], Maddux [21], [22], Sain–Németi [36]. For all of these variants, it was proved in Sain et al [36], [34], [32], [37], [26] that if one uses the usual Zermelo-Fraenkel set theory ZF C as his metatheory then this task cannot be solved for the following reason. The equational theories of these concrete classes are not finitely axiomatizable; further, these concrete classes are not axiomatizable by any set of first-order formulas. (There are even further negative results in the quoted papers, see section 4 for a summary.) These results hold if one works in our usual set theory ZF C as metatheory.

This might look discouraging, but if we are motivated by computer science applications of fork algebras, then the idea comes up that there might be alternative set theories to ZF C which are just as suitable for computer science as ZF C is. Indeed, Aczel [1] and Barwise–Etchemendy [5] discuss many so called non-well-founded set theories which are suitable for computer science, for theories of natural language as well as for parts of Philosophical Logic. These set theories are obtained from ZF C by dropping the Axiom of Foundation and adding some new axioms to replace it. It was also proved in Sain–Németi [36] that for many of these non-well-founded set theories the above quoted negative results carry over (for all variants of concrete classes of expanded relation algebras in the literature). In the present paper we discuss a particular non-well-founded set theory, denoted here as ZF C^{−} +BAF A_{0}, and we look at some particular concrete classes of expanded relation algebras (see Defs. 4 and 10 below), such that in our set theory our concrete classes are axiomatizable by finitely many equations. Thus we can provide an abstract class of, say, fork algebras, defined by finitely many equations such that every member of the class can be strongly represented. On the other hand, by [36], even our classes behave ‘badly’ in ZF C as well as in many other non-well-founded set theories. (Our concrete classes are exceptional in the sense that the other variants in the literature remain non-finitely axiomatizable even in ZF C^{−} + BAF A_{0}.) The results of this paper were announced in [30].

1There are cases when strong representation theorems are not available, and therefore so called weak representation theorems are used as a substitute. These representation theorems are called weak because the class K of algebras they use to represent an abstract class is not concrete in the sense defined above. In the case of fork algebraic weak representation theorems, all the relation algebraic operations are represented in a concrete way, but the extra operation ‘fork’ based on pairing remains abstract in the sense that it is represented only via some abstract class of groupoids, which cannot be recovered from the universes of the algebras in question, cf. Gyuris [13], [14], Sain–Németi [36], Baum et al [6]. Weak and strong representation theorems were discussed and carefully compared in detail (with examples from the literature) in e.g. Sain–Németi [36], Henkin–Monk–Tarski [17, pp.459–461, item 2.7.46].

For completeness, we note that the word ontology in the title refers to the fact that the antifoundation axiom used in this paper states the existence of certain kinds of sets. Therefore, at least in a sense, accepting or rejecting this axiom might depend on one’s ontological commitment. (The basic question seems to be whether we want to have sets which are different from one another but undistinguishable in the language of set theory.) In this connection, we note that we are under the impression that one can do ‘ordinary mathematics’ in ZF C^{−} + BAF A_{0} reasonably comfortably^{2}.

The paper is structured as follows. In section 2 we introduce the particular non-well-founded set theory ZF C^{−} + BAF A_{0} we use as our metatheory. We state, in ZF C^{−} + BAF A_{0}, our main technical lemma about the characterization of set theoretical projection functions. We introduce the various classes of expanded relation algebras and discuss their strong representation theory in ZF C + BAF A_{0}. We also prove that the approaches (1) and (2) above can be considered as equivalent ones in a very strong sense. Section 3 is devoted to some properties of our metatheory ZF C + BAF A_{0}, and to the proof of our main lemma. Section 4 gives a detailed summary of the negative results achieved in the above quoted papers of Sain et al. Section 5 discusses the connections with the so called ‘finitization problem’ of algebraic logic. We also discuss briefly some motivations coming from logic.

2 Representing relation algebras expanded with operations based on forming ordered pairs

In this section we develop a representation theory for some classes of expanded relation algebras. Since the validity of the statements may depend on the metatheory used, we carefully indicate, after the number of each theorem and claim, the meta (set)theory in which the theorem in question is proved. In particular, ZF C denotes Zermelo-Fraenkel Set Theory with the Axiom of Choice (which includes the Axiom of Foundation) and ZF C^{−} is ZF C without the Axiom of Foundation. We do not even assume the Collection Principle as an axiom of ZF C^{−} (which is used as an axiom of non-well-founded set theories in Aczel [1]). We use ZF and ZF^{−} similarly for set theories without the Axiom of Choice.

2As it is proved in section 3, if ZF C is consistent then the set theory BAF A_{0}^{+} =^{def} (ZF C^{−} + BAF A_{0} + collection principle) is consistent, too. Since our theorems are proved in ZF C^{−} + BAF A_{0} as metatheory, they also remain true in BAF A_{0}^{+}. We mention this because, on the basis of [4], we conjecture that practically all theorems in e.g. the textbook Grätzer [12] are true in BAF A_{0}^{+} (in place of ZF C). We believe that we have a proof that all the “isomorphism invariant” theorems of universal algebra and abstract algebra are equi-provable in ZF C and BAF A_{0}^{+}. We think that these equi-provability results can be pushed far beyond “isomorphism invariance”, e.g. we checked that the known non-finitizability results of algebraic logic (cf. [28], [2]) also remain true in BAF A_{0}^{+}.

E.g. the class of representable relation algebras remains non-finitely axiomatizable in BAF A_{0}^{+}.

Notation 1 ⟨x, y⟩ denotes the usual set theoretic ordered pair of x and y, i.e. ⟨x, y⟩ =^{def} {{x}, {x, y}}. For any set U, U×U =^{def} {⟨x, y⟩ : x, y ∈ U}. A binary relation on U is some subset of U×U. For any binary relation E, dom E denotes the domain of E that is, dom E =^{def} {a : ⟨a, b⟩ ∈ E for some b}. We consider functions as special binary relations. A partial function on some set U is a function f with dom f ⊆ U. In case of some partial function f we will use notation f(a) = b instead of writing ⟨a, b⟩ ∈ f.

For any class K of algebras, I K, SK and PK denote, respectively, the classes of all isomorphic copies, of subalgebras, and of isomorphic copies of direct products of members of K. □

DEFINITION 2 An algebraic structure A = ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′⟩ is a relation algebra if equations (R0)–(R7) below are valid in A (cf. e.g. Henkin–Monk–Tarski [18], or Tarski–Givant [41]).

(R0) the Boolean algebraic equations for +, ·, 1, 0, and −

(R1) (x ; y) ; z = x ; (y ; z)

(R2) (x + y) ; z = (x ; z) + (y ; z)

(R3) x ; 1′ = x

(R4) x˘ ˘ = x

(R5) (x + y)˘ = x˘ + y˘

(R6) (x ; y)˘ = y˘ ; x˘

(R7) x˘ ; [−(x ; y)] ≤ −y

A relation algebra A is called a set (or proper) relation algebra if A is a set of binary relations on some set U and the operations +, ·, 1, 0, −, ; ,˘ , 1′ coincide with the usual set theoretic operations of union, intersection, ⋃ A, empty set, complementation relative to ⋃ A, relation composition, converse, and the identity relation on U, respectively. The set U is called the base of A. ⋃ A (which is, being the biggest element of A, always an equivalence relation with domain U) is called the unit^{3} of A. If A consists of all the subsets of U × U then A is called a full set relation algebra. □

Recall that a representation theory usually consists of

• defining a concrete class of algebras, i.e. where the universe of an algebra determines every operation of the algebra in question;

• an axiomatic (abstract) class of algebras, defined by finitely many first-order formulas (preferably equations) valid in the concrete class; and then

• a strong representation theorem stating that every member of the abstract class is isomorphic to a member of the concrete class.

In this sense, the class of relation algebras is an abstract class, while the class of set relation algebras is a concrete one. Thus we call a relation algebra representable if it is isomorphic to a set relation algebra.

An abstract subclass of relation algebras can be given as follows. A relation algebra A is called a QRA (cf. Tarski–Givant [41])^{4} iff the following (existential) formula is valid in A.

∃p∃q (p˘ ; p ≤ 1′ ∧ q˘ ; q ≤ 1′ ∧ p˘ ; q = 1)

Such elements p, q are called quasi-projections of A.

THEOREM 3 [Tarski]^{5} (in ZF C^{−}) Every QRA is representable.

3If A is simple then the unit of A can be taken to be U × U, cf. [17], [18].

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

5In 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. [41, pp.xvi line 6 bottom up–xvii line 12, and footnote 3 on p.168].

Proof. The proof can be found e.g. in Tarski–Givant [41] or in Maddux [20], see also Simon [38]. Those proofs are done in ZF C, but it can be checked that they do not use the Axiom of Foundation. We note that for countable QRA’s, the Axiom of Choice is not needed in the proof either.

This theorem is a strong representation theorem in the above sense, since all the operations are represented in a concrete way. However, one can expand the similarity type with the constant symbols p and q, as it is done in Németi [27], Andréka–Jónsson–Németi [3], Maddux [20], [21], [22], Mikulás–Sain–Simon [26], Sain–Simon [37]. That is, let

K =^{def} {⟨A, p, q⟩ : A is a QRA, and p, q are quasi-projections of A}.

Then Tarski’s theorem does not imply that every member of K is strongly representable. Though, in the representing set relation algebras, quasi-projections p and q are partial functions with p˘ ; q = 1, their behaviour cannot be ‘found out of’ the universe of the algebra, they can be any pair of partial functions on the base of the algebra in question which satisfy p˘ ; q = 1. However, if such an algebra belonged to some concrete class then its universe would have to determine p and q in a unique way.

We want to find classes of algebras which will be candidates for being concrete classes in a representation theory of relation algebras expanded with quasi-projections. To this end, for any set U one can define the binary relations

P_{U} =^{def} {⟨⟨u, x⟩, u⟩ : u ∈ U, ⟨u, x⟩ ∈ U}, and

Q_{U} =^{def} {⟨⟨x, u⟩, u⟩ : u ∈ U, ⟨x, u⟩ ∈ U}.

P_{U} and Q_{U} are called the left and right projections on U, respectively. The structure ⟨U, P_{U}, Q_{U}⟩ is called the projection structure of U.

We say that an equivalence relation E on some set U is closed if whenever ⟨u, v⟩ ∈ E then ⟨⟨u, v⟩, u⟩ ∈ E also holds. (This implies that also ⟨⟨u, v⟩, v⟩ ∈ E, since E is an equivalence relation.) We note that if there is some closed E on U then U must be closed under forming ordered pairs ‘relative to’ E that is, for any u, v ∈ U, if ⟨u, v⟩ ∈ E then ⟨u, v⟩ ∈ U must hold. On the other hand, if E ⊆ U × U is closed then U is not necessarily closed under the projections P_{U} and Q_{U} that is, there can be some ⟨u, v⟩ ∈ U such that u ∉ U and/or v ∉ U. But if ⟨u, v⟩ ∈ E holds then closedness requires not only u, v ∈ U but the stronger ⟨⟨u, v⟩, u⟩, ⟨⟨u, v⟩, v⟩ ∈ E.

The following classes of algebras were suggested first in [27].

DEFINITION 4 An algebra A = ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′, p, q⟩ is called a partial projection set algebra (a SetPPA) if conditions (i)–(iii) below hold.

(i) ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′⟩ is a set relation algebra, say with base U and unit E;

(ii) E is closed;

(iii) p = P_{U} ∩ E = {⟨⟨u, x⟩, u⟩ ∈ E : u ∈ U, ⟨u, x⟩ ∈ U} q = Q_{U} ∩ E = {⟨⟨x, u⟩, u⟩ ∈ E : u ∈ U, ⟨x, u⟩ ∈ U}.

That is, p and q are the projections on U, restricted (as relations) to the binary relation E.

A partial projection set algebra is called a projection set algebra (a SetPA) if dom p = dom q also holds. Thus SetPA ⊆ SetPPA clearly holds. □

Claim 5 (in ZF^{−}) If ⟨A, p, q⟩ is a projection set algebra (with base U and unit E) then

p = {⟨⟨u, v⟩, u⟩ : ⟨u, v⟩ ∈ E}, and

q = {⟨⟨u, v⟩, v⟩ : ⟨u, v⟩ ∈ E}.

Proof. p = P_{U} ∩ E ⊇ {⟨⟨u, v⟩, u⟩ : ⟨u, v⟩ ∈ E}, because E is closed. For the other inclusion, assume that ⟨⟨u, v⟩, u⟩ ∈ E for some ⟨u, v⟩, u ∈ U. Then ⟨u, v⟩ ∈ dom (P_{U} ∩ E) = dom (Q_{U} ∩ E), thus ⟨⟨u, v⟩, v⟩ ∈ (Q_{U} ∩ E) ⊆ E. Therefore, since E is an equivalence relation, ⟨u, v⟩ ∈ E also holds. Similar argument works for q.

The classes SetPA and SetPPA are certainly concrete classes. However, as it is proved in Sain– Németi [36], in ZF C these classes cannot support a representation theory. It is shown in [36] that the equational theories of the classes SetPPA and SetPA are not finitely axiomatizable (cf. section 4 below). Roughly speaking, these negative results are ‘due to’ the fact that the Axiom of Foundation does not allow the existence of ‘not nice’ projection structures. E.g. an infinite p-chain u_{0} →^{p} u_{1} →^{p} u_{2} →^{p} … would result in an infinite descending ∈-chain u_{0} ∋ {u_{1}} ∋ u_{1} ∋ {u_{2}} ∋ …, thus it cannot exist in ZF C. Therefore the idea comes up to experiment with non-well-founded set theories where such objects do exist. The anti-foundation axiom we introduce below postulates the existence of as many non-well-founded sets as possible without harming the Axiom of Extensionality.

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 Axiom of Extensionality of ZF C:

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

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

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

(∀ set U)(∀ set E ⊆ U × U)
(⟨U, E⟩ is extensional ⇒ (∃ transitive W) ⟨U, E⟩ is isomorphic to ⟨W, ∈_{W} ⟩),

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

Now we show that, in ZF C^{−} + BAF A_{0}, both I SetPPA and I SetPA are axiomatizable by finitely many equations. To this end, we define a partial projection algebra (a PPA) to be an algebra A = ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′, p, q⟩ satisfying equations (P0)–(P4) below.

(P0) (R0)–(R7)

(P1) p˘ ; p ≤ 1′

(P2) q˘ ; q ≤ 1′

(P3) (p ; p˘ ) · (q ; q˘ ) ≤ 1′

(P4) p˘ ; q = 1

THEOREM 6 (in ZF C^{−} + BAF A_{0}) Every partial projection algebra is representable that is, it is isomorphic to some partial projection set algebra. Consequently,

PPA = I SetPPA

that is, the class of representable partial projection algebras is axiomatizable by finitely many equations, namely by (P0)–(P4).

Before proving the theorem we discuss some standard properties of projection structures.

(p1) P_{U} is a partial function on U.

(p2) Q_{U} is a partial function on U.

(p3) For any a, b ∈ (dom P_{U} ∩ dom Q_{U}), if P_{U}(a) = P_{U}(b) and Q_{U}(a) = Q_{U}(b) hold then a = b.

Claim 7 (in ZF^{−}) Let A be a set relation algebra with base U and unit E, and let p, q ∈ A. Then

(i) p˘ ; p ≤ 1′ holds in A iff p satisfies (p1) i.e., p is a partial function on U;

(ii) q˘ ; q ≤ 1′ holds in A iff q satisfies (p2) i.e., q is a partial function on U; (iii) (p ; p˘ )·(q ; q˘ ) ≤ 1′ holds in A iff p and q satisfy (p3) i.e., for any u, v ∈ (dom p∩dom q),

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

if there are some w, z ∈ U such that ⟨u, w⟩, ⟨v, w⟩ ∈ p and ⟨u, z⟩, ⟨v, z⟩ ∈ q then u = v;

(iv) p˘ ; q = 1 holds in A iff (∀⟨u, v⟩ ∈ E) (∃w ∈ U) ⟨w, u⟩ ∈ p and ⟨w, v⟩ ∈ q;

(v) p ; 1 = q ; 1 holds in A iff (∀u ∈ U) [(∃v ∈ U)⟨u, v⟩ ∈ p ⇔ (∃v ∈ U)⟨u, v⟩ ∈ q] (that is, dom p = dom q).

Proof of Claim 7. The implications from right to left are obvious by the definitions. The other directions are also easy, but they need some extra consideration. E.g. p˘ ; p ≤ 1′ clearly implies, that for any ⟨u, v⟩ ∈ E, if ⟨w, u⟩ ∈ p and ⟨w, v⟩ ∈ p for some w ∈ U then u = v must hold. However, for any u, v ∈ U, if ⟨w, u⟩ ∈ p and ⟨w, v⟩ ∈ p for some w ∈ U then, since E is an equivalence relation, ⟨u, v⟩ ∈ E must hold, proving that p is a partial function on U. Similar argument works for cases (ii) and (iii). In case (v), p˘ ; q = 1 clearly implies that dom p ∩ dom E = dom q ∩ dom E. But dom E = U, since E is reflexive.

Lemma 8 below is our basic technical tool in proving Theorem 6 and the other representation theorems below. It states that, in ZF^{−} + BAF A_{0}, properties (p1)–(p3) do characterize projection structures up to isomorphism.

LEMMA 8 (in ZF^{−} +BAF A_{0}) Let p and q be binary relations on some set U. Then the structure ⟨U, p, q⟩ is isomorphic to some projection structure ⟨W, P_{W} , Q_{W} ⟩ iff p and q have properties (p1)–(p3) above.

The proof of Lemma 8 is in section 3. We note that its non-trivial direction obviously fails in ZF C. E.g. consider some one-element set U = {u} with dom p = dom q = {u} and with p(u) = q(u) = u. Then ⟨U, p, q⟩ clearly have properties (p1)–(p3). On the other hand, every set which is in the domain of both projections is the ordered pair of its left and right projections. Thus, if ⟨U, p, q⟩ were isomorphic to the projection structure of some set W = {w} then w = ⟨P_{W} (w), Q_{W} (w)⟩ = ⟨w, w⟩ = {{w}} would hold. However, such a set w cannot be well-founded. See section 4 for some non-well-founded set theories where this lemma also fails.

Proof of Theorem 6. Let A = ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′, p, q⟩ be a partial projection algebra. Then by (P0)–(P2) and (P4), the relation algebra type reduct A^{−} of A is a QRA. Therefore, by Theorem 3, A^{−} is representable, i.e. there is some isomorphism g to a set relation algebra B, say with base U and unit E. By Claim 7(i)–(iii), g(p) and g(q) satisfy properties (p1)–(p3). Therefore, by Lemma 8, there is some isomorphism F from the structure ⟨U, g(p), g(q)⟩ to the projection structure ⟨W, P_{W} , Q_{W} ⟩ of some set W. Let C be the set relation algebra on base W that is isomorphic to B via the mapping f from binary relations on U to binary relations on W, induced by the bijection F : U → W. (E.g. the unit of C is f(E) = {⟨f(u), f(v)⟩ : ⟨u, v⟩ ∈ E} and f(g(p)) = P_{W}, f(g(q)) = Q_{W}.) Then the algebra ⟨B, g(p), g(q)⟩ is certainly isomorphic to ⟨C, P_{W} , Q_{W} ⟩. It remains to show that ⟨C, P_{W} , Q_{W} ⟩ ∈ SetPPA. First, since g(p) ⊆ E and P_{W} = f(g(p)), P_{W} ⊆ f(E) (and similarly, Q_{W} ⊆ f(E)), thus ⟨C, P_{W} , Q_{W} ⟩ = ⟨C, P_{W} ∩f(E), Q_{W} ∩f(E)⟩. Finally, we show that f(E) is closed. Indeed, take some ⟨a, b⟩ ∈ f(E). Since equation (P4) is valid in ⟨C, P_{W} , Q_{W} ⟩, Claim 7(iv) implies that there is some c ∈ W with P_{W} (c) = a and Q_{W} (c) = b. Since P_{W} and Q_{W} are the projections on W, this c must be equal to ⟨a, b⟩ that is, ⟨⟨a, b⟩, a⟩ ∈ P_{W} = P_{W} ∩ f(E) ⊆ f(E) and similarly, ⟨⟨a, b⟩, b⟩ ∈ f(E) hold. We proved that the partial projection algebra A is isomorphic to the partial projection set algebra ⟨C, P_{W} , Q_{W} ⟩.

[figure: ⟨A^{−}, p, q⟩; g; ⟨B, g(p), g(q)⟩; f; ⟨C, P_{W} , Q_{W} ⟩ ∈ SetPPA; ⟨C, P_{W} ∩ f(E), Q_{W} ∩ f(E)⟩; ⟨U, g(p), g(q)⟩; F; ⟨W, P_{W} , Q_{W} ⟩]

It is routine to check that every partial projection set algebra satisfies equations (P0)–(P4). We note that the unit of a SetPPA is taken to be closed in order to satisfy (P4).

A partial projection algebra is called a projection algebra (a PA) if it also satisfies equation (P5) below.

(P5) p ; 1 = q ; 1

Obviously, PA ⊆ PPA holds.

THEOREM 9 (in ZF C^{−} + BAF A_{0}) Every projection algebra is representable that is, it is isomorphic to some projection set algebra. Consequently,

PA = I SetPA

that is, the class of representable projection algebras is axiomatizable with finitely many equations, namely with (P0)–(P5).

Proof. Using the notation of the previous proof, if (P5) holds in A then (P5) also holds in ⟨C, P_{W} , Q_{W} ⟩ (since it is isomorphic to A via mapping f). Thus, by Claim 7(v), dom P_{W} = dom Q_{W} holds. On the other hand, projection set algebras clearly satisfy (P5), also by Claim 7(v).

Instead of expanding the similarity type of relation algebras with the constant symbols p and q, one can introduce a binary function symbol ▽, called fork, as it is done in e.g. Veloso–Haeberer [42], [43], [16], Baum–Haeberer–Veloso [7], Berghammer et al [8], Frias et al [9], Baum et al [6], Frias–Gordillo [10]. Let R, S be binary relations on some set U. Then R▽_{U}S is the following binary relation.

R▽_{U}S =^{def} {⟨u, ⟨v, w⟩⟩ : ⟨u, v⟩ ∈ R, ⟨u, w⟩ ∈ S}

[figure: · u; · w; v ·; · ⟨v, w⟩; ∈ R; ∈ S; ∈ R▽_{U}S]

The picture above motivates the name ‘fork’. We note that R▽_{U}S is not necessarily a binary relation on U, since ⟨v, w⟩ ∉ U can happen for some v, w ∈ U.

DEFINITION 10 A fork algebra (an FA) is an algebra ⟨A, +, ·, 1, 0, −, ; ,˘ , 1′, ▽⟩ satisfying equations (F0)–(F3) below.

(F0) (R0)–(R7)

(F1) x▽y = (x ; (1′▽1)) · (y ; (1▽1′))

(F2) (x▽y) ; (z▽w)˘ = (x ; z˘ ) · (y ; w˘ )

(F3) (1′▽1)˘ ▽(1▽1′)˘ ≤ 1′

A fork set algebra (a SetFA) is an algebra ⟨A, ▽⟩ such that

(i) A is a set relation algebra, say with base U and unit E;

(ii) ▽ coincides with ▽_{U};

(iii) E is closed under ▽_{U} i.e., for any R, S ⊆ E, R▽_{U}S ⊆ E also holds. □

Claim 11 (in ZF^{−}) I SetFA ⊆ FA.

We note that algebras satisfying (F0)–(F3) are called pre-fork algebras in Gyuris [13], [14]. Recently, the fork algebra literature started to call the models of (F0)–(F3) abstract fork algebras, cf. Frias et al [10], [11].

Next we discuss the connection between the two ways of expanding relation algebras. Namely, we show that fork algebras and projection algebras are equivalent in the strongest possible sense. To this end, consider the terms

p^{▽} =^{def} (1′▽1)˘ and

q^{▽} =^{def} (1▽1′)˘

of the similarity type of fork algebras; and the term

x▽^{pq}y := (x ; p˘ ) · (y ; q˘ )

of the similarity type of projection algebras.

Claim 12 (in ZF^{−}) For any set relation algebra A, say with base U and unit E, the following hold.

(i) E is closed iff E is closed under ▽_{U}.

(ii) Let p = P_{U} ∩E, q = Q_{U} ∩E. Then for any R, S ∈ A, R▽^{pq}S = R▽_{U}S holds. Consequently, if ⟨A, p, q⟩ ∈ SetPPA then ⟨A, ▽^{pq}⟩ ∈ SetFA.

Proof. For (i): Assume E is closed and let R, S ⊆ E. For any ⟨u, ⟨v, w⟩⟩ ∈ R▽_{U}S, ⟨u, v⟩ ∈ R ⊆ E and ⟨u, w⟩ ∈ S ⊆ E, thus ⟨v, w⟩ ∈ E also holds. This implies, by E being closed, that ⟨⟨v, w⟩, v⟩ ∈ E and therefore, by ⟨u, v⟩ ∈ E, ⟨u, ⟨v, w⟩⟩ ∈ E.

In the other direction, for any ⟨u, v⟩ ∈ E, ⟨⟨u, v⟩, u⟩ ∈ (1′▽_{U}1)˘ thus, by E being closed under ▽_{U}, ⟨⟨u, v⟩, u⟩ ∈ E holds.

Item (ii) can be proved by a routine computation.

THEOREM 13 (in ZF^{−}) The classes FA and PA are equivalent in the following sense (cf. McKenzie–McNulty–Taylor [25, Def. 4.138]).

(i) [cf. Gyuris [13], [14]] For any ⟨A, ▽⟩ ∈ FA, ⟨A, p^{▽}, q^{▽}⟩ ∈ PA.

(ii) For any ⟨A, p, q⟩ ∈ PPA, ⟨A, ▽^{pq}⟩ ∈ FA.

(iii) The equation x▽y = x▽^{p^{▽}q^{▽}}y is valid in FA.

(iv) The equations p = p^{▽^{pq}} and q = q^{▽^{pq}} are valid in PA.

Proof. For (i): We quote from [13], [14] the derivations of (P1), (P2) and (P4):

p^{▽}˘ ; p^{▽} = (1′▽1)˘ ˘ ; (1′▽1)˘ =^{(F0),(F2)} (1′ ; 1′˘ ) · (1 ; 1˘ ) ≤^{(F0)} 1′

q^{▽}˘ ; q^{▽} = (1▽1′)˘ ˘ ; (1▽1′)˘ =^{(F0),(F2)} (1 ; 1˘ ) · (1′ ; 1′˘ ) ≤^{(F0)} 1′

p^{▽}˘ ; q^{▽} = (1′▽1)˘ ˘ ; (1▽1′)˘ =^{(F0),(F2)} (1′ ; 1˘ ) · (1 ; 1′˘ ) =^{(F0)} 1.

(P3) can be derived as follows.

(p^{▽} ; p^{▽}˘ ) · (q^{▽} ; q^{▽}˘ ) =^{(F2)} (p^{▽}▽q^{▽}) ; (p^{▽}▽q^{▽})˘ =

= [(1′▽1)˘ ▽(1▽1′)˘ ] ; [(1′▽1)˘ ▽(1▽1′)˘ ]˘ ≤^{(F0),(F3)} 1′ ; 1′˘ =^{(F0)} 1′.

Finally, for (P5):

1 ; (1′▽1) ≤^{(F0),(F1)} 1 ; (1▽1) =^{(F1)} 1 ; [(1 ; (1′▽1)) · (1 ; (1▽1′))] ≤^{(F0)} 1 ; (1▽1′).

Therefore p^{▽} ; 1 = (1′▽1)˘ ; 1 =^{(F0)} (1 ; (1′▽1))˘ ≤^{(F0)} (1 ; (1▽1′))˘ =^{(F0)} q^{▽} ; 1.

For (ii): Assume that some of the equations (F0)–(F3) (with ▽^{pq} in place of ▽) fails in some PPA. Then it also fails in some countable subalgebra B of the PPA in question. The relation algebraic reduct of B is a QRA thus, by Theorem 3, it is representable that is, isomorphic to an algebra whose elements are binary relations. (For countable algebras, Theorem 3 can be proved without the Axiom of Choice.) Now it is routine to check that equations (F0)–(F3) (with ▽^{pq}) hold in those PPA’s whose elements are binary relations.

For (iii): x▽^{p^{▽}q^{▽}}y = (x ; p^{▽}˘ ) · (y ; q^{▽}˘ ) = [(x ; (1′▽1)˘ ˘ ] · [y ; (1▽1′)˘ ˘ ] =^{(F0),(F1)} x▽y.

For (iv): p^{▽^{pq}} = (1′▽^{pq}1)˘ = [(1′ ; p˘ ) · (1 ; q˘ )]˘ =^{(P0)} (1′ ; p˘ )˘ · (1 ; q˘ )˘ =^{(P0)} p · (q ; 1) =^{(P5)}

p · (p ; 1) =^{(P0)} p. One can prove q^{▽^{pq}} = q in a similar way.

It is proved in Sain–Németi [36] that, in ZF C, the class SetFA cannot support a representation theory (cf. section 4 below). However, in ZF C^{−} + BAF A_{0}, we have a representation theorem for partial projection algebras (Theorem 6 above) which, by Claim 12 and Theorem 13, can be ‘converted to’ a representation theorem of fork algebras.

THEOREM 14 (in ZF C^{−} + BAF A_{0}) Every fork algebra is representable that is, it is isomorphic to some set fork algebra. Consequently,

FA = I SetFA

that is, the class of representable fork algebras is axiomatizable with finitely many equations, namely with (F0)–(F3).

Proof. Let ⟨A, ▽⟩ ∈ FA. Then, by Theorem 13(i), ⟨A, p^{▽}, q^{▽}⟩ ∈ PPA. Thus, by Theorem 6, ⟨A, p^{▽}, q^{▽}⟩ is isomorphic to some ⟨B, p, q⟩ ∈ SetPPA. Therefore, by Claim 12, ⟨B, ▽^{pq}⟩ ∈ SetFA which is certainly isomorphic to ⟨A, ▽^{p^{▽}q^{▽}}⟩. But, by Theorem 13(iii), the latter is just ⟨A, ▽⟩.

Remark 15 Besides their finite axiomatizability, the classes I SetPPA, I SetPA and I SetFA have other ‘nice’ properties in the set theory ZF C^{−} + BAF A_{0}. Namely, in ZF C^{−} + BAF A_{0}, these classes enjoy the so called super amalgamation property (and hence the so called strong amalgamation property), in the sense of Madarász [19], Marx [23]. The proofs of these theorems are analogous with the proof (in ZF C) of the strong amalgamation property of QRA, given in Sain [33]. □

3 Projection functions in non-well-founded set theories

THEOREM 16 [cf. Aczel [1]] If ZF C^{−} is consistent then ‘ZF C^{−} + BAF A_{0}+collection principle’ is also consistent.

Proof. Since in [1] this theorem is not explicitly stated, we list the main ‘landmarks’ of its proof in [1]. Our formulation of BAF A_{0} is denoted by BA_{1} in [1]. Boffa’s Anti-foundation Axiom BAF A is formulated on p.59, and Exercise 5.14 on p.65 states that BAF A implies BA_{1}. On p.61 it is stated that ‘BAF A 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 ‘ZF C^{−}+collection principle’. Next, Theorem 5.18 on p.66 states that, assuming that there is a definable well-ordering of the universe, there exists a superuniversal system. Finally, the assumption that ‘there is a definable well-ordering of the universe’ holds in the constructible universe L, and V = L is consistent with ZF C^{−}.

Proof of Lemma 8 of section 2. We start with introducing some notation. Let E be a binary relation on some set V. For u, v_{1},…, v_{n} ∈ V,

u = {v_{1},…, v_{n}}_{E} ⟺^{def} (∀z ∈ V) (⟨z, u⟩ ∈ E ⇔ (z = v_{1} or … or z = v_{n})).

In case of u = {v_{1},…, v_{n}}_{E} we say that v_{1},…, v_{n} are the E-elements of u. Similarly, for any u ∈ V and v ≠ w ∈ V,

u = ⟨v, v⟩_{E}  ⟺^{def}  (∃x ∈ V) x = {v}_{E} and u = {x}_{E}
u = ⟨v, w⟩_{E}  ⟺^{def}  (∃x, y ∈ V) x = {v}_{E}, y = {v, w}_{E} and u = {x, y}_{E}.

If u = ⟨v, w⟩_{E} we say that u is the E-pair of v and w.

Now assume that some structure ⟨U, p, q⟩ satisfying (p1)–(p3) is given. We will construct a structure ⟨V, E⟩ for some set V ⊇ U such that the following hold.

(♯) (∀u, v ∈ U) (p(u) = v ⟺ u = ⟨v, x⟩_{E} for some x ∈ V)

(♯♯) (∀u, v ∈ U) (q(u) = v ⟺ u = ⟨x, v⟩_{E} for some x ∈ V).

The motivation for the construction is as follows. The structure ⟨V, E⟩ is intended to ‘mimic’ the ∈-structure of the transitive closure^{7} of some set whose projection structure is isomorphic to ⟨U, p, q⟩. If we want to find some transitive set such that its ∈-structure is isomorphic to ⟨V, E⟩ then we also have to ensure the extensionality of ⟨V, E⟩. In order to achieve extensionality, in the construction of V we always take new sets unless it is ‘explicitly required’ that some set coincides with one of the sets already taken.

What kind of new sets do we need in V to have properties (♯) and (♯♯)? Certainly, for each v ≠ w ∈ U such that p(u) = v and q(u) = w for some u ∈ dom p ∩ dom q, we need a new^{8} set, call it pair_{vw}, which ‘mimics’ the set {v, w}. We also take the following new sets:

• singl_{v}, for each v ∈ U such that v = p(u) for some u ∈ dom p;

• pair_{?u} and ?_{u}, for each u ∈ dom p − dom q;

• pair_{∗u}, singl_{∗u} and ∗_{u}, for each u ∈ dom q − dom p;

• ♣_{u} and ♠_{u}, for each u ∈ U − (dom p ∪ dom q).

Now let V be the expansion of U with these new sets.

Next we are defining a binary relation E on V. First, for each u ∈ dom p ∩ dom q, add the following pairs to E (in the figures below ⟨x, y⟩ ∈ E is illustrated by x → y):

[figure: if p(u) ≠ q(u); · u; · singl_{p(u)}; · p(u); pair_{p(u)q(u)} ·; q(u) ·]

[figure: if p(u) = q(u); · u; · singl_{p(u)}; · p(u)]

7The transitive closure of some set x is the smallest transitive set containing x as a subset.

8Such new sets certainly exist, even in non-well-founded set theories. However, to be explicit, e.g. one can choose pair_{vw} to be the set {α, v, w}, where α is the smallest ordinal which is not in the transitive closure of U.

For each u ∈ dom p − dom q, add the following pairs to E:

[figure: · u; · singl_{p(u)}; · p(u); pair_{?u} ·; ?_{u} ·]

For each u ∈ dom q − dom p, add the following pairs to E:

[figure: · u; · singl_{∗u}; · ∗_{u}; pair_{∗u} ·; q(u) ·]

For each u ∈ U − (dom p ∪ dom q), add the following pairs to E:

[figure: · u; · ♣_{u}; · ♠_{u}]

Claim 16.1 ⟨V, E⟩ satisfies properties (♯) and (♯♯) above.

Proof of Claim 16.1. To prove (♯), take some u, v ∈ U and assume p(u) = v. If u ∈ dom p ∩ dom q and also q(u) = v then u = {singl_{v}}_{E} and singl_{v} = {v}_{E}, thus u = ⟨v, v⟩_{E}. If q(u) ≠ v then u = {singl_{v}, pair_{vq(u)}}_{E} and singl_{v} = {v}_{E}, pair_{vq(u)} = {v, q(u)}_{E}, thus u = ⟨v, q(u)⟩_{E}. If u ∈ dom p − dom q then u = {singl_{v}, pair_{?u}}_{E} and singl_{v} = {v}_{E}, pair_{?u} = {v,?_{u}}_{E}, thus u = ⟨v,?_{u}⟩_{E}.

For the other direction of (♯), assume that u = ⟨v, x⟩_{E}, for some u, v ∈ U and x ∈ V. Then u must belong to dom p ∪ dom q, since inspection shows that elements of U − (dom p ∪ dom q) are not E-pairs. We show that u ∈ dom p must hold. Indeed, assume u ∈ dom q − dom p. Then u = {singl_{∗u}, pair_{∗u}}_{E}. Thus either singl_{∗u} = {v}_{E} or pair_{∗u} = {v}_{E}. In the first case v = ∗_{u}, contradicting v ∈ U. The second case cannot happen, since pair_{∗u} has two E-elements. So we have u ∈ dom p. Then ⟨singl_{p(u)}, u⟩ ∈ E and singl_{p(u)} has exactly one E-element. Therefore it follows from u = ⟨v, x⟩_{E} that singl_{p(u)} = {v}_{E}, implying p(u) = v.

Property (♯♯) can be proved similarly.

Claim 16.2 ⟨V, E⟩ is extensional.

Proof of Claim 16.2. We will say that z ∈ V E-distinguishes x ∈ V from y ∈ V if ⟨z, x⟩ ∈ E and ⟨z, y⟩ ∉ E or the other way round. We say that x, y ∈ V are E-distinguishable if there is some z ∈ V that E-distinguishes between them. We have to prove that any x ≠ y ∈ V are E-distinguishable. To this end, let the subset V_{0} ⊆ V be defined as follows.

V_{0} =^{def} U ∪ {singl_{v} : v ∈ U and ∃u ∈ U with p(u) = v} ∪

∪ {pair_{vw} : v ≠ w ∈ U and ∃u ∈ U with p(u) = v, q(u) = w}.

First, we show that any x ∈ V_{0} and y ∈ V −V_{0} are E-distinguishable. Indeed, ?_{u} E-distinguishes members of V_{0} from ?_{u} and also from pair_{?u}; ∗_{u} E-distinguishes members of V_{0} from ∗_{u}, from pair_{∗u} and also from singl_{∗u}; ♠_{u} E-distinguishes members of V_{0} from ♠_{u} and also from ♣_{u}.

Second, we show that any x ≠ y ∈ V − V_{0} are E-distinguishable. Indeed, for any u ∈ dom p − dom q, pair_{?u} has two E-elements, while ?_{u} has only one, thus they must be E-distinguishable. For any u ≠ v ∈ dom p − dom q, ?_{u} E-distinguishes ?_{u} from ?_{v}, and also pair_{?u} from pair_{?v}. For any u ∈ dom q − dom p, both pair_{∗u} and ∗_{u} have two E-elements, while singl_{∗u} has only one, thus singl_{∗u} is E-distinguishable from pair_{∗u} and also from ∗_{u}; and e.g. q(u) E-distinguishes pair_{∗u} from ∗_{u}. For any u ≠ v ∈ dom q − dom p, ∗_{u} E-distinguishes ∗_{u} from ∗_{v}, singl_{∗u} from singl_{∗v}, and also pair_{∗u} from pair_{∗v}. ?_{u} E-distinguishes ?_{u} from ∗_{v}, from singl_{∗v}, and from pair_{∗v}; and also pair_{?u} from ∗_{v}, from singl_{∗v}, and from pair_{∗v}. ♣_{u} E-distinguishes ♣_{u} from ♠_{u}, and ♠_{u} E-distinguishes other members of V − V_{0} from ♠_{u} and from ♣_{u}.

Third, we show that any x ≠ y ∈ V_{0} are E-distinguishable. Indeed, for any u, v, w ∈ U, u and singl_{v}, and also u and pair_{vw} are E-distinguishable, since every E-element of singl_{v} and pair_{vw} belongs to U, while u always has some E-element which does not belong to U. pair_{vw} has two E-elements, while singl_{v} has only one, thus they must be E-distinguishable. For any v_{1} ≠ v_{2} such that v_{1} = p(u_{1}), v_{2} = p(u_{2}) for some u_{1}, u_{2} ∈ U, v_{1} E-distinguishes singl_{v_{1}} from singl_{v_{2}}. Take any v_{1} ≠ w_{1} and v_{2} ≠ w_{2} such that {v_{1}, w_{1}} ≠ {v_{2}, w_{2}} and v_{1} = p(u_{1}), w_{1} = q(u_{1}), v_{2} = p(u_{2}), w_{2} = q(u_{2}) for some u_{1}, u_{2} ∈ U. If v_{1} ≠ v_{2} then v_{1} E-distinguishes pair_{v_{1}w_{1}} from pair_{v_{2}w_{2}}. If v_{1} = v_{2} then w_{1} ≠ w_{2} must hold, thus w_{1} E-distinguishes pair_{v_{1}w_{1}} from pair_{v_{2}w_{2}}. It remains to E-distinguish the elements of U from each other. U can be partitioned to the following four parts:

U = (dom p ∩ dom q) ∪ (dom p − dom q) ∪ (dom q − dom p) ∪ (U − (dom p ∪ dom q)).

Then for any u ∈ U,

u ∈ dom p − dom q ⟺ ⟨pair_{?u}, u⟩ ∈ E,
u ∈ dom q − dom p ⟺ ⟨singl_{∗u}, u⟩ ∈ E
u ∈ U − (dom p ∪ dom q) ⟺ ⟨♣_{u}, u⟩ ∈ E.

Thus, if u and v are in different blocks of the partition above then they must be E-distinguishable.

If u ≠ v ∈ dom p ∩ dom q then, by property (p3), either p(u) ≠ p(v) or q(u) ≠ q(v). If p(u) ≠ p(v) then singl_{p(u)} E-distinguishes u from v. If p(u) = p(v) and q(u) ≠ q(v) then either p(u) = q(u) or not. If p(u) = q(u) then p(v) ≠ q(v), thus v has two E-elements and u has only one, thus they must be E-distinguishable. If p(u) ≠ q(u) then pair_{p(u)q(u)} E-distinguishes u from v.

If u ≠ v ∈ dom p − dom q then pair_{?u} E-distinguishes between them. If u ≠ v ∈ dom q − dom p then singl_{∗u} E-distinguishes between them. If u ≠ v ∈ U − (dom p ∪ dom q) then u E-distinguishes between them, completing the proof of Claim 16.2.

So we have an extensional structure ⟨V, E⟩. Therefore, by BAF A_{0}, ⟨V, E⟩ is isomorphic to ⟨Z, ∈_{Z}⟩ for some transitive set Z. Call this isomorhpism f. Then it is easy to check that

(♯♯♯) (∀x, y, z ∈ V) (x = ⟨y, z⟩_{E} ⟺ f(x) = ⟨f(y), f(z)⟩).

Let W =^{def} {f(u) : u ∈ U}. We claim that the restriction of f to U is an isomorphism between ⟨U, p, q⟩ and the projection structure ⟨W, P_{W} , Q_{W} ⟩. Indeed, for any u, v ∈ U, if ⟨u, v⟩ ∈ p then, by (♯), u = ⟨v, x⟩_{E} for some x ∈ V therefore, by (♯♯♯), f(u) = ⟨f(v), f(x)⟩. Since u, v ∈ U implies f(u), f(v) ∈ W, we obtain ⟨f(u), f(v)⟩ ∈ P_{W}. For the other direction, assume ⟨f(u), f(v)⟩ ∈ P_{W} for some u, v ∈ U. Then f(u) = ⟨f(v), y⟩ for some set y. But f(u) ∈ W ⊆ Z and Z is transitive, thus there is some x ∈ V with f(x) = y. This implies, by (♯♯♯) and (♯), that ⟨u, v⟩ ∈ p.

(⟨u, v⟩ ∈ q ⇔ ⟨f(u), f(v)⟩ ∈ Q_{W}) can be proved in a similar way, completing the proof of Lemma 8.

4 A summary of negative results

In this section we summarize the negative results of Sain–Németi [36] concerning the representation theory of the expanded relation algebras introduced in section 2. We will see that it is not really the Axiom of Foundation that is ‘responsible’ for the failure of the representation theorems in ZF C, but rather the following version of Extensionality, called the Axiom of Strong Extensionality (SE). This axiom ‘helps to identify’ non-well-founded sets.

(SE) For any transitive sets x, y, if the structures ⟨x, ∈⟩ and ⟨y, ∈⟩ are isomorphic then x = y.

SE is an axiom of ‘forbidding’ type. It does not state the existence of anything, but it forbids to exist ‘too many’ or ‘too ugly’ sets. E.g. one can prove from SE that there are no infinite descending ∈-chains of distinct singletons as follows. Assume we have such a chain, say

u_{0} ∋ u_{1} ∋ u_{2} ∋ ….

Then the transitive closure trc(u_{0}) of u_{0} is not equal to trc(u_{1}), since u_{1} ∈ trc(u_{0}) − trc(u_{1}). But ⟨trc(u_{0}), ∈⟩ and ⟨trc(u_{1}), ∈⟩ are isomorphic structures, contradicting SE.

SE is a theorem both of ZF and of the non-well-founded set theories in Barwise–Etchemendy [5]. To unify the various non-well-founded set theories, Aczel [1, section 4] introduces the flexible axiom AF A^{∼}, where the special equivalence relation ∼ is a parameter of the axiom. For various choices of ∼, we obtain different anti-foundation axioms, e.g. Scott’s anti-foundation axiom, the basic variant AF A of Aczel, Finsler’s anti-foundation axiom, etc. [1, Prop.4.26, p.52] shows that SE is a theorem in all of these set theories. (Our axiom SE is a part of Finsler’s axiom and is denoted by F AF A_{2} in [1].)

The following claim states that Lemma 8 of section 3 fails in strongly extensional set theories.

Claim 17 (in ZF^{−} +SE) There is some structure ⟨U, p, q⟩ satisfying properties (p1)–(p3) which is not isomorphic to any projection system.

Proof. Consider the set ω of natural numbers and the usual successor function suc. Then ⟨ω, suc, suc⟩ certainly satisfies (p1)–(p3). Assume that ⟨ω, suc, suc⟩ is isomorphic to some projection system ⟨U, P_{U}, Q_{U}⟩. Then U is a countable set, say U = {u_{n} : n ∈ ω}, and for any n ∈ ω, u_{n} = ⟨P_{U}(u_{n}), Q_{U}(u_{n})⟩ = ⟨u_{n+1}, u_{n+1}⟩ = {{u_{n+1}}}. Therefore

u_{0} ∋ {u_{1}} ∋ u_{1} ∋ {u_{2}} ∋ u_{2} ∋ …

is an infinite descending ∈-chain of distinct singletons, contradicting SE.

Our main representation theorems also fail if one uses some strongly extensional metatheory: the classes of representable algebras are not axiomatizable by finitely many equations. Moreover, the following stronger theorem holds.

THEOREM 18 [Sain-Németi [36]] (in ZF^{−} + SE) The classes I SetPPA, I SetPA and I SetFA are not axiomatizable by any set of first-order sentences.

Idea of proof. It is proved in [36] that one can find a ‘bad’ ultrapower of some set algebra (belonging to any of the above classes) such that any set algebra which is isomorphic to that ‘bad’ ultrapower must contain an infinite descending ∈-chain of distinct singletons. The Axiom of Choice can be eliminated by replacing ultrapowers with using the compactness theorem for countable languages.

The following theorem states that, in strongly extensional set theories, even the equational theories of the above classes are very far from being computable. This theorem was first proved in Sain–Simon [37] in ZF. The proof in ZF^{−} + SE is published in [36].

THEOREM 19 [cf. Sain-Németi [36]] (in ZF^{−} + SE) The equational theories of the classes SetPPA, SetPA and SetFA are Π_{1}^{1}-hard. Consequently, they are not recursively enumerable. In particular, they are not finitely axiomatizable.

Idea of proof. It is proved in [36] that there is a recursive translation, sending each first-order formula φ of the language of arithmetic to some equation e_{φ} of the similarity type of projection algebras (or of fork algebras), such that

φ holds in the standard model of arithmetic iff (say) I SetPA ⊧ e_{φ}.

The idea behind the above translation is that in any A ∈ SetPA with base U, one can define a structure isomorphic to some model of arithmetic. In particular, (p^{A} ∩ q^{A})˘ plays the role of the successor function. SE comes into the picture when one tries to prove that p^{A} ∩ q^{A} is not ‘nonstandard’ in the sense that there is no infinite ‘predecessor-chain’ that is, there is no infinite sequence of distinct elements u_{0}, u_{1}, u_{2},… ∈ U with

(∀n ∈ ω) (p^{A} ∩ q^{A})(u_{n}) = u_{n+1}.

Since A ∈ SetPA, p^{A} and q^{A} are the projections on U, thus such a chain would result in an infinite descending ∈-chain of distinct singletons

u_{0} ∋ {u_{1}} ∋ u_{1} ∋ {u_{2}} ∋ u_{2} ∋ …

(cf. the proof of Claim 17 above), contradicting SE.

Next we would like to mention some negative results of [36] which already hold in ZF^{−}. These theorems are about certain subclasses of our classes of representables. A set projection algebra A with base U is called a true pairing algebra (a TPA) (cf. Maddux [22], [21]) if its unit is U × U and^{9} there is some nonempty set U_{0} (called the set of urelements) with the following properties:

(i) U is the smallest set such that U_{0} ⊆ U and U × U ⊆ U;

(ii) U − U_{0} = U × U.

We note that for any A ∈ SetPA with base U, A ∈ TPA iff there is some set U_{0} of urelements which does not contain ordered pairs and U = ⋃_{n∈ω} U_{n}, where U_{n+1} = (⋃_{i≤n} U_{i}) × (⋃_{i≤n} U_{i}). Thus, the base of some TPA cannot contain infinite (p ∪ q)-chains. From this it follows that

(∗) (in ZF^{−}) the base of some TPA cannot contain infinite descending ∈-chains of distinct singletons.

Indeed, if u_{0} ∋ u_{1} ∋ u_{2} ∋ … were such a chain then u_{0} = {u_{1}} = {{u_{2}}} = ⟨u_{2}, u_{2}⟩, u_{2} = ⟨u_{4}, u_{4}⟩, etc. would hold. Therefore ⟨u_{0}, u_{2}, u_{4},…⟩ would be an infinite (p ∪ q)-chain.

The following theorem was first proved in Sain–Simon [37], cf. also [26]. The proof is published in [36].

THEOREM 20 (in ZF^{−})

(i) I TPA and SPTPA are not axiomatizable by any set of first-order sentences.

(ii) The equational theory of TPA is Π_{1}^{1}-hard. Therefore it is not finitely axiomatizable.

Idea of proof. It is in [36]. In fact, the proofs of Theorem 18 and 19 go through without SE in this case, because of (∗) above.

Finally, we note that one can define a class, called the class of true fork algebras, in a way similar to TPA. Then the equational theory of true fork algebras is provably non-finitely axiomatizable, already in ZF^{−} (hence the same holds in any extension, like ZF C^{−} + BAF A_{0}, of ZF^{−}). The same applies to the so called ‘concatenation version’ (cf. Haeberer–Veloso [16]), to the ‘free groupoid version’ (cf. Baum–Haeberer–Veloso [7]) and to the ‘finite tree version’ (cf. Haeberer– Baum–Schmidt [15]) of fork algebras, because the equational theory of TPA is interpretable in the equational theories of these classes. These results as well as some further negative results in this line are proved in [36].

9In [22], notation ‘TPA’ denoted the class of those TPA’s which consist of all the subsets of some set U × U.

5 The finitization problem, connections with logic

The finitization problem of algebraic logic (cf. e.g. [28]) asks whether the reason for non-finite axiomatizability of the classes of representable relation algebras or finite dimensional representable cylindric algebras is caused only by Tarski’s not including enough operations on relations into the definitions of these classes. A possible formulation of this problem is the following.

For any set U, let R(U × U) denote the full set relation algebra with base U (cf. Definition 2). Consider the question whether

one can add to the operations of set relation algebras finitely many natural operations f_{1},…, f_{n} such that the class

SP{⟨R(U × U), f_{1},…, f_{n}⟩ : U is a set}

would be a finitely axiomatizable variety (or quasivariety).

A key issue here is what ‘naturalness’ requirements the extra operations f_{1},…, f_{n} should satisfy. The so called soft version of the finitization problem requires f_{1},…, f_{n} to be set theoretically definable (without parameters). This requirement is motivated by the fact that the other operations ∩, ; , ˘ , etc. of set relation algebras are set theoretically definable operations (see below for further motivations coming from logic). Typical examples for set theoretically definable operations are the projections P_{U}, Q_{U} and the fork operation ▽_{U}. The hard version of the finitization problem requires f_{1},…, f_{n} to be invariant under all permutations of U.^{10} A typical example for such an f_{i} is taking the transitive closure R^{∗} of a relation R. In ZF C, no solution is known for either the soft or the hard version of the finitization problem, cf. e.g. [28].^{11} As a contrast, by Theorems 6, 9 and 14 way above, in ZF C^{−} + BAF A_{0} the soft version of the finitization problem does admit positive solutions.

There are various motivations for the finitization problem coming from ‘pure’ logic.

(1) First order logic L_{ωω} is such that its valid formula schemas cannot be axiomatized by any finite schema of axioms and rules. The question is whether there is a new logic L_{ωω}^{+}, containing L_{ωω} as a (definable) fragment, such that L_{ωω}^{+} admits a finite axiomatization of schemas. The new connectives of L_{ωω}^{+} are subject to some ‘naturalness’ conditions (this is where the above conditions on f_{i} come from).

(2) The finite variable fragments L_{n} of L_{ωω} are strongly incomplete in the sense that they admit no finite schema axiomatization, cf. [28].^{12} The task here is to expand L_{n} with new logical connectives (e.g. with generalized quantifiers) such that the so obtained L_{n}^{+} would admit a complete finite axiomatization.

(3) In Marx–Venema [24, pp.115–123], it is described how L_{ωω} and L_{n} can be translated to equivalent propositional modal logics. It turns out there that these modal counterparts of L_{ωω} and L_{n} are not finitely axiomatizable. The question is whether these modal logics can be expanded with new (natural) connectives such that they would become finitely axiomatizable.

Using the (algebraic) results in this paper, the soft versions of the above problems (of logic) can receive positive answers, cf. e.g. [29], [30, section 5], [31].

10A, say, unary operation f is called permutation invariant on U if for any permutation π : U → U, and R ⊆ U ×U, π(f_{i}(R)) = f_{i}(π(R)) holds (where π(R) =^{def} {⟨π(u), π(v)⟩ : ⟨u, v⟩ ∈ R}).

11This applies only to the so called finite dimensional version of the problem. The infinite dimensional version was solved positively in Sain [32], [34], Sain–Gyuris [35].

12The same applies for the versions L_{∞,ω}^{n} and L_{κ,ω}^{n} (with κ ≥ ω) of L_{n} which allow infinite conjunctions built up from L_{n} formulas.

References

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

[2] H. Andréka, Complexity of the equations valid in algebras of relations, Thesis for D.Sc. (a post-habilitation degree) with Hungar. Acad. Sci., Budapest, 1991; http://circle.mathinst.hu/pub/algebraic-logic/complex.dvi; Annals of Pure and Applied Logic (to appear).

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

[4] H. Andréka, Á. Kurucz and I. Németi, Connections between axioms of set theory and basic theorems of universal algebra, this JOURNAL, vol. 59 (1994), pp. 912–923.

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

[6] G.A. Baum, M.F. Frias, 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.

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

[8] R. Berghammer, A.M. Haeberer, G. Schmidt and P.A.S. Veloso, Comparing two different approaches to products in abstract relation algebras, in: Proc. of AMAST’93 (eds.: M.Nivat, C.Rattray, T.Rus and G.Scollo), Workshops in Computing, Springer-Verlag, London, 1993.

[9] M.F. Frias, G.A. Baum, A.M. Haeberer and P.A.S. Veloso, Fork algebras are representable, Bull. of the Section of Logic, Univ. of Łódz, vol. 24(2) (1995), pp. 64–75.

[10] M.F. Frias and S. Gordillo, Semantic optimization of queries in deductive object-oriented database, to appear in Proc. of ADBIS’95, LNCS, Springer Verlag.

[11] M.F. Frias, A.M. Haeberer and P.A.S. Veloso, A finite axiomatization of fork algebras, Bull. of the Section of Logic, Univ. of Łódz, vol. 24(4) (1995), pp. 193–200.

[12] G. Grätzer, Universal Algebra, Springer Verlag, 1979, 2nd edition.

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

[14] V. Gyuris, Representability of fork algebras, Theoretical Computer Science (to appear).

[15] A.M. Haeberer, G.A. Baum and G. Schmidt, Dealing with non-constructive specifications involving quantifiers, Preprint, Pontifícia Univ. Católica do Rio de Janeiro, Dept. of Inf., 1993.

[16] A.M. Haeberer and P.A.S. Veloso, Partial relations for program derivation: adequacy, inevitability and expressiveness, in: ‘Constructing programs from specifications’ (ed.: B.Möller), Proc. of the IFIP TC2 Working Conference on Constructing Programs from Specifications, N.H., IFIP WG 2.1, 1991, pp.319–371.

[17] L. Henkin, J.D. Monk and A. Tarski, Cylindric Algebras, Part I, North-Holland, Amsterdam, 1971.

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

[19] J.X. Madarász, Interpolation in algebraizable logics; semantics for non-normal multi-modal logic, Journal of Applied Nonclassical Logic, Helena Rasiowa volume (to appear).

[20] R. Maddux, Some sufficient condition for the representability of relation algebras, Algebra Universalis, vol. 8 (1978), pp. 162–172.

[21] R. Maddux, Finitary algebraic logic, Zeitschr. f. math. Logik und Grundlagen d. Math., vol. 35 (1989), pp. 321–332.

[22] R. Maddux, Finitary algebraic logic, II, Math. Logic Quarterly (formerly: Zeitschr. f. math. Logik und Grundlagen d. Math.), vol. 39 (1993), pp. 566–569.

[23] M. Marx, Algebraic relativization and arrow logic, PhD Dissertation, University of Amsterdam, 1995.

[24] M. Marx and Y. Venema, Multi-Dimensional Modal Logic, Applied Logic Series Vol. 4, Kluwer Academic Publishers, 1997.

[25] 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.

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

[27] I. Németi, Free algebras and decidability in algebraic logic, Dissertation for D.Sc. with Hung. Academy of Sciences, Budapest, 1986. In Hungarian.

[28] I. Németi, Algebraization of quantifier logics, an introductory overview, 12th version, Preprint No. 13/1996., Math. Inst. Hungar. Acad. Sci., Budapest; http://circle.mathinst.hu/pub/algebraic-logic/survey.dvi; An extended abstract appeared in Studia Logica, vol. 50 (3,4) (1991), pp. 485–569.

[29] I. Németi, Ontology can turn negative results to positive, Bull. of the Section of Logic, Univ. of Łódz, vol. 25(1) (1996), pp. 29–40.

[30] I. Németi, Strong representability of fork algebras, a set theoretic foundation, Journal of the IGPL, vol. 5(1) (1997), pp. 3–23.

[31] I. Németi and A. Simon, Weakly higher order cylindric algebras and finite schema axiomatization of the representables, Preprint, Math. Inst. Hungar. Acad. Sci., Budapest, 1995.

[32] I. Sain, On the search for a finitizable algebraization of first order logic, Preprint, Math. Inst. Hungar. Acad. Sci., Budapest, 1997 (first version, 1988); http://circle.math-inst.hu/pub/algebraic-logic/finitize.dvi (submitted).

[33] I. Sain, Beth’s and Craig’s properties via epimorphisms and amalgamation in algebraic logic, in: Algebraic Logic and Universal Algebra in Computer Science (eds: C.H. Bergman, R.D. Maddux and D.L. Pigozzi), Lecture Notes in Comp. Sci. Vol. 425, Springer Verlag, 1990, pp. 209–226.

[34] I. Sain, On the problem of finitizing first order logic and its algebraic counterpart. (A survey of results and methods.), in: Logic Colloquium’92 (eds: L. Csirmaz, D.M. Gabbay and M. de Rijke), CSLI Publications, 1995, pp. 243–292.

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

[36] I. Sain and I. Németi, Fork algebras in usual and in non-well-founded set theories (an overview), Studia Logica Library, a special volume dedicated to the memory of Helena Rasiowa (to appear).

[37] I. Sain and A. Simon, The complexity of equational theory of relation algebras with projection elements, Preprint, Math. Inst. Hungar. Acad. Sci., Budapest, 1993.

[38] A. Simon, A purely algebraic proof of representability of quasi-projective relation algebras (QRA’s), Preprint, Math. Inst. Hungar. Acad. Sci., Budapest, 1995.

[39] S.G. Simpson, Which set existence axioms are needed to prove the Cauchy/Peano theorem? this JOURNAL, vol. 49 (1984), pp. 783–802.

[40] A. Tarski, On the calculus of relations, this JOURNAL, vol. 6 (1941), pp. 73–89.

[41] A. Tarski and S. Givant, A formalization of set theory without variables, AMS Colloquium Publications vol. 41, 1988.

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

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